awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
h :
  LE.le (α := Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        s :
      Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        t :
      Con c.Quotient)
x y : M
hs : ((↑s : Con M) : (a : M) → M → Prop) x y
mp :
  ∀ (a b : M) (ht : ((↑t : Con M).toSetoid : M → M → Prop) a b)
    (hx :
      Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
        ((c.mkMulHom : (a : M) → c.Quotient) x : c.Quotient))
    (hy :
      Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) b : c.Quotient)
        ((c.mkMulHom : (a : M) → c.Quotient) y : c.Quotient)),
    ((↑t : Con M) : (a : M) → M → Prop) x y
⊢ ((↑t : Con M) : (a : M) → M → Prop) x y

Tactic:
rcases h ⟨x, y, hs, rfl, rfl⟩ with ⟨a, b, ht, hx, hy⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
h :
  LE.le (α := Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        s :
      Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        t :
      Con c.Quotient)
x y : M
hs : ((↑s : Con M) : (a : M) → M → Prop) x y
a b : M
ht : ((↑t : Con M).toSetoid : M → M → Prop) a b
hx :
  Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) x : c.Quotient)
hy :
  Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) b : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) y : c.Quotient)
⊢ ((↑t : Con M) : (a : M) → M → Prop) x y

Tactic:
t.1.trans (t.1.symm <| t.2 <| c.eq.1 hx) (t.1.trans ht (t.2 <| c.eq.1 hy))

Premises used: Con.trans, Con.eq, Con.symm, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
h :
  LE.le (α := Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        s :
      Con c.Quotient)
    (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
            invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : { d : Con M // c ≤ d }) → Con c.Quotient)
        t :
      Con c.Quotient)
x y : M
hs : ((↑s : Con M) : (a : M) → M → Prop) x y
a b : M
ht : ((↑t : Con M).toSetoid : M → M → Prop) a b
hx :
  Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) a : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) x : c.Quotient)
hy :
  Eq (α := c.Quotient) ((c.mkMulHom : (a : M) → c.Quotient) b : c.Quotient)
    ((c.mkMulHom : (a : M) → c.Quotient) y : c.Quotient)
⊢ ((↑t : Con M) : (a : M) → M → Prop) x y

Tactic:
exact t.1.trans (t.1.symm <| t.2 <| c.eq.1 hx) (t.1.trans ht (t.2 <| c.eq.1 hy))

Premises used: Con.trans, Con.eq, Con.symm, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
⊢ s ≤ t →
    LE.le (α := Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          s :
        Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          t :
        Con c.Quotient)

Tactic:
Relation.map_mono

Premises used: Relation.map_mono
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.6137
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
inst_3 : FunLike F M N
inst_4 : MulHomClass F M N
c : Con M
s t : { d : Con M // c ≤ d }
⊢ s ≤ t →
    LE.le (α := Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          s :
        Con c.Quotient)
      (({ toFun := fun (d : { d : Con M // c ≤ d }) ↦ mapOfSurjective c.mkMulHom ⋯ ⋯,
              invFun := fun (d : Con c.Quotient) ↦ Subtype.mk (p := fun (d : Con M) ↦ c ≤ d) (comap toQuotient ⋯ d) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { d : Con M // c ≤ d }) → Con c.Quotient)
          t :
        Con c.Quotient)

Tactic:
exact Relation.map_mono

Premises used: Relation.map_mono
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
inst : MulOneClass M
c : Con M
⊢ ker c.mk' = c

Tactic:
ext fun _ _ => c.eq

Premises used: Con.eq, Con.ext
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
inst : MulOneClass M
c : Con M
⊢ Surjective (α := M) (β := c.Quotient) (⇑c.mk' : (a : M) → c.Quotient)

Tactic:
Quotient.mk''_surjective

Premises used: Con.Quotient, Quotient.mk''_surjective, Con.toQuotient
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
inst : MulOneClass M
c : Con M
⊢ Eq (α := (a : M) → c.Quotient) (⇑c.mk' : (a : M) → c.Quotient) toQuotient

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
f : M →* P
x y : M
⊢ (ker f : (a : M) → M → Prop) x y ↔ Eq.{u_3 + 1} (α := P) ((f : (a : M) → P) x : P) ((f : (a : M) → P) y : P)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N →* M
x y : N
rw :
  Eq.{u_1 + 1} (α := c.Quotient) ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)
      ((↑((f : (a : N) → M) y) : c.Quotient) : c.Quotient) ↔
    Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) x) : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) y) : c.Quotient)
⊢ (c : (a : M) → M → Prop) ((f : (a : N) → M) x : M) ((f : (a : N) → M) y) ↔
    Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) x) : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) y) : c.Quotient)

