awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y_1 : M
f_1 f : M →* P
x y : Con.Quotient (ker f)
a : M
h :
  Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
        (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
      ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) y :
      ↥(MonoidHom.mrange (kerLift f)))
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) y : P)
have mk : ∀ (a_1 : M)
  (h :
    Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
      (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
          (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
        ↥(MonoidHom.mrange (kerLift f)))
      (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
          (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) :
        ↥(MonoidHom.mrange (kerLift f)))),
  Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) : P)
Tactic: rcases y with ⟨⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x y : M
f_1 f : M →* P
x_1 : ↥(MonoidHom.mrange (kerLift f))
w : P
z : Con.Quotient (ker f)
hz : (kerLift f : (a : (ker f).Quotient) → P) z = w
⊢ Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) z :
      ↥(MonoidHom.mrange (kerLift f)))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (MonoidHom.mrange (kerLift f)) x) w ⋯ :
      ↥(MonoidHom.mrange (kerLift f)))
have rcases : Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
  (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) z :
    ↥(MonoidHom.mrange (kerLift f)))
  (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (MonoidHom.mrange (kerLift f)) x)
      ((kerLift f : (a : (ker f).Quotient) → P) z) sorry :
    ↥(MonoidHom.mrange (kerLift f)))
Tactic: rcases hz with ⟨⟩
Cleared hypotheses: w, hz
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : Con.Quotient (ker f)
⊢ Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
have rw : Eq.{u_3 + 1} (α := P)
  ((kerLift f : (a : (ker f).Quotient) → P) (↑(g ((kerLift f : (a : (ker f).Quotient) → P) x)) : (ker f).Quotient) : P)
  ((kerLift f : (a : (ker f).Quotient) → P) x : P)
Tactic: rw [Function.comp_apply, kerLift_mk, hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : Con.Quotient (ker f)
rw :
  Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) (↑(g ((kerLift f : (a : (ker f).Quotient) → P) x)) : (ker f).Quotient) :
      P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
have rw₁ : Eq.{u_3 + 1} (α := P) ((f : (a : M) → P) (g ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
  ((kerLift f : (a : (ker f).Quotient) → P) x : P)
Tactic: rw [Function.comp_apply, kerLift_mk, hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : Con.Quotient (ker f)
rw :
  Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) (↑(g ((kerLift f : (a : (ker f).Quotient) → P) x)) : (ker f).Quotient) :
      P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
rw₁ :
  Eq.{u_3 + 1} (α := P) ((f : (a : M) → P) (g ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
have rw₂ : Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) x : P) ((kerLift f : (a : (ker f).Quotient) → P) x : P)
Tactic: rw [Function.comp_apply, kerLift_mk, hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : P
| x
have rw : ((f : (a : M) → P) (g x) : P)
Tactic: rw [← hf x]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : P
⊢ (kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) x) = x
have conv_rhs : Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) x) : P) ((f : (a : M) → P) (g x) : P)
Tactic: conv_rhs => rw [← hf x]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih :
  ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)
