awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : Mul M
inst_2 : Zero β
c : RingCon M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 0
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 0
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ (c : (a : M) → M → Prop) (f.sum h) (g.sum h')

Tactic:
c.toAddCon.finsuppSum h h' hf hf' H

Premises used: RingCon.toAddCon, AddCon.finsuppSum
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : Add M
inst_2 : CommMonoid M
inst_3 : (i : ι) → Zero (β i)
inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : RingCon 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')

Tactic:
c.toCon.dfinsuppProd h h' hf hf' H

Premises used: RingCon.toCon, Con.dfinsuppProd
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : Mul M
inst_3 : (i : ι) → Zero (β i)
inst_4 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : RingCon M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 0
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 0
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.sum (β := β) h) (g.sum (β := β) h')

Tactic:
c.toAddCon.dfinsuppSum h h' hf hf' H

Premises used: RingCon.toAddCon, AddCon.dfinsuppSum
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : Mul M
inst_3 : (i : ι) → AddCommMonoid (β i)
c : RingCon 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)

Tactic:
c.toAddCon.dfinsuppSumAddHom h h' H

Premises used: RingCon.toAddCon, AddCon.dfinsuppSumAddHom
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
mk :
  ∀ (toCon : Con R)
    (add' :
      ∀ {w x y z : R},
        (toCon.toSetoid : R → R → Prop) w x →
          (toCon.toSetoid : R → R → Prop) y z → (toCon.toSetoid : R → R → Prop) (w + y) (x + z)),
    Eq.{u_1 + 1} (α := Con R) ((fun (c : RingCon R) ↦ c.toCon) { toCon := toCon, add' := @add' })
        ((fun (c : RingCon R) ↦ c.toCon) d) →
      { toCon := toCon, add' := @add' : RingCon R } = d
⊢ Eq.{u_1 + 1} (α := Con R) ((fun (c : RingCon R) ↦ c.toCon) c) ((fun (c : RingCon R) ↦ c.toCon) d) → c = d

Tactic:
cases c
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
d : RingCon R
toCon : Con R
add' :
  ∀ {w x y z : R},
    (toCon.toSetoid : R → R → Prop) w x →
      (toCon.toSetoid : R → R → Prop) y z → (toCon.toSetoid : R → R → Prop) (w + y) (x + z)
⊢ Eq.{u_1 + 1} (α := Con R) ((fun (c : RingCon R) ↦ c.toCon) { toCon := toCon, add' := @add' })
      ((fun (c : RingCon R) ↦ c.toCon) d) →
    { toCon := toCon, add' := @add' : RingCon R } = d

Tactic:
congr!
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ c.toCon = d.toCon ↔ c = d

Tactic:
toCon_injective.eq_iff

Premises used: RingCon.toCon_injective, Function.Injective.eq_iff
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
s : Con R
h :
  ∀ {w x y z : R},
    (s.toSetoid : R → R → Prop) w x → (s.toSetoid : R → R → Prop) y z → (s.toSetoid : R → R → Prop) (w + y) (x + z)
