awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
⊢ Eq (α := RingHom.{u_1, u_3} R₁ (A ⧸ I)) (RingHom.comp (mk I) (algebraMap R₁ A)) (algebraMap R₁ (A ⧸ I))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
x : R₁
⊢ Eq (α := A ⧸ I) ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) x) : A ⧸ I)
    ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) x : A ⧸ I)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
⊢ Surjective (α := A) (β := A ⧸ I) (⇑(mkₐ R₁ I) : (a : A) → A ⧸ I)

Tactic:
Quot.mk_surjective

Premises used: Submodule.Quotient.mk, Quotient, Quot.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I : Ideal A
inst_3 : I.IsTwoSided
⊢ ker (F := A →+* A ⧸ I) (↑(mkₐ R₁ I) : A →+* A ⧸ I) = I

Tactic:
Ideal.mk_ker

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
mp : Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I) → I = ⊥
mpr : I = ⊥ → Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)
⊢ Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I) ↔ I = ⊥

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
h : Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)
mp : Eq (α := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (mk I) I) ⊥
⊢ I = ⊥

Tactic:
rw [← map_eq_bot_iff_of_injective h.1]

Premises used: Ideal.map_eq_bot_iff_of_injective, And.left
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
h : Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)
⊢ Eq (α := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (mk I) I) ⊥

Tactic:
(map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm

Premises used: Iff.mpr, Ideal.mk_ker, le_of_eq, Eq.symm, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
h : Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)
⊢ Eq (α := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (mk I) I) ⊥

Tactic:
exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm

Premises used: Iff.mpr, Ideal.mk_ker, le_of_eq, Eq.symm, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
h rw : I = ⊥
rw₁ rw₂ : Eq.{u_3 + 1} (α := Ideal A) ⊥ ⊥
⊢ Eq (α := Ideal A) (ker (F := A →+* A ⧸ I) (mk I)) ⊥

Tactic:
rw [mk_ker, h]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
⊢ I = ⊥ → Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)

Tactic:
exact fun h => ⟨(injective_iff_ker_eq_bot _).mpr <| by rw [mk_ker, h], mk_surjective⟩
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
⊢ Eq (α := A ⧸ I →+* A ⧸ J) (↑(factorₐ R₁ hIJ) : A ⧸ I →+* A ⧸ J) (factor hIJ)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.Quotient.factor, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
x : A
⊢ Eq (α := A ⧸ J) ((factorₐ R₁ hIJ : (a : A ⧸ I) → A ⧸ J) ((mk I : (a : A) → A ⧸ I) x) : A ⧸ J)
    ((mk J : (a : A) → A ⧸ J) x : A ⧸ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
⊢ Eq (α := A →ₐ[R₁] A ⧸ J) (AlgHom.comp (factorₐ R₁ hIJ) (mkₐ R₁ I)) (mkₐ R₁ J)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, AlgHom.comp, Ideal.Quotient.mkₐ, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
x : A ⧸ I
⊢ Eq (α := A ⧸ J) ((factorₐ R₁ hIJ : (a : A ⧸ I) → A ⧸ J) x : A ⧸ J) ((factor hIJ : (a : A ⧸ I) → A ⧸ J) x : A ⧸ J)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
H :
  ∀ (x : A ⧸ I),
    Eq (α := A ⧸ I) ((factorₐ R ⋯ : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)
      ((AlgHom.id R (A ⧸ I) : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)
⊢ Eq (α := A ⧸ I →ₐ[R] A ⧸ I) (factorₐ R ⋯) (AlgHom.id R (A ⧸ I))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
x : A ⧸ I
⊢ Eq (α := A ⧸ I) ((factorₐ R ⋯ : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)
    ((AlgHom.id R (A ⧸ I) : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
K : Ideal A
inst_5 : K.IsTwoSided
hJK : J ≤ K
H :
  ∀ (x : A),
    Eq (α := A ⧸ K)
      ((AlgHom.comp (AlgHom.comp (factorₐ R₁ hJK) (factorₐ R₁ hIJ)) (mkₐ R₁ I) : (a : A) → A ⧸ K) x : A ⧸ K)
      ((AlgHom.comp (factorₐ R₁ ⋯) (mkₐ R₁ I) : (a : A) → A ⧸ K) x : A ⧸ K)
⊢ Eq (α := A →ₐ[R₁] A ⧸ K) (AlgHom.comp (AlgHom.comp (factorₐ R₁ hJK) (factorₐ R₁ hIJ)) (mkₐ R₁ I))
    (AlgHom.comp (factorₐ R₁ ⋯) (mkₐ R₁ I))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
I J : Ideal A
inst_3 : I.IsTwoSided
inst_4 : J.IsTwoSided
hIJ : I ≤ J
K : Ideal A
inst_5 : K.IsTwoSided
hJK : J ≤ K
x : A
⊢ Eq (α := A ⧸ K) ((AlgHom.comp (AlgHom.comp (factorₐ R₁ hJK) (factorₐ R₁ hIJ)) (mkₐ R₁ I) : (a : A) → A ⧸ K) x : A ⧸ K)
    ((AlgHom.comp (factorₐ R₁ ⋯) (mkₐ R₁ I) : (a : A) → A ⧸ K) x : A ⧸ K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
inst_7 : Semiring B
inst_8 : Algebra R₁ B
I : Ideal A
inst_9 : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
r : R₁
⊢ Eq.{u_3 + 1} (α := A ⧸ I) ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r : A ⧸ I)
    ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r) : A ⧸ I)

Tactic:
have : algebraMap R₁ (A ⧸ I) r = Ideal.Quotient.mk I (algebraMap R₁ A r) := rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u
S : Type v
F : Type w
inst : Ring R
inst_1 : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst_2 : CommSemiring R₁
inst_3 : CommSemiring R₂
inst_4 : Ring A
inst_5 : Algebra R₁ A
inst_6 : Algebra R₂ A
inst_7 : Semiring B
inst_8 : Algebra R₁ B
I : Ideal A
inst_9 : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
r : R₁
this :
  Eq.{u_3 + 1} (α := A ⧸ I) ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r : A ⧸ I)
    ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r) : A ⧸ I)
rw :
  OneHom.toFun (↑(↑(lift I (↑f : A →+* B) hI) : A ⧸ I →* B) : OneHom (A ⧸ I) B)
      ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r)) =
    (algebraMap R₁ B : (a : R₁) → B) r