Tactic:
rw [← c.eq]

Premises used: Con.eq
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ Eq.{u_1 + 1} (α := c.Quotient) ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)
      ((↑((f : (a : N) → M) y) : c.Quotient) : c.Quotient) ↔
    Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) x) : c.Quotient)
      ((c.mk' : (a : M) → c.Quotient) ((f : (a : N) → M) y) : c.Quotient)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
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 : M →* P
H : c ≤ ker f
rw : Eq.{u_3 + 1} (α := P) (Con.liftOn (c := c) 1 (⇑f : (a : M) → P) ⋯ : P) ((f : (a : M) → P) 1 : P)
⊢ Eq.{u_3 + 1} (α := P) (Con.liftOn (c := c) 1 (⇑f : (a : M) → P) ⋯) 1

Tactic:
rw [← f.map_one]

Premises used: MonoidHom.map_one
-- Module: Mathlib.GroupTheory.Congruence.Hom
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 : M →* P
H : c ≤ ker f
⊢ Eq.{u_3 + 1} (α := P) (Con.liftOn (c := c) 1 (⇑f : (a : M) → P) ⋯ : P) ((f : (a : M) → P) 1 : P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
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 : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
dsimp : (f : (a : M) → P) (m * n) = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)
⊢ Con.liftOn (HMul.hMul (α := c.Quotient) (↑m : c.Quotient) (↑n : c.Quotient)) (⇑f : (a : M) → P) ⋯ =
    HMul.hMul (α := P) (Con.liftOn (c := c) (↑m : c.Quotient) (⇑f : (a : M) → P) ⋯)
      (Con.liftOn (c := c) (↑n : c.Quotient) (⇑f : (a : M) → P) ⋯)

Tactic:
dsimp only [← coe_mul, Con.liftOn_coe]

Premises used: Con.liftOn_coe, Con.coe_mul
-- Module: Mathlib.GroupTheory.Congruence.Hom
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 : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
rw rw₁ :
  HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P) =
    HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)