⊢ Eq (α := (a : R) → R → Prop) (⇑{ toCon := s, add' := @h : RingCon R } : (a : R) → R → Prop) (⇑s : (a : R) → R → Prop)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ Eq (α := R → R → Prop) (⇑c.toSetoid : R → R → Prop) (⇑c : (a : R) → R → Prop)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ Eq (α := (a : R) → R → Prop) (⇑c.toCon : (a : R) → R → Prop) (⇑c : (a : R) → R → Prop)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x : R
⊢ (c : (a : R) → R → Prop) x x

Tactic:
c.refl' x

Premises used: RingCon.toCon, Setoid.refl', Con.toSetoid
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x y : R
⊢ (c : (a : R) → R → Prop) x y → (c : (a : R) → R → Prop) y x

Tactic:
c.symm'

Premises used: RingCon.toCon, Setoid.symm', Con.toSetoid
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x y z : R
⊢ (c : (a : R) → R → Prop) x y → (c : (a : R) → R → Prop) y z → (c : (a : R) → R → Prop) x z

Tactic:
c.trans'

Premises used: RingCon.toCon, Setoid.trans', Con.toSetoid
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
w x y z : R
⊢ (c : (a : R) → R → Prop) w x → (c : (a : R) → R → Prop) y z → (c : (a : R) → R → Prop) (w + y) (x + z)

Tactic:
c.add'

Premises used: RingCon.add'
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
w x y z : R
⊢ (c : (a : R) → R → Prop) w x → (c : (a : R) → R → Prop) y z → (c : (a : R) → R → Prop) (w * y) (x * z)

Tactic:
c.mul'

Premises used: RingCon.toCon, Con.mul'
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
S : Type u_2
inst : AddGroup S
inst_1 : Mul S
t : RingCon S
a b c d : S
h : (t : (a : S) → S → Prop) a b
h' : (t : (a : S) → S → Prop) c d
⊢ (t : (a : S) → S → Prop) (a - c) (b - d)

Tactic:
t.toAddCon.sub h h'

Premises used: RingCon.toAddCon, AddCon.sub
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
S : Type u_2
inst : AddGroup S
inst_1 : Mul S
t : RingCon S
a b : S
h : (t : (a : S) → S → Prop) a b
⊢ (t : (a : S) → S → Prop) (-a) (-b)

Tactic:
t.toAddCon.neg h

Premises used: RingCon.toAddCon, AddCon.neg
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
S : Type u_2
inst : AddMonoid S
inst_1 : Mul S
t : RingCon S
m : ℕ
x y : S
hx : (t : (a : S) → S → Prop) x y
⊢ (t : (a : S) → S → Prop) (m • x) (m • y)

Tactic:
t.toAddCon.nsmul m hx

Premises used: RingCon.toAddCon, AddCon.nsmul
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
S : Type u_2
inst : AddGroup S
inst_1 : Mul S
t : RingCon S
z : ℤ
x y : S
hx : (t : (a : S) → S → Prop) x y
⊢ (t : (a : S) → S → Prop) (z • x) (z • y)

Tactic:
t.toAddCon.zsmul z hx

Premises used: RingCon.toAddCon, AddCon.zsmul
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
s : Con R
h :
  ∀ {w x y z : R},
    (s.toSetoid : R → R → Prop) w x → (s.toSetoid : R → R → Prop) y z → (s.toSetoid : R → R → Prop) (w + y) (x + z)
a b : R
⊢ ({ toCon := s, add' := @h : RingCon R } : (a : R) → R → Prop) a b ↔ (s : (a : R) → R → Prop) a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
H : Eq (α := (a : R) → R → Prop) (⇑c : (a : R) → R → Prop) (⇑d : (a : R) → R → Prop)
⊢ c = d

Tactic:
DFunLike.coe_injective H

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
H h : ∀ (x x_1 : R), (c : (a : R) → R → Prop) x x_1 ↔ (d : (a : R) → R → Prop) x x_1
⊢ Eq (α := (a : R) → R → Prop) (⇑c : (a : R) → R → Prop) (⇑d : (a : R) → R → Prop)

Tactic:
ext
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
H : ∀ (x y : R), (c : (a : R) → R → Prop) x y ↔ (d : (a : R) → R → Prop) x y
x x_1 : R
⊢ (c : (a : R) → R → Prop) x x_1 ↔ (d : (a : R) → R → Prop) x x_1

Tactic:
apply H
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
H : c.toSetoid = d.toSetoid
⊢ c = d

Tactic:
ext <| Setoid.ext_iff.1 H

Premises used: RingCon.ext, Setoid.ext_iff, Iff.mp
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ Eq (α := (a : R) → R → Prop) (⇑c : (a : R) → R → Prop) (⇑d : (a : R) → R → Prop) ↔ c = d

Tactic:
simp
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_2
R' : Type u_3
F : Type u_4
inst : Add R
inst_1 : Add R'
inst_2 : FunLike F R R'
inst_3 : AddHomClass F R R'
inst_4 : Mul R
inst_5 : Mul R'
inst_6 : MulHomClass F R R'
J : RingCon R'
f : F
x y : R
⊢ (J.comap f : (a : R) → R → Prop) x y ↔ (J : (a : R') → R' → Prop) ((f : (a : R) → R') x : R') ((f : (a : R) → R') y)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x : R
⊢ Eq (α := Quot (α := R) (⇑c : (a : R) → R → Prop)) (Quot.mk (⇑c : (a : R) → R → Prop) x) (↑x : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
a b : R
⊢ Eq (α := c.Quotient) (↑a : c.Quotient) (↑b : c.Quotient) ↔ (c : (a : R) → R → Prop) a b

Tactic:
Quotient.eq''

Premises used: Quotient.eq'', RingCon.toQuotient, RingCon.Quotient
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x y : R
⊢ (↑(x + y) : c.Quotient) = HAdd.hAdd (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quotient.map₂, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x y : R
⊢ (↑(x * y) : c.Quotient) = HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quotient.map₂, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddZeroClass R
inst_1 : Mul R
c : RingCon R
⊢ Eq.{u_1 + 1} (α := c.Quotient) (↑0 : c.Quotient) 0

Tactic:
rfl

Premises used: RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : MulOneClass R
c : RingCon R
⊢ Eq.{u_1 + 1} (α := c.Quotient) (↑1 : c.Quotient) 1

Tactic:
rfl

Premises used: RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Mul R
c : RingCon R
x : R
⊢ Eq (α := c.Quotient) (↑(-x) : c.Quotient) (-(↑x : c.Quotient))

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Mul R
c : RingCon R
x y : R
⊢ (↑(x - y) : c.Quotient) = HSub.hSub (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quotient.map₂, rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Mul R
c : RingCon R
z : ℤ
x : R
⊢ (↑(z • x) : c.Quotient) = HSMul.hSMul (β := c.Quotient) z (↑x : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
c : RingCon R
n : ℕ
x : R
⊢ (↑(n • x) : c.Quotient) = HSMul.hSMul (β := c.Quotient) n (↑x : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : Add R
inst_1 : Monoid R
c : RingCon R
x : R
n : ℕ
⊢ (↑(x ^ n) : c.Quotient) = HPow.hPow (α := c.Quotient) (↑x : c.Quotient) n

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : Mul R
c : RingCon R
n : ℕ
⊢ Eq.{u_1 + 1} (α := c.Quotient) (↑(↑n : R) : c.Quotient) (↑n : c.Quotient)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : AddGroupWithOne R
inst_1 : Mul R
c : RingCon R
n : ℕ
⊢ Eq.{u_1 + 1} (α := c.Quotient) (↑(↑n : R) : c.Quotient) (↑n : c.Quotient)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
c : RingCon R
⊢ Surjective (α := R) (β := c.Quotient) (⇑c.mk' : (a : R) → c.Quotient)

Tactic:
Quotient.mk''_surjective

Premises used: RingCon.toQuotient, RingCon.Quotient, Quotient.mk''_surjective
-- Module: Mathlib.RingTheory.Congruence.Defs
Goal:
R : Type u_1
inst : NonAssocSemiring R
c : RingCon R
⊢ Eq (α := (a : R) → c.Quotient) (⇑c.mk' : (a : R) → c.Quotient) toQuotient

Tactic:
rfl

Premises used: RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
f : M →+* N
⊢ comap ⊥ f = ker f

Tactic:
rfl

Premises used: RingCon.ker, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
f : M →+* N
x y : M
⊢ (ker f : (a : M) → M → Prop) x y ↔ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c : RingCon M
⊢ ker c.mk' = c

Tactic:
ext fun _ _ => Quotient.eq''

Premises used: Quotient.eq'', RingCon.ext
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
f : M →+* N
g : N →+* P
x y : M
⊢ (ker (g.comp f) : (a : M) → M → Prop) x y ↔ ((ker g).comap f : (a : M) → M → Prop) x y

Tactic:
simp [ker_apply, comap_rel]

Premises used: RingCon.ker_apply, RingCon.comap_rel
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
g : N →+* M
rw : Eq (α := RingCon N) (c.comap g) ((ker c.mk').comap g)
rw₁ rw₂ : Eq (α := RingCon N) (c.comap g) (c.comap g)
⊢ c.comap g = ker (c.mk'.comp g)

Tactic:
rw [ker_comp, ker_mk'_eq]

Premises used: RingCon.ker_comp, RingCon.ker_mk'_eq
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
⊢ ∀ (a₁ a₂ : M),
    (c.toSetoid : M → M → Prop) a₁ a₂ ↔
      (d.toSetoid : M → M → Prop) ((Equiv.refl M : (a : M) → M) a₁ : M) ((Equiv.refl M : (a : M) → M) a₂ : M)

Tactic:
apply RingCon.ext_iff.mp h

Premises used: RingCon.ext_iff, Iff.mp
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
mk :
  ∀ (a : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
        (Quotient.congr (Equiv.refl M) ⋯).toFun y
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x * (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
a : M
mk :
  ∀ (a_1 : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun
        (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
          (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
        (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a * y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases y with ⟨⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
a a_1 : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun
      (HMul.hMul (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) *
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
mk :
  ∀ (a : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a + y) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
        (Quotient.congr (Equiv.refl M) ⋯).toFun y
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (x + y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun x + (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
a : M
mk :
  ∀ (a_1 : M),
    (Quotient.congr (Equiv.refl M) ⋯).toFun
        (HAdd.hAdd (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
          (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
        (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a + y) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
      (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rcases y with ⟨⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
inst_2 : NonAssocSemiring P
c d : RingCon M
h : c = d
x y : c.Quotient
a a_1 : M
⊢ (Quotient.congr (Equiv.refl M) ⋯).toFun
      (HAdd.hAdd (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) a)
        (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)) =
    (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a) +
      (Quotient.congr (Equiv.refl M) ⋯).toFun (Quot.mk (⇑c.toSetoid : M → M → Prop) a_1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c d : RingCon M
h : c = d
a : M
⊢ Eq (α := d.Quotient) ((RingCon.congr h : (a : c.Quotient) → d.Quotient) (↑a : c.Quotient) : d.Quotient)
    ((↑a : d.Quotient) : d.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Eq.{u_2 + 1} (α := (a : N) → N → Prop)
    (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))

Tactic:
le_antisymm ?_ <| (RingCon.gi N).gc.le_u_l _

Premises used: RingCon.gi, GaloisConnection.le_u_l, le_antisymm, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
refine :
  LE.le.{u_2} (α := (a : N) → N → Prop) (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))
⊢ Eq.{u_2 + 1} (α := (a : N) → N → Prop)
    (⇑(mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N)) : (a : N) → N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N))

Tactic:
refine le_antisymm ?_ <| (RingCon.gi N).gc.le_u_l _

Premises used: RingCon.gi, GaloisConnection.le_u_l, le_antisymm, GaloisInsertion.gc
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))

Tactic:
have := Relation.map_equivalence c.toSetoid.2 _ hf h
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i : N
_ :
  ∀ (i_1 : N),
    (mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i i_1 ≤
      Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i i_1
⊢ LE.le (α := (fun (a : N) ↦ N → Prop) i)
    ((mapGen.{u_1, u_2} (M := M) (c := c) (⇑f : (a : M) → N) : (a : N) → N → Prop) i : N → Prop)
    (Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) i : N → Prop)

Tactic:
_
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i i_1 x y : N
a : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y

Tactic:
a
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i i_1 x y : N
a : Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x y

Tactic:
exact a
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
this :
  Equivalence.{u_2 + 1} (α := N)
    (Relation.Map.{u_1 + 1, u_1 + 1, u_2 + 1, u_2 + 1} (α := M) (⇑c.toSetoid : M → M → Prop) (⇑f : (a : M) → N)
      (⇑f : (a : M) → N))
i i_1 x : N
⊢ Relation.Map (α := M) (β := M) (⇑c : (a : M) → M → Prop) (⇑f : (a : M) → N) (⇑f : (a : M) → N) x x

Tactic:
this.refl x

Premises used: Equivalence.refl