rw₁ :
  Eq.{u_4 + 1} (α := B)
    ((lift I (↑f : A →+* B) hI : (a : A ⧸ I) → B)
        ((mk I : (a : A) → A ⧸ I) ((algebraMap R₁ A : (a : R₁) → A) r) : A ⧸ I) :
      B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₂ :
  Eq.{u_4 + 1} (α := B) (((↑f : A →+* B) : (a : A) → B) ((algebraMap R₁ A : (a : R₁) → A) r : A) : B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₃ :
  Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) ((algebraMap R₁ A : (a : R₁) → A) r : A) : B)
    ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₄ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) r 1) : B) ((algebraMap R₁ B : (a : R₁) → B) r : B)
rw₅ : (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r 1
rw₆ : HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B) = HSMul.hSMul (β := B) r 1
rw₇ rw₈ : HSMul.hSMul (β := B) r 1 = HSMul.hSMul (β := B) r 1
⊢ OneHom.toFun (↑(↑(lift I (↑f : A →+* B) hI) : A ⧸ I →* B) : OneHom (A ⧸ I) B)
      ((algebraMap R₁ (A ⧸ I) : (a : R₁) → A ⧸ I) r) =
    (algebraMap R₁ B : (a : R₁) → B) r

Tactic:
rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk,
        AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one,
        map_smul, map_one]

Premises used: AlgHom.coe_toRingHom, Ideal.Quotient.lift_mk, RingHom.toFun_eq_coe, Algebra.algebraMap_eq_smul_one, map_one, map_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
I : Ideal A
inst_5 : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
x : A ⧸ I
⊢ Eq.{u_4 + 1} (α := B) ((liftₐ I f hI : (a : A ⧸ I) → B) x : B) ((lift I (↑f : A →+* B) hI : (a : A ⧸ I) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
I : Ideal A
inst_5 : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) (0 : B)
⊢ AlgHom.comp (liftₐ I f hI) (mkₐ R₁ I) = f

Tactic:
AlgHom.ext fun _ => (Ideal.Quotient.lift_mk I (f : A →+* B) hI :)

Premises used: AlgHom.ext, Ideal.Quotient.lift_mk, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
rw : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) ⊤
rw₁ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (LinearMap.range (Submodule.mkQ I))
rw₂ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) ⊤)
rw₃ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (span {1}))
rw₄ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (Submodule.map (Submodule.mkQ I) (A ∙ 1))
rw₅ :
  Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
    (Submodule.span A (Set.image (α := A) (⇑(Submodule.mkQ I) : (a : A) → A ⧸ I) {1}))
rw₆ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (Submodule.mkQ I : (a : A) → A ⧸ I) 1)
rw₇ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ Submodule.Quotient.mk 1)
rw₈ rw₉ : Eq (α := Submodule A (A ⧸ I)) (A ∙ (mk I : (a : A) → A ⧸ I) 1) (A ∙ (mk I : (a : A) → A ⧸ I) 1)
⊢ Eq (α := Submodule A (A ⧸ I)) (A ∙ 1) ⊤

Tactic:
rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one,
    Ideal.span, Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]

Premises used: Set.image_singleton, Ideal.Quotient.mk, Submodule.map_top, Submodule.range_mkQ, Ideal.span_singleton_one, Submodule.mkQ_apply, map_one, Ideal.Quotient.mk_eq_mk, Ideal.span, Submodule.map_span
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
inst : CommRing R
a : R
I : Ideal R
⊢ HSMul.hSMul (β := Submodule R (R ⧸ I)) a ⊤ = R ∙ Submodule.Quotient.mk a

Tactic:
simp [← Ideal.Quotient.span_singleton_one, Algebra.smul_def, Submodule.smul_span]