⊢ (c : (a : M) → M → Prop) (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod
have cons : (c : (a : M) → M → Prop) (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)
Tactic: rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
l : List ι
f g : ι → M
h : ∀ x ∈ l, (c : (a : M) → M → Prop) (f x) (g x)
⊢ (c : (a : M) → M → Prop) (List.map f l).prod (List.map g l).prod
have nil : ∀ (h : ∀ (x : ι), Membership.mem (γ := List ι) [] x → (c : (a : M) → M → Prop) (f x) (g x)),
  (c : (a : M) → M → Prop) (List.map f []).prod (List.map g []).prod
Tactic: induction l with
  | nil =>
    simpa only [List.map_nil, List.prod_nil] using c.refl 1
  | cons x xs ih =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
    exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
l : List ι
f g : ι → M
h : ∀ x ∈ l, (c : (a : M) → M → Prop) (f x) (g x)
nil :
  ∀ (h : ∀ (x : ι), Membership.mem (γ := List ι) [] x → (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f []).prod (List.map g []).prod
⊢ (c : (a : M) → M → Prop) (List.map f l).prod (List.map g l).prod
have cons : ∀ (x : ι) (xs : List ι)
  (ih :
    ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
      (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod)
  (h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)),
  (c : (a : M) → M → Prop) (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod
Tactic: induction l with
  | nil =>
    simpa only [List.map_nil, List.prod_nil] using c.refl 1
  | cons x xs ih =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
    exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
h : ∀ x ∈ s, (c : (a : M) → M → Prop) (f x) (g x)
⊢ (c : (a : M) → M → Prop) (Multiset.map f s).prod (Multiset.map g s).prod
have mk : ∀ (a : List ι)
  (h :
    ∀ (x : ι),
      Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a) x →
        (c : (a : M) → M → Prop) (f x) (g x)),
  (c : (a : M) → M → Prop) (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod
    (Multiset.map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod
Tactic: rcases s
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ (c : (a : M) → M → Prop) (f.prod h) (g.prod h')
have refine : Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod h) : c.Quotient)
  ((c.mk' : (a : M) → c.Quotient) (g.prod h') : c.Quotient)
Tactic: refine Quotient.exact (show c.mk' _ = c.mk' _ from ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod h') : c.Quotient)
have rw : Eq.{u_3 + 1} (α := c.Quotient) (f.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
  (g.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))
Tactic: rw [map_finsuppProd, map_finsuppProd]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ (c : (a : M) → M → Prop) (f.prod (β := β) h) (g.prod (β := β) h')
have refine : Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod (β := β) h) : c.Quotient)
  ((c.mk' : (a : M) → c.Quotient) (g.prod (β := β) h') : c.Quotient)
Tactic: refine Quotient.exact (show c.mk' _ = c.mk' _ from ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod (β := β) h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod (β := β) h') : c.Quotient)
have rw : Eq.{u_3 + 1} (α := c.Quotient) (f.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
  (g.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))
Tactic: rw [map_dfinsuppProd, map_dfinsuppProd]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → AddMonoidHom.{u_2, u_3} (β i) M
f g : Π₀ (i : ι), β i
H :
  ∀ (i : ι),
    (c : (a : M) → M → Prop) ((h i : (a : β i) → M) ((f : (a : ι) → β a) i) : M)
      ((h' i : (a : β i) → M) ((g : (a : ι) → β a) i))
⊢ (c : (a : M) → M → Prop) ((DFinsupp.sumAddHom (β := β) h : (a : Π₀ (i : ι), β i) → M) f : M)
    ((DFinsupp.sumAddHom (β := β) h' : (a : Π₀ (i : ι), β i) → M) g)
have simp_rw : (c : (a : M) → M → Prop) (f.sum (β := β) fun (x : ι) ↦ (⇑(h x) : (a : β x) → M))
  (g.sum (β := β) fun (x : ι) ↦ (⇑(h' x) : (a : β x) → M))
Tactic: simp_rw [DFinsupp.sumAddHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.BigOperators (goal)
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → AddMonoidHom.{u_2, u_3} (β i) M
f g : Π₀ (i : ι), β i
H :
  ∀ (i : ι),
    (c : (a : M) → M → Prop) ((h i : (a : β i) → M) ((f : (a : ι) → β a) i) : M)
      ((h' i : (a : β i) → M) ((g : (a : ι) → β a) i))
⊢ (c : (a : M) → M → Prop) ((DFinsupp.sumAddHom (β := β) h : (a : Π₀ (i : ι), β i) → M) f : M)
    ((DFinsupp.sumAddHom (β := β) h' : (a : Π₀ (i : ι), β i) → M) g)
have simp_rw : (c : (a : M) → M → Prop) (f.sum (β := β) fun (x : ι) ↦ (⇑(h x) : (a : β x) → M))
  (g.sum (β := β) fun (x : ι) ↦ (⇑(h' x) : (a : β x) → M))
Tactic: classical
  simp_rw [DFinsupp.sumAddHom_apply]
  exact c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ c.toSetoid = d.toSetoid → c = d
have mk : ∀ (toSetoid : Setoid M)
  (mul' :
    ∀ {w x y z : M},
      (toSetoid : M → M → Prop) w x → (toSetoid : M → M → Prop) y z → (toSetoid : M → M → Prop) (w * y) (x * z)),
  { toSetoid := toSetoid, mul' := @mul' : Con M }.toSetoid = d.toSetoid →
    { toSetoid := toSetoid, mul' := @mul' : Con M } = d
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d x y : Con M
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop) ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) x)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)
⊢ x = y
have rcases : ∀ (x : M → M → Prop) (iseqv : Equivalence x)
  (mul' :
    ∀ {w x_1 y z : M},
      ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
        ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z))
  (h :
    Eq.{u_1 + 1} (α := (a : M) → M → Prop)
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)),
  { r := x, iseqv := iseqv, mul' := @mul' : Con M } = y
Tactic: rcases x with ⟨⟨x, _⟩, _⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d y : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)
⊢ { r := x, iseqv := iseqv, mul' := @mul' : Con M } = y
have rcases : ∀ (y : M → M → Prop) (iseqv_1 : Equivalence y)
  (mul'_1 :
    ∀ {w x y_1 z : M},
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
          ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z))
  (h :
    Eq.{u_1 + 1} (α := (a : M) → M → Prop)
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop))
        { r := y, iseqv := iseqv_1, mul' := @mul'_1 })),
  { r := x, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
Tactic: rcases y with ⟨⟨y, _⟩, _⟩
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (hypothesis)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
y : M → M → Prop
iseqv_1 : Equivalence y
mul'_1 :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv_1, mul' := @mul'_1 })
⊢ { r := x, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
have this : x = y
Tactic: have : x = y := h
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
y : M → M → Prop
iseqv_1 : Equivalence y
mul'_1 :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv_1, mul' := @mul'_1 })
this : x = y
⊢ { r := x, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
have subst : ∀ (iseqv : Equivalence y)
  (mul' :
    ∀ {w x y_1 z : M},
      ({ r := y, iseqv := iseqv } : M → M → Prop) w x →
        ({ r := y, iseqv := iseqv } : M → M → Prop) y_1 z →
          ({ r := y, iseqv := iseqv } : M → M → Prop) (w * y_1) (x * z))
  (h :
    Eq.{u_1 + 1} (α := (a : M) → M → Prop)
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv, mul' := @mul' })
      ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop))
        { r := y, iseqv := iseqv_1, mul' := @mul'_1 })),
  { r := y, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
Tactic: subst x
Cleared hypotheses: x, iseqv, mul', h, this
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x y : M
h : ((sInf S).toSetoid : M → M → Prop) x y
r : Setoid M
h_1 : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ (r : M → M → Prop) x y
have rw : (c.toSetoid : M → M → Prop) x y
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
⊢ Eq (α := (a : M) → M → Prop) (⇑(sInf S) : (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S))
have h : ∀ (x x_1 : M), (sInf S : (a : M) → M → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x x_1 : M
⊢ (sInf S : (a : M) → M → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S) x x_1
have h : (sInf S : (a : M) → M → Prop) x x_1 ↔ ∀ (i : Con M) (i_1 : i ∈ S), (i : (a : M) → M → Prop) x x_1
Tactic: simp only [sInf_image, iInf_apply, iInf_Prop_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
have rw : Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
rw :
  Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
have rw₁ : Eq (α := (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' Set.range f))
  (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
rw :
  Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₁ :
  Eq (α := (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
have rw₂ : Eq (α := (a : M) → M → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f)))
  (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Congruence.Defs (goal)
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
rw :
  Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₁ :
  Eq (α := (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₂ :
  Eq (α := (a : M) → M → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
have rw₃ : Eq (α := (a : M) → M → Prop) (iInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f))
  (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]