⊢ (f : (a : M) → P) (m * n) = HMul.hMul (α := P) (β := P) ((f : (a : M) → P) m : P) ((f : (a : M) → P) n : P)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con 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', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con 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', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
h : ∀ (x : M), Eq.{u_3 + 1} (α := P) (((c.lift f H).comp c.mk' : (a : M) → P) x : P) ((f : (a : M) → P) x : P)
⊢ (c.lift f H).comp c.mk' = f

Tactic:
ext
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x : M
⊢ Eq.{u_3 + 1} (α := P) (((c.lift f H).comp c.mk' : (a : M) → P) x : P) ((f : (a : M) → P) x : P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
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 : M →* P
f : MonoidHom.{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, Con.eq
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : MonoidHom.{u_1, u_3} c.Quotient P
h :
  ∀ (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.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : MonoidHom.{u_1, u_3} c.Quotient P
x : c.Quotient
h :
  ∀ (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.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : MonoidHom.{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.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f g : MonoidHom.{u_1, u_3} c.Quotient P
h : f.comp c.mk' = g.comp c.mk'
rw : c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯
⊢ f = g

Tactic:
rw [← lift_apply_mk' f, ← lift_apply_mk' g]

Premises used: Con.lift_apply_mk'
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f g : MonoidHom.{u_1, u_3} c.Quotient P
h : f.comp c.mk' = g.comp c.mk'
⊢ c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f g : MonoidHom.{u_1, u_3} c.Quotient P
h :
  ∀ (a : M),
    Eq.{u_3 + 1} (α := P) ((f : (a : c.Quotient) → P) (↑a : c.Quotient) : P)
      ((g : (a : c.Quotient) → P) (↑a : c.Quotient) : P)
⊢ f = g

Tactic:
hom_ext <| DFunLike.ext _ _ h

Premises used: Con.hom_ext, DFunLike.ext
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
g : MonoidHom.{u_1, u_3} c.Quotient P
Hg : g.comp c.mk' = f
⊢ g = c.lift f H

Tactic:
hom_ext Hg

Premises used: Con.hom_ext
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con 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:
fun y =>
  (Exists.elim (hf y)) fun w hw => ⟨w, (lift_mk' h w).symm ▸ hw⟩

Premises used: Eq.rec, Exists.intro, Con.lift_mk', Con.toQuotient, Eq.symm, Function.Surjective, Exists.elim
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
c : Con 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:
toSetoid_injective <| Setoid.ker_eq_lift_of_injective f H h

Premises used: Con.toSetoid_injective, Setoid.ker_eq_lift_of_injective, DFunLike.coe
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass 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', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass P
f : M →* P
⊢ Injective.{u_1 + 1, u_3 + 1} (α := Con.Quotient (ker f)) (β := P) (⇑(kerLift f) : (a : (ker f).Quotient) → P)

Tactic:
fun x y =>
  Quotient.inductionOn₂' x y fun _ _ => (ker f).eq.2

Premises used: Quotient.inductionOn₂', Function.Injective
-- Module: Mathlib.GroupTheory.Congruence.Hom
Goal:
M : Type u_1
inst : MulOneClass M
c d : Con 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.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
mp :
  (∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y) →
    ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
mpr :
  (∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y) →
    ∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y
⊢ (∀ {x y : Mᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
            (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
mp : ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
⊢ ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y

Tactic:
_
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
x : M
mp : ∀ {y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
⊢ ∀ {y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y

Tactic:
_
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h : ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
mpr :
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
⊢ ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y

Tactic:
_
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h : ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
x : Mᵐᵒᵖ
mpr :
  ∀ {y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
⊢ ∀ {y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y

Tactic:
_
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
x y : M
h' : (c : (a : M) → M → Prop) x y
⊢ (d : (a : M) → M → Prop) x y

Tactic:
h h'

Premises used: MulOpposite.unop
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h :
  ∀ {x y : Mᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
        x y
x y : M
h' : (c : (a : M) → M → Prop) x y
⊢ (d : (a : M) → M → Prop) x y

Tactic:
exact h h'
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h : ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
x y : Mᵐᵒᵖ
h' :
  ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
      (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
    x y
⊢ ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
      (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
    x y

Tactic:
h h'
-- Module: Mathlib.GroupTheory.Congruence.Opposite
Goal:
M : Type u_1
inst : Mul M
c d : Con M
h : ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y
x y : Mᵐᵒᵖ
h' :
  ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) c : Con Mᵐᵒᵖ) :
      (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
    x y
⊢ ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : Con M) → Con Mᵐᵒᵖ) d : Con Mᵐᵒᵖ) :
      (a : Mᵐᵒᵖ) → Mᵐᵒᵖ → Prop)
    x y

Tactic:
exact h h'
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Con.ker (F := FreeMonoid (M ⊕ N) →* M ∗ N) mk = coprodCon M N

Tactic:
Con.mk'_ker _

Premises used: Monoid.Coprod.mk, Con.mk'_ker, Monoid.Coprod