Premises used: Ideal.Quotient.span_singleton_one, Algebra.smul_def, Submodule.smul_span
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : HasQuotient.Quotient A (B := Ideal A) (ker f)
obtain :
  ∀ (a : A),
    (f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
        (HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (ker f)) r
          ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))) =
      HSMul.hSMul (β := B) r
        ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
            ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
          B)
⊢ (f.kerLift : (a : A ⧸ ker f.toRingHom) → B) (r • x) =
    HSMul.hSMul (β := B) r ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B) x : B)

Tactic:
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x

Premises used: Ideal.Quotient.mkₐ_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ (f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
      (HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (ker f)) r
        ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))) =
    HSMul.hSMul (β := B) r
      ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
          ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
        B)

Tactic:
_root_.map_smul f _ _

Premises used: Quotient.liftOn', AddCon.liftOn, map_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ (f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
      (HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (ker f)) r
        ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))) =
    HSMul.hSMul (β := B) r
      ((f.kerLift : (a : A ⧸ ker f.toRingHom) → B)
          ((Quotient.mkₐ R₁ (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
        B)

Tactic:
exact _root_.map_smul f _ _

Premises used: map_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ Eq.{u_4 + 1} (α := B)
    ((kerLiftAlg f : (a : A ⧸ ker f) → B)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)
    ((f : (a : A) → B) a : B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
⊢ (↑(kerLiftAlg f) : A ⧸ ker f →+* B) = kerLift (↑f : A →+* B)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Ideal.comap, RingHom.kerLift, Ideal.Quotient.lift, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, rfl, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
⊢ Injective.{u_3 + 1, u_4 + 1} (α := HasQuotient.Quotient A (B := Ideal A) (ker f)) (β := B)
    (⇑(kerLiftAlg f) : (a : A ⧸ ker f) → B)

Tactic:
RingHom.kerLift_injective (R := A) (S := B) f

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, RingHom.kerLift_injective, RingHomClass.toRingHom, Ideal.comap, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_4 + 1} (α := B)
    ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)
    ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
a₁ :
  Eq.{u_4 + 1} (α := B)
    ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
        (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) a) :
          HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)
    ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)
⊢ Eq.{u_3 + 1} (α := HasQuotient.Quotient A (B := Ideal A) (ker f))
    (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) a) :
      HasQuotient.Quotient A (B := Ideal A) (ker f))
    ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f))

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hf).injective

Premises used: AlgEquiv.injective, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst : CommSemiring R₁
inst_1 : Ring A
inst_2 : Algebra R₁ A
inst_3 : Semiring B
inst_4 : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_4 + 1} (α := B)
    ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
        (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) a) :
          HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)
    ((quotientKerAlgEquivOfSurjective hf : (a : A ⧸ ker f) → B)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) a : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
dsimp :
  Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((↑(quotientKerAlgEquivOfSurjective hf).symm : B →ₐ[R] A ⧸ ker f) : (a : B) → A ⧸ ker (↑f : A →+* B))
            ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker (F := A →+* B) (↑f : A →+* B))) :
      C)
    ((g : (a : A) → C) x : C)
⊢ Eq.{u_8 + 1} (α := C) ((f.liftOfSurjective hf g H : (a : B) → C) ((f : (a : A) → B) x : B) : C)
    ((g : (a : A) → C) x : C)

Tactic:
dsimp [AlgHom.liftOfSurjective]

Premises used: AlgHom.liftOfSurjective
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
erw :
  Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      C)
    ((g : (a : A) → C) x : C)
⊢ Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((↑(quotientKerAlgEquivOfSurjective hf).symm : B →ₐ[R] A ⧸ ker f) : (a : B) → A ⧸ ker (↑f : A →+* B))
            ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker (F := A →+* B) (↑f : A →+* B))) :
      C)
    ((g : (a : A) → C) x : C)

Tactic:
erw [AlgEquiv.coe_algHom]

Premises used: AlgEquiv.coe_algHom
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
rw :
  Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) x : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      C)
    ((g : (a : A) → C) x : C)
⊢ Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        (((quotientKerAlgEquivOfSurjective hf).symm : (a : B) → A ⧸ ker f) ((f : (a : A) → B) x) :
          HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      C)
    ((g : (a : A) → C) x : C)

Tactic:
rw [Ideal.quotientKerAlgEquivOfSurjective_symm_apply]

Premises used: Ideal.quotientKerAlgEquivOfSurjective_symm_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
x : A
⊢ Eq.{u_8 + 1} (α := C)
    ((Quotient.liftₐ (ker (F := A →+* B) (↑f : A →+* B)) g H : (a : A ⧸ ker (↑f : A →+* B)) → C)
        ((Quotient.mk (ker f) : (a : A) → A ⧸ ker f) x : HasQuotient.Quotient A (B := Ideal A) (ker f)) :
      C)
    ((g : (a : A) → C) x : C)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
Goal:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
hf : Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →ₐ[R] C
H : LE.le (α := Ideal A) (ker f.toRingHom) (ker g.toRingHom)
H₁ :
  ∀ (x : A), Eq.{u_8 + 1} (α := C) (((f.liftOfSurjective hf g H).comp f : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
⊢ (f.liftOfSurjective hf g H).comp f = g

Tactic:
ext