diff --git a/src/Init/Grind/AC.lean b/src/Init/Grind/AC.lean
index 5243e014c7..47acb0975f 100644
--- a/src/Init/Grind/AC.lean
+++ b/src/Init/Grind/AC.lean
@@ -299,35 +299,82 @@ theorem Seq.denote_concat {α} (ctx : Context α) {inst₁ : Std.Associative ctx
 
 attribute [local simp] Seq.denote_concat
 
+theorem eq_orient {α} (ctx : Context α) (lhs rhs : Seq)
+    : lhs.denote ctx = rhs.denote ctx → rhs.denote ctx = lhs.denote ctx := by
+  simp_all
+
+theorem eq_simp_lhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq)
+    : lhs₁.denote ctx = rhs₁.denote ctx → lhs₁.denote ctx = rhs₂.denote ctx → rhs₁.denote ctx = rhs₂.denote ctx := by
+  simp_all
+
+theorem eq_simp_rhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq)
+    : lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = lhs₁.denote ctx → lhs₂.denote ctx = rhs₁.denote ctx := by
+  simp_all
+
+theorem diseq_simp_lhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ rhs₂ : Seq)
+    : lhs₁.denote ctx = rhs₁.denote ctx → lhs₁.denote ctx ≠ rhs₂.denote ctx → rhs₁.denote ctx ≠ rhs₂.denote ctx := by
+  simp_all
+
+theorem diseq_simp_rhs_exact {α} (ctx : Context α) (lhs₁ rhs₁ lhs₂ : Seq)
+    : lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ lhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₁.denote ctx := by
+  simp_all
+
 noncomputable def simp_prefix_cert (lhs rhs tail s s' : Seq) : Bool :=
   s.beq' (lhs.concat_k tail) |>.and' (s'.beq' (rhs.concat_k tail))
 
-/--
-Given `lhs = rhs`, and a term `s := lhs * tail`, rewrite it to `s' := rhs * tail`
--/
-theorem simp_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs tail s s' : Seq)
-    : simp_prefix_cert lhs rhs tail s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
-  simp [simp_prefix_cert]; intro _ _ h; subst s s'; simp [h]
+theorem eq_simp_lhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
+  simp [simp_prefix_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem eq_simp_rhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
+  simp [simp_prefix_cert]; intros; subst rhs₂ rhs₂'; simp_all
+
+theorem diseq_simp_lhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_prefix_cert lhs₁ rhs₁ tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
+  simp [simp_prefix_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem diseq_simp_rhs_prefix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ tail lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_prefix_cert lhs₁ rhs₁ tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
+  simp [simp_prefix_cert]; intros; subst rhs₂ rhs₂'; simp_all
 
 noncomputable def simp_suffix_cert (lhs rhs head s s' : Seq) : Bool :=
   s.beq' (head.concat_k lhs) |>.and' (s'.beq' (head.concat_k rhs))
 
-/--
-Given `lhs = rhs`, and a term `s := head * lhs`, rewrite it to `s' := head * rhs`
--/
-theorem simp_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs head s s' : Seq)
-    : simp_suffix_cert lhs rhs head s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
-  simp [simp_suffix_cert]; intro _ _ h; subst s s'; simp [h]
+theorem eq_simp_lhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
+  simp [simp_suffix_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem eq_simp_rhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
+  simp [simp_suffix_cert]; intros; subst rhs₂ rhs₂'; simp_all
+
+theorem diseq_simp_lhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
+  simp [simp_suffix_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem diseq_simp_rhs_suffix {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
+  simp [simp_suffix_cert]; intros; subst rhs₂ rhs₂'; simp_all
 
 noncomputable def simp_middle_cert (lhs rhs head tail s s' : Seq) : Bool :=
   s.beq' (head.concat_k (lhs.concat_k tail)) |>.and' (s'.beq' (head.concat_k (rhs.concat_k tail)))
 
-/--
-Given `lhs = rhs`, and a term `s := head * lhs * tail`, rewrite it to `s' := head * rhs * tail`
--/
-theorem simp_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs head tail s s' : Seq)
-    : simp_middle_cert lhs rhs head tail s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
-  simp [simp_middle_cert]; intro _ _ h; subst s s'; simp [h]
+theorem eq_simp_lhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
+  simp [simp_middle_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem eq_simp_rhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
+  simp [simp_middle_cert]; intros; subst rhs₂ rhs₂'; simp_all
+
+theorem diseq_simp_lhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
+  simp [simp_middle_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem diseq_simp_rhs_middle {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
+  simp [simp_middle_cert]; intros; subst rhs₂ rhs₂'; simp_all
 
 noncomputable def superpose_prefix_suffix_cert (p c s lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
   lhs₁.beq' (p.concat_k c) |>.and'
@@ -422,6 +469,22 @@ theorem simp_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst
     : simp_ac_cert c lhs rhs s s' → lhs.denote ctx = rhs.denote ctx → s.denote ctx = s'.denote ctx := by
   simp [simp_ac_cert]; intro _ _; subst s s'; simp; intro h; rw [h]
 
+theorem eq_simp_lhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂'.denote ctx = rhs₂.denote ctx := by
+  simp [simp_ac_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem eq_simp_rhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx = rhs₂.denote ctx → lhs₂.denote ctx = rhs₂'.denote ctx := by
+  simp [simp_ac_cert]; intros; subst rhs₂ rhs₂'; simp_all
+
+theorem diseq_simp_lhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Seq)
+    : simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂'.denote ctx ≠ rhs₂.denote ctx := by
+  simp [simp_ac_cert]; intros; subst lhs₂ lhs₂'; simp_all
+
+theorem diseq_simp_rhs_ac {α} (ctx : Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op} (c lhs₁ rhs₁ lhs₂ rhs₂ rhs₂' : Seq)
+    : simp_ac_cert c lhs₁ rhs₁ rhs₂ rhs₂' → lhs₁.denote ctx = rhs₁.denote ctx → lhs₂.denote ctx ≠ rhs₂.denote ctx → lhs₂.denote ctx ≠ rhs₂'.denote ctx := by
+  simp [simp_ac_cert]; intros; subst rhs₂ rhs₂'; simp_all
+
 noncomputable def superpose_ac_cert (a b c lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Seq) : Bool :=
   lhs₁.beq' (c.union_k a) |>.and'
   (lhs₂.beq' (c.union_k b)) |>.and'
@@ -505,6 +568,10 @@ theorem diseq_erase_dup {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_
       (lhs rhs lhs' rhs' : Seq) : eq_erase_dup_cert lhs rhs lhs' rhs' → lhs.denote ctx ≠ rhs.denote ctx → lhs'.denote ctx ≠ rhs'.denote ctx := by
   simp [eq_erase_dup_cert]; intro _ _; subst lhs' rhs'; simp
 
+theorem diseq_erase0 {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)}
+      (lhs rhs lhs' rhs' : Seq) : eq_erase0_cert lhs rhs lhs' rhs' → lhs.denote ctx ≠ rhs.denote ctx → lhs'.denote ctx ≠ rhs'.denote ctx := by
+  simp [eq_erase0_cert]; intro _ _; subst lhs' rhs'; simp
+
 noncomputable def diseq_unsat_cert (lhs rhs : Seq) : Bool :=
   lhs.beq' rhs
 
diff --git a/src/Lean/Meta/Tactic/Grind/AC/Eq.lean b/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
index ab762aa771..4b74056711 100644
--- a/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
@@ -91,18 +91,18 @@ local macro "gen_cnstr_fns " cnstr:ident : command =>
 
   private def $(mkId `simplifyLhsWithA) (c : $cnstr) (c' : EqCnstr) (r : AC.SubseqResult) : $cnstr :=
     match r with
-    | .exact    => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c c' }
-    | .prefix s => { c with lhs := c'.rhs ++ s, h := .simp_prefix (lhs := true) s c c' }
-    | .suffix s => { c with lhs := s ++ c'.rhs, h := .simp_suffix (lhs := true) s c c' }
-    | .middle p s => { c with lhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := true) p s c c' }
+    | .exact    => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c' c }
+    | .prefix s => { c with lhs := c'.rhs ++ s, h := .simp_prefix (lhs := true) s c' c }
+    | .suffix s => { c with lhs := s ++ c'.rhs, h := .simp_suffix (lhs := true) s c' c }
+    | .middle p s => { c with lhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := true) p s c' c }
     | .false => c
 
   private def $(mkId `simplifyRhsWithA) (c : $cnstr) (c' : EqCnstr) (r : AC.SubseqResult) : $cnstr :=
     match r with
-    | .exact    => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c c' }
-    | .prefix s => { c with rhs := c'.rhs ++ s, h := .simp_prefix (lhs := false) s c c' }
-    | .suffix s => { c with rhs := s ++ c'.rhs, h := .simp_suffix (lhs := false) s c c' }
-    | .middle p s => { c with rhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := false) p s c c' }
+    | .exact    => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c' c }
+    | .prefix s => { c with rhs := c'.rhs ++ s, h := .simp_prefix (lhs := false) s c' c }
+    | .suffix s => { c with rhs := s ++ c'.rhs, h := .simp_suffix (lhs := false) s c' c }
+    | .middle p s => { c with rhs := p ++ c'.rhs ++ s, h := .simp_middle (lhs := false) p s c' c }
     | .false => c
 
   /-- Simplifies `c` using the basis when `(← isCommutative)` is `false` -/
@@ -135,14 +135,14 @@ local macro "gen_cnstr_fns " cnstr:ident : command =>
 
   private def $(mkId `simplifyLhsWithAC) (c : $cnstr) (c' : EqCnstr) (r : AC.SubsetResult) : $cnstr :=
     match r with
-    | .exact    => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c c' }
-    | .strict s => { c with lhs := c'.rhs.union s, h := .simp_ac (lhs := true) s c c' }
+    | .exact    => { c with lhs := c'.rhs, h := .simp_exact (lhs := true) c' c }
+    | .strict s => { c with lhs := c'.rhs.union s, h := .simp_ac (lhs := true) s c' c }
     | .false => c
 
   private def $(mkId `simplifyRhsWithAC) (c : $cnstr) (c' : EqCnstr) (r : AC.SubsetResult) : $cnstr :=
     match r with
-    | .exact    => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c c' }
-    | .strict s => { c with rhs := c'.rhs.union s, h := .simp_ac (lhs := false) s c c' }
+    | .exact    => { c with rhs := c'.rhs, h := .simp_exact (lhs := false) c' c }
+    | .strict s => { c with rhs := c'.rhs.union s, h := .simp_ac (lhs := false) s c' c }
     | .false => c
 
   /--
@@ -196,7 +196,7 @@ def saveDiseq (c : DiseqCnstr) : ACM Unit := do
 
 def DiseqCnstr.assert (c : DiseqCnstr) : ACM Unit := do
   let c ← c.eraseDup
-  -- let c ← c.simplify -- TODO: uncomment after implementing proof generation
+  let c ← c.simplify
   trace[grind.ac.assert] "{← c.denoteExpr}"
   if c.lhs == c.rhs then
     c.setUnsat
@@ -306,8 +306,11 @@ private def getNext? : ACM (Option EqCnstr) := do
   return some c
 
 private def checkDiseqs : ACM Unit := do
-  -- TODO
-  return ()
+  let diseqs := (← getStruct).diseqs
+  modifyStruct fun s => { s with diseqs := {} }
+  for c in diseqs do
+    c.assert
+    if (← isInconsistent) then return
 
 private def propagateEqs : ACM Unit := do
   -- TODO
diff --git a/src/Lean/Meta/Tactic/Grind/AC/Proof.lean b/src/Lean/Meta/Tactic/Grind/AC/Proof.lean
index b325eee223..f34cd281cc 100644
--- a/src/Lean/Meta/Tactic/Grind/AC/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Proof.lean
@@ -121,6 +121,51 @@ where
   go : ProofM Expr := do
     mkContext (← x)
 
+partial def EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr := do caching c do
+  match c.h with
+  | .core a b lhs rhs =>
+    let h ← match (← isCommutative), (← hasNeutral) with
+      | false, false => mkAPrefix ``AC.eq_norm_a
+      | false, true  => mkAIPrefix ``AC.eq_norm_ai
+      | true,  false => mkACPrefix ``AC.eq_norm_ac
+      | true,  true  => mkACIPrefix ``AC.eq_norm_aci
+    return mkApp6 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← mkEqProof a b)
+  | .erase_dup c₁ =>
+    let h ← mkDupPrefix ``AC.eq_erase_dup
+    return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
+  | .erase0 c₁ =>
+    let h ← mkAIPrefix ``AC.eq_erase0
+    return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
+  | .simp_exact isLhs c₁ c₂ =>
+    let h ← mkPrefix <| if isLhs then ``AC.eq_simp_lhs_exact else ``AC.eq_simp_rhs_exact
+    let o := if isLhs then c₂.rhs else c₂.lhs
+    return mkApp5 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl o) (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_prefix isLhs tail c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_prefix else ``AC.eq_simp_rhs_prefix
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_suffix isLhs head c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_suffix else ``AC.eq_simp_rhs_suffix
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_middle isLhs head tail c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.eq_simp_lhs_middle else ``AC.eq_simp_rhs_middle
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp10 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_ac isLhs s c₁ c₂ =>
+    let h ← mkACPrefix <| if isLhs then ``AC.eq_simp_lhs_ac else ``AC.eq_simp_rhs_ac
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl s) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .swap c =>
+    let h ← mkPrefix ``AC.eq_orient
+    return mkApp3 h (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) (← c.toExprProof)
+  | .superpose_prefix .. => throwError "NIY"
+  | .superpose_ac .. => throwError "NIY"
+
 partial def DiseqCnstr.toExprProof (c : DiseqCnstr) : ProofM Expr := do caching c do
   match c.h with
   | .core a b lhs rhs =>
@@ -133,7 +178,33 @@ partial def DiseqCnstr.toExprProof (c : DiseqCnstr) : ProofM Expr := do caching
   | .erase_dup c₁ =>
     let h ← mkDupPrefix ``AC.diseq_erase_dup
     return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
-  | _ => throwError "NIY"
+  | .erase0 c₁ =>
+    let h ← mkAIPrefix ``AC.diseq_erase0
+    return mkApp6 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c.lhs) (← mkSeqDecl c.rhs) eagerReflBoolTrue (← c₁.toExprProof)
+  | .simp_exact isLhs c₁ c₂ =>
+    let h ← mkPrefix <| if isLhs then ``AC.diseq_simp_lhs_exact else ``AC.diseq_simp_rhs_exact
+    let o := if isLhs then c₂.rhs else c₂.lhs
+    return mkApp5 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl o) (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_prefix isLhs tail c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_prefix else ``AC.diseq_simp_rhs_prefix
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_suffix isLhs head c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_suffix else ``AC.diseq_simp_rhs_suffix
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_middle isLhs head tail c₁ c₂ =>
+    let h ← mkAPrefix <| if isLhs then ``AC.diseq_simp_lhs_middle else ``AC.diseq_simp_rhs_middle
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp10 h (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl head) (← mkSeqDecl tail) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .simp_ac isLhs s c₁ c₂ =>
+    let h ← mkACPrefix <| if isLhs then ``AC.diseq_simp_lhs_ac else ``AC.diseq_simp_rhs_ac
+    let s' := if isLhs then c.lhs else c.rhs
+    return mkApp9 h (← mkSeqDecl s) (← mkSeqDecl c₁.lhs) (← mkSeqDecl c₁.rhs) (← mkSeqDecl c₂.lhs) (← mkSeqDecl c₂.rhs) (← mkSeqDecl s')
+      eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
 def DiseqCnstr.setUnsat (c : DiseqCnstr) : ACM Unit := do
   let h ← withProofContext do
diff --git a/src/Lean/Meta/Tactic/Grind/AC/Types.lean b/src/Lean/Meta/Tactic/Grind/AC/Types.lean
index 6a0f85795b..a0771e89c1 100644
--- a/src/Lean/Meta/Tactic/Grind/AC/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Types.lean
@@ -61,11 +61,11 @@ inductive DiseqCnstrProof where
   | core (a b : Expr) (ea eb : AC.Expr)
   | erase_dup (c : DiseqCnstr)
   | erase0 (c : DiseqCnstr)
-  | simp_exact (lhs : Bool) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
-  | simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
-  | simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
-  | simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
-  | simp_middle (lhs : Bool) (s₁ s₂ : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
+  | simp_exact (lhs : Bool) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
+  | simp_middle (lhs : Bool) (s₁ s₂ : AC.Seq) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
 end
 
 structure Struct where
diff --git a/tests/lean/run/grind_ac_2.lean b/tests/lean/run/grind_ac_2.lean
new file mode 100644
index 0000000000..647b5fc98a
--- /dev/null
+++ b/tests/lean/run/grind_ac_2.lean
@@ -0,0 +1,44 @@
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
+    : op a (op b b) = c → op c c = op (op a b) (op b c) := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
+    : op a (op b b) = c → op (op a b) (op b c) = op c c := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
+    : op a (op b b) = c → op (op c a) (op b b) = op c c := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c : α)
+    : op a (op b b) = c → op c c = op (op c a) (op b b) := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : op a (op b b) = op c d → op c (op d c) = op (op a b) (op b c) := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : op a (op b b) = op c d → op (op a b) (op b c) = op (op c d) c := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : op a (op b b) = op c d → op c (op c (op d c)) = op (op c a) (op b (op b c)) := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] (a b c d : α)
+    : op a (op b b) = op c d → op (op c a) (op b (op b c)) = op c (op c (op d c))  := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d : α)
+    : op a (op b b) = op d c → op c (op d c) = op (op b a) (op b c) := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op] (a b c d : α)
+    : op a (op b b) = op d c → op (op b a) (op b c) = op c (op d c)  := by
+  grind only
+
+example {α : Sort u} (op : α → α → α) [Std.Associative op] [Std.Commutative op]
+    (one : α) [Std.LawfulIdentity op one] (a b c d : α)
+    : op a (op (op b one) b) = op d c → op (op b a) (op (op b one) c) = op (op c one) (op d c)  := by
+  grind only