awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have 1 : ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R_1 : Type u
S : Type v
F : Type w
inst : Ring R_1
inst_1 : Semiring S
ι_1 : Type u_1
R : Type u_2
inst_2 : CommRing R
ι : Type u_3
inst_3 : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have 1₁ : ∀ (h : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  (IsCoprime on f) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R ⧸ I ⊓ J →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)
have h : Eq (α := R →+* R ⧸ I)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (Quotient.mk (I ⊓ J)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I ⊓ J)))
Tactic: apply Quotient.ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))
have h : ∀ (x : R),
  Eq (α := R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
              (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I ⊓ J)) :
          (a : R) → R ⧸ I)
        x :
      R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ I) x : R ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R ⧸ I ⊓ J →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)
have h : Eq (α := R →+* R ⧸ J)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
    (Quotient.mk (I ⊓ J)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I ⊓ J)))
Tactic: apply Quotient.ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I ⊓ J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I ⊓ J)))
have h : ∀ (x : R),
  Eq (α := R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
              (↑(I.quotientInfEquivQuotientProd J coprime) : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I ⊓ J)) :
          (a : R) → R ⧸ J)
        x :
      R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I ⊓ J)) : (a : R) → R ⧸ J) x : R ⧸ J)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R ⧸ I * J →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)
have h : Eq (α := R →+* R ⧸ I)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (Quotient.mk (I * J)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I * J)))
Tactic: apply Quotient.ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R →+* R ⧸ I)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))
have h : ∀ (x : R),
  Eq (α := R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (fst (R ⧸ I) (R ⧸ J))
              (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I * J)) :
          (a : R) → R ⧸ I)
        x :
      R ⧸ I)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I * J)) : (a : R) → R ⧸ I) x : R ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R ⧸ I * J →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (factor ⋯)
have h : Eq (α := R →+* R ⧸ J)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
      (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
    (Quotient.mk (I * J)))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I * J)))
Tactic: apply Quotient.ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ Eq (α := R →+* R ⧸ J)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
        (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
      (Quotient.mk (I * J)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor ⋯) (Quotient.mk (I * J)))
have h : ∀ (x : R),
  Eq (α := R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (snd (R ⧸ I) (R ⧸ J))
              (↑(I.quotientMulEquivQuotientProd J coprime) : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J))
            (Quotient.mk (I * J)) :
          (a : R) → R ⧸ J)
        x :
      R ⧸ J)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factor sorry) (Quotient.mk (I * J)) : (a : R) → R ⧸ J) x : R ⧸ J)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
⊢ Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I) ↔ I = ⊥
have mp : Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I) → I = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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 = ⊥
⊢ Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I) ↔ I = ⊥
have mpr : I = ⊥ → Bijective (α := A) (β := A ⧸ I) (⇑(mk I) : (a : A) → A ⧸ I)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ I = ⊥
have mp : Eq (α := Ideal (A ⧸ I)) (map (F := A →+* A ⧸ I) (mk I) I) ⊥
Tactic: rw [← map_eq_bot_iff_of_injective h.1]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
A : Type u_3
inst : Ring A
I : Ideal A
inst_1 : I.IsTwoSided
h rw : I = ⊥
⊢ Eq (α := Ideal A) (ker (F := A →+* A ⧸ I) (mk I)) ⊥
have rw₁ : Eq.{u_3 + 1} (α := Ideal A) ⊥ ⊥
Tactic: rw [mk_ker, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_5
A : Type u_6
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
⊢ Eq (α := A ⧸ I →ₐ[R] A ⧸ I) (factorₐ R ⋯) (AlgHom.id R (A ⧸ I))
have H : ∀ (x : A ⧸ I),
  Eq (α := A ⧸ I) ((factorₐ R sorry : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)
    ((AlgHom.id R (A ⧸ I) : (a : A ⧸ I) → A ⧸ I) x : A ⧸ I)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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
⊢ 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))
have 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₁ sorry) (mkₐ R₁ I) : (a : A) → A ⧸ K) x : A ⧸ K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
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₁
⊢ 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
have 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)
Tactic: have : algebraMap R₁ (A ⧸ I) r = Ideal.Quotient.mk I (algebraMap R₁ A r) := rfl
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ 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
have rw₄ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) (HSMul.hSMul (β := A) r 1) : B) ((algebraMap R₁ B : (a : R₁) → B) r : B)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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)
⊢ 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
have rw₅ : (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r 1
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
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
⊢ 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
have rw₆ : HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B) = HSMul.hSMul (β := B) r 1
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]