awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 d_1 c : RingCon M
d : RingCon c.Quotient
y : c.Quotient
x : M
H :
  ∀ (y : M),
    (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
        ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
      (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
        ((c.mk' : (a : M) → c.Quotient) y)
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) y

Tactic:
obtain ⟨y, rfl⟩ := c.mk'_surjective y

Premises used: RingCon.mk'_surjective, 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_1 d_1 c : RingCon M
d : RingCon c.Quotient
x y : M
H :
  (d.comap c.mk' : (a : M) → M → Prop) x y ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
H₁ H₂ :
  (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y) ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)
⊢ (mapGen (M := M) (c := d.comap c.mk') (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
      ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) y) ↔
    (d : (a : c.Quotient) → c.Quotient → Prop) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) y)

Tactic:
rw [mapGen_apply_apply_of_surjective _ (comap_bot c.mk' ▸ comap_mono bot_le) c.mk'_surjective,
      comap_rel]

Premises used: RingCon.mapGen_apply_apply_of_surjective, RingCon.comap_rel, RingCon.mk'_surjective
-- 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_1 d c : RingCon M
s t : (↑(Set.Ici c) : Type u_1)
simp :
  (∀ (x x_1 : M),
      (mapGen (M := M) (c := (↑s : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1) →
        (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
    ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y
⊢ LE.le (α := RingCon c.Quotient)
      (({
              toFun := fun (d : (↑(Set.Ici c) : Type u_1)) ↦
                mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient),
              invFun := fun (d : RingCon c.Quotient) ↦
                Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Ici c) : Type u_1)) → RingCon c.Quotient)
          s :
        RingCon c.Quotient)
      (({
              toFun := fun (d : (↑(Set.Ici c) : Type u_1)) ↦
                mapGen (M := M) (c := (↑d : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient),
              invFun := fun (d : RingCon c.Quotient) ↦
                Subtype.mk (p := fun (x : RingCon M) ↦ x ∈ Set.Ici c) (d.comap c.mk') ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : (↑(Set.Ici c) : Type u_1)) → RingCon c.Quotient)
          t :
        RingCon c.Quotient) ↔
    s ≤ t

Tactic:
simp only [Equiv.coe_fn_mk, le_def, c.mk'_surjective.forall, ← Subtype.coe_le_coe]

Premises used: Function.Surjective.forall, RingCon.mk'_surjective, Subtype.coe_le_coe, RingCon.le_def, Equiv.coe_fn_mk
-- 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_1 d c : RingCon M
s t : (↑(Set.Ici c) : Type u_1)
simp_rw :
  (∀ (x x_1 : M),
      ((↑s : RingCon M) : (a : M) → M → Prop) x x_1 →
        (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
    ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y
⊢ (∀ (x x_1 : M),
      (mapGen (M := M) (c := (↑s : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1) →
        (mapGen (M := M) (c := (↑t : RingCon M)) (⇑c.mk' : (a : M) → c.Quotient) : (a : c.Quotient) → c.Quotient → Prop)
          ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) ((c.mk' : (a : M) → c.Quotient) x_1)) ↔
    ∀ {x y : M}, ((↑s : RingCon M) : (a : M) → M → Prop) x y → ((↑t : RingCon M) : (a : M) → M → Prop) x y

Tactic:
simp_rw [mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le s.2) c.mk'_surjective,
      mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le t.2) c.mk'_surjective]

Premises used: RingCon.mapGen_apply_apply_of_surjective, RingCon.mk'_surjective, RingCon.mk', Eq.trans_le, RingCon.ker_mk'_eq, Subtype.property
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
x : M
⊢ Eq.{u_3 + 1} (α := P) ((c.lift f H : (a : c.Quotient) → P) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) : P)
    ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
x : M
⊢ Eq.{u_3 + 1} (α := P) ((c.lift f H : (a : c.Quotient) → P) (↑x : c.Quotient) : P) ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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_1 d c : RingCon M
x_1 y_1 : M
f_1 : M →+* P
f : RingHom.{u_1, u_3} c.Quotient P
x y : M
h : (c : (a : M) → M → Prop) x y
rw rw₁ :
  Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
    ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑x : c.Quotient) : P)
    ((f : (a : c.Quotient) → P) (↑y : c.Quotient) : P)

Tactic:
rw [c.eq.2 h]

Premises used: Iff.mpr, RingCon.eq
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : RingHom.{u_1, u_3} c.Quotient P
a :
  ∀ (x : c.Quotient),
    Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)
⊢ c.lift (f.comp c.mk') ⋯ = f

Tactic:
ext x
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : RingHom.{u_1, u_3} c.Quotient P
x : c.Quotient
a :
  ∀ (a : M),
    Eq.{u_3 + 1} (α := P)
      ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
      ((f : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
⊢ Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) x : P) ((f : (a : c.Quotient) → P) x : P)

Tactic:
rcases x with ⟨⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : RingHom.{u_1, u_3} c.Quotient P
x : c.Quotient
a : M
⊢ Eq.{u_3 + 1} (α := P) ((c.lift (f.comp c.mk') ⋯ : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)
    ((f : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) a) : P)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f g : RingHom.{u_1, u_3} c.Quotient P
h : f.comp c.mk' = g.comp c.mk'
x : M
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) : P)
    ((g : (a : c.Quotient) → P) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) : P)

Tactic:
congr($h x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f g : RingHom.{u_1, u_3} c.Quotient P
h : f.comp c.mk' = g.comp c.mk'
x : M
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) : P)
    ((g : (a : c.Quotient) → P) ((c.mk' : (a : M) → c.Quotient) x : c.Quotient) : P)

Tactic:
exact congr($h x)
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
g : RingHom.{u_1, u_3} c.Quotient P
Hg : g.comp c.mk' = f
⊢ g.comp c.mk' = (c.lift f H).comp c.mk'

Tactic:
aesop
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔
    Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)

Tactic:
⟨fun H ↦ (Quot.surjective_lift fun x x_1 h_1 ↦ h h_1).mp H,
    fun H ↦ AddCon.lift_surjective_of_surjective h H⟩

Premises used: Quot.surjective_lift, Iff.intro, AddCon.lift_surjective_of_surjective, Iff.mp
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔
    Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)

Tactic:
refine ⟨fun H ↦ (Quot.surjective_lift fun x x_1 h_1 ↦ h h_1).mp H,
    fun H ↦ AddCon.lift_surjective_of_surjective h H⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
hf : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ Surjective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P)

Tactic:
lift_surjective_iff.mpr hf

Premises used: Iff.mpr, RingCon.lift_surjective_iff
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔ c = ker f

Tactic:
⟨fun H ↦ ext'' (Setoid.ker_eq_lift_of_injective f h H).symm, ?_⟩

Premises used: RingCon.ext'', Iff.intro, Eq.symm, Setoid.ker_eq_lift_of_injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
refine : c = ker f → Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P)
⊢ Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔ c = ker f

Tactic:
refine ⟨fun H ↦ ext'' (Setoid.ker_eq_lift_of_injective f h H).symm, ?_⟩
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
H : c = ker f
a₁ : c.Quotient
x : M
a₂ : c.Quotient
y : M
⊢ Eq.{u_3 + 1} (α := P) ((c.lift f h : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) : P)
      ((c.lift f h : (a : c.Quotient) → P) (Quot.mk (⇑c.toSetoid : M → M → Prop) y) : P) →
    Eq (α := c.Quotient) (Quot.mk (⇑c.toSetoid : M → M → Prop) x) (Quot.mk (⇑c.toSetoid : M → M → Prop) y)

Tactic:
simp [H]
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
h : c ≤ ker f
⊢ Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ∧
      Surjective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f h) : (a : c.Quotient) → P) ↔
    c = ker f ∧ Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)

Tactic:
simp only [lift_injective_iff, lift_surjective_iff]

Premises used: RingCon.lift_surjective_iff, RingCon.lift_injective_iff
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
h : Injective.{u_1 + 1, u_3 + 1} (α := c.Quotient) (β := P) (⇑(c.lift f H) : (a : c.Quotient) → P)
⊢ ker f = c

Tactic:
(lift_injective_iff.mp h).symm

Premises used: Iff.mp, Eq.symm, RingCon.lift_injective_iff
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
x : M
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (↑x : (ker f).Quotient) : P) ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
⊢ Injective.{u_1 + 1, u_3 + 1} (α := (ker f).Quotient) (β := P) (⇑(kerLift f) : (a : (ker f).Quotient) → P)

Tactic:
AddCon.kerLift_injective (f : M →+ P)

Premises used: Quotient.liftOn', AddMonoidHomClass.toAddMonoidHom, AddCon.liftOn, RingCon.Quotient, AddCon.kerLift_injective, AddCon.ker
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c d : RingCon M
h : c ≤ d
x : c.Quotient
⊢ Eq (α := d.Quotient) ((c.map d h : (a : c.Quotient) → d.Quotient) x : d.Quotient)
    ((c.lift d.mk' ⋯ : (a : c.Quotient) → d.Quotient) x : d.Quotient)

Tactic:
rfl

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

Tactic:
RingHom.rangeS_eq_top.mpr (mk'_surjective _)

Premises used: Iff.mpr, RingHom.rangeS_eq_top, RingCon.mk'_surjective
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
⊢ (c.lift f H).rangeS = f.rangeS

Tactic:
SetLike.coe_injective <| Set.range_quot_lift _

Premises used: Set.range_quot_lift, SetLike.coe_injective
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
⊢ (kerLift f).rangeS = f.rangeS

Tactic:
rangeS_lift fun _ _ => id

Premises used: RingCon.kerLift, id, RingCon.rangeS_lift
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
x : M
⊢ Eq.{u_3 + 1} (α := P)
    ((↑((quotientKerEquivRangeS f : (a : (ker f).Quotient) → ↥f.rangeS) (↑x : (ker f).Quotient)) : P) : P)
    ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : (ker f).Quotient
⊢ Eq.{u_3 + 1} (α := P) ((quotientKerEquivOfRightInverse f g hf : (a : (ker f).Quotient) → P) x : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : NonAssocSemiring M
inst_1 : NonAssocSemiring P
f : M →+* P
hf : Surjective.{u_1 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
x : M
⊢ Eq.{u_3 + 1} (α := P) ((quotientKerEquivOfSurjective f hf : (a : (ker f).Quotient) → P) (↑x : (ker f).Quotient) : P)
    ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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 : N →+* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_1 + 1} (α := c.Quotient)
    ((c.comapQuotientEquivOfSurj f hf hcd : (a : d.Quotient) → c.Quotient) (↑x : d.Quotient) : c.Quotient)
    ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, 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 : N →+* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
d : RingCon N
hcd : d = c.comap f
x : N
rw :
  Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
        ((c.comapQuotientEquivOfSurj f hf hcd : (a : d.Quotient) → c.Quotient) (↑x : d.Quotient)) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)
rw₁ rw₂ : Eq (α := d.Quotient) (↑x : d.Quotient) (↑x : d.Quotient)
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivOfSurj f hf hcd).symm : (a : c.Quotient) → d.Quotient)
        (↑((f : (a : N) → M) x) : c.Quotient) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
rw [← c.comapQuotientEquivOfSurj_mk hf hcd x, RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply, RingCon.comapQuotientEquivOfSurj_mk
-- 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 : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((RingEquiv.symm (c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd) : RingEquiv.{u_1, u_2} c.Quotient d.Quotient) :
          (a : c.Quotient) → d.Quotient)
        (((c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd : RingEquiv.{u_2, u_1} d.Quotient c.Quotient) :
            (a : d.Quotient) → c.Quotient)
          (↑x : d.Quotient)) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
RingEquiv.symm_apply_apply _ _

Premises used: RingEquiv.symm_apply_apply
-- 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 : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
h :
  ⟦(f : (a : N) → M) x⟧ =
    ((c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd : RingEquiv.{u_2, u_1} d.Quotient c.Quotient) :
        (a : d.Quotient) → c.Quotient)
      (↑x : d.Quotient)
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((RingEquiv.symm (c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd) : RingEquiv.{u_1, u_2} c.Quotient d.Quotient) :
          (a : c.Quotient) → d.Quotient)
        ⟦(f : (a : N) → M) x⟧ :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
convert! RingEquiv.symm_apply_apply _ _

Premises used: RingEquiv.symm_apply_apply
-- 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 : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
h : ⟦(f : (a : N) → M) x⟧ = (↑((f : (a : N) → M) x) : c.Quotient)
⊢ ⟦(f : (a : N) → M) x⟧ =
    ((c.comapQuotientEquivOfSurj (↑f : N →+* M) ⋯ hcd : RingEquiv.{u_2, u_1} d.Quotient c.Quotient) :
        (a : d.Quotient) → c.Quotient)
      (↑x : d.Quotient)

Tactic:
rw [comapQuotientEquivOfSurj_mk, RingEquiv.coe_toRingHom]

Premises used: RingEquiv.coe_toRingHom, RingCon.comapQuotientEquivOfSurj_mk
-- 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 : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦(f : (a : N) → M) x⟧ = (↑((f : (a : N) → M) x) : c.Quotient)

Tactic:
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 : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_1 + 1} (α := ↥(c.mk'.comp f).rangeS)
    ((c.comapQuotientEquivRangeS f hcd : (a : d.Quotient) → ↥(c.mk'.comp f).rangeS) (↑x : d.Quotient) :
      ↥(c.mk'.comp f).rangeS)
    (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (c.mk'.comp f).rangeS) (↑((f : (a : N) → M) x) : c.Quotient) ⋯ :
      ↥(c.mk'.comp f).rangeS)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, 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 : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivRangeS f hcd).symm : (a : ↥(c.mk'.comp f).rangeS) → d.Quotient)
        (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (c.mk'.comp f).rangeS) (↑((f : (a : N) → M) x) : c.Quotient) ⋯) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
simp [RingEquiv.symm_apply_eq]

Premises used: RingEquiv.symm_apply_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_1 : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HMul.hMul (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    (d.mk' : (a : M) → d.Quotient) (a * b)

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_1 : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
rw :
  (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HAdd.hAdd (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    (d.mk' : (a : M) → d.Quotient) (a + b)
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HAdd.hAdd (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    HAdd.hAdd (α := d.Quotient) (β := d.Quotient) ((d.mk' : (a : M) → d.Quotient) a : d.Quotient)
      ((d.mk' : (a : M) → d.Quotient) b : d.Quotient)

Tactic:
rw [← d.mk'.map_add]

Premises used: RingCon.mk', RingHom.map_add
-- 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_1 : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HAdd.hAdd (α := (ker (c.map d h)).Quotient) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    (d.mk' : (a : M) → d.Quotient) (a + b)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c d : RingCon M
h : c ≤ d
x : M
⊢ (c.quotientQuotientEquivQuotient d h : (a : (ker (c.map d h)).Quotient) → d.Quotient) ⟦⟦x⟧⟧ = ⟦x⟧

Tactic:
rfl

Premises used: Quotient.liftOn', rfl