awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallySmooth R A
inst_8 : FormallySmooth A B
C : Type (max u_4 u_6)
x : CommRing C
x_1 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have obtain : ∀ (f' : A →ₐ[R] C) (e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = f.comp (IsScalarTower.toAlgHom R A B)),
  ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: obtain ⟨f', e⟩ := FormallySmooth.comp_surjective _ _ I hI (f.comp (IsScalarTower.toAlgHom R A B))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallySmooth R A
inst_8 : FormallySmooth A B
C : Type (max u_4 u_6)
x : CommRing C
x_1 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
⊢ ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have obtain : ∀ (f'' : B →ₐ[A] C)
  (e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f'' = { toRingHom := f.toRingHom, commutes' := sorry : B →ₐ[A] C ⧸ I }),
  ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: obtain ⟨f'', e'⟩ := comp_surjective _ _ I hI { f with commutes' := AlgHom.congr_fun e.symm }
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallySmooth R A
inst_8 : FormallySmooth A B
C : Type (max u_4 u_6)
x : CommRing C
x_1 : Algebra R C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = f.comp (IsScalarTower.toAlgHom R A B)
this : Algebra A C := f'.toAlgebra
f'' : B →ₐ[A] C
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f'' = { toRingHom := f.toRingHom, commutes' := ⋯ : B →ₐ[A] C ⧸ I }
⊢ ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
have e'₁ : Eq (α := B →ₐ[R] C ⧸ I) (AlgHom.restrictScalars R (AlgHom.comp (Ideal.Quotient.mkₐ A I) f''))
  (AlgHom.restrictScalars R (S := A) { toRingHom := f.toRingHom, commutes' := sorry })
Tactic: apply_fun AlgHom.restrictScalars R at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallySmooth R B
⊢ FormallySmooth A B
have refine : ∀ (C : Type (max u_5 u_6)) (x : CommRing C) (x_1 : Algebra A C) (I : Ideal C) (hI : HPow.hPow (β := ℕ) I 2 = ⊥)
  (f : B →ₐ[A] C ⧸ I), ∃ (a : B →ₐ[A] C), AlgHom.comp (Ideal.Quotient.mkₐ A I) a = f
Tactic: refine iff_comp_surjective.mpr fun C _ _ I hI f ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallySmooth R B
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra A C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A C) (algebraMap R A))
scalarTowerInst : IsScalarTower R A C := ⋯
⊢ ∃ (a : B →ₐ[A] C), AlgHom.comp (Ideal.Quotient.mkₐ A I) a = f
have obtain : ∀ (g : B →ₐ[R] C) (hg : AlgHom.comp (Ideal.Quotient.mkₐ R I) g = AlgHom.restrictScalars R f),
  ∃ (a : B →ₐ[A] C), AlgHom.comp (Ideal.Quotient.mkₐ A I) a = f
Tactic: obtain ⟨g, hg⟩ := Algebra.FormallySmooth.comp_surjective _ _ I hI (f.restrictScalars R)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallySmooth R B
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra A C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A C) (algebraMap R A))
scalarTowerInst : IsScalarTower R A C := ⋯
g : B →ₐ[R] C
hg : AlgHom.comp (Ideal.Quotient.mkₐ R I) g = AlgHom.restrictScalars R f
⊢ ∃ (a : B →ₐ[A] C), AlgHom.comp (Ideal.Quotient.mkₐ A I) a = f
have suffices : Eq (α := A →ₐ[R] C) (g.comp (IsScalarTower.toAlgHom R A B)) (IsScalarTower.toAlgHom R A C)
Tactic: suffices g.comp (IsScalarTower.toAlgHom R A B) = IsScalarTower.toAlgHom R A C from
    ⟨{ __ := g, commutes' x := congr($this x) }, AlgHom.ext fun x ↦ congr($hg x)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallySmooth R B
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra A C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A C) (algebraMap R A))
scalarTowerInst : IsScalarTower R A C := ⋯
g : B →ₐ[R] C
hg : AlgHom.comp (Ideal.Quotient.mkₐ R I) g = AlgHom.restrictScalars R f
⊢ Eq (α := A →ₐ[R] C) (g.comp (IsScalarTower.toAlgHom R A B)) (IsScalarTower.toAlgHom R A C)
have a : Eq (α := A →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (g.comp (IsScalarTower.toAlgHom R A B)))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A C))
Tactic: apply Algebra.FormallyUnramified.comp_injective _ hI
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallyUnramified R A
inst_8 : FormallySmooth R B
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra A C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B →ₐ[A] C ⧸ I
algInst : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A C) (algebraMap R A))
scalarTowerInst : IsScalarTower R A C := ⋯
g : B →ₐ[R] C
hg : AlgHom.comp (Ideal.Quotient.mkₐ R I) g = AlgHom.restrictScalars R f
⊢ Eq (α := A →ₐ[R] C ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I) (g.comp (IsScalarTower.toAlgHom R A B)))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A C))
have a : Eq (α := A →ₐ[R] C ⧸ I) (AlgHom.comp (AlgHom.restrictScalars R f) (IsScalarTower.toAlgHom R A B))
  (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A C))
Tactic: rw [← AlgHom.comp_assoc, hg]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
inst_1 : CommRing A
inst_2 : Algebra R A
h : Function.Surjective.{u_4 + 1, u_6 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ FormallySmooth R A ↔ IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
have rw : (∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
    AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A) ↔
  IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
Tactic: rw [Algebra.FormallySmooth.iff_split_surjection (Algebra.ofId R A) h]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
inst_1 : CommRing A
inst_2 : Algebra R A
h : Function.Surjective.{u_4 + 1, u_6 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ (∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
      AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A) ↔
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
have mp : (∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
    AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A) →
  IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_6
inst_1 : CommRing A
inst_2 : Algebra R A
h : Function.Surjective.{u_4 + 1, u_6 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
mp :
  (∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
      AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A) →
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
⊢ (∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
      AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A) ↔
    IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
have mpr : IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) →
  ∃ (g : A →ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (AlgHom.toRingHom (ofId R A))) 2),
    AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C
inst_6 : Algebra R_1 C
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
⊢ FormallySmooth B (B ⊗[R] A)
have refine : ∀ (C : Type (max u_5 u_6)) (x : CommRing C) (x_1 : Algebra B C) (I : Ideal C) (hI : HPow.hPow (β := ℕ) I 2 = ⊥)
  (f : B ⊗[R] A →ₐ[B] C ⧸ I), ∃ (a : B ⊗[R] A →ₐ[B] C), AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
Tactic: refine .of_comp_surjective fun C _ _ I hI f ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
⊢ ∃ (a : B ⊗[R] A →ₐ[B] C), AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
have this₁ : IsScalarTower R B C
Tactic: haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ ∃ (a : B ⊗[R] A →ₐ[B] C), AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
have refine_1 : A →ₐ[R] C
Tactic: refine ⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
refine_1 : A →ₐ[R] C
⊢ ∃ (a : B ⊗[R] A →ₐ[B] C), AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
have refine_2 : AlgHom.comp (Ideal.Quotient.mkₐ B I)
    (TensorProduct.productLeftAlgHom (ofId B C)
      (lift I sorry (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight))) =
  f
Tactic: refine ⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ AlgHom.comp (Ideal.Quotient.mkₐ B I)
      (TensorProduct.productLeftAlgHom (ofId B C)
        (lift I ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight))) =
    f
have refine_2 : Eq (α := B ⊗[R] A →ₐ[R] C ⧸ I)
  (AlgHom.restrictScalars R (S := B)
      (AlgHom.comp (Ideal.Quotient.mkₐ B I)
        (TensorProduct.productLeftAlgHom (ofId B C)
          (lift I sorry (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) :
    B ⊗[R] A →ₐ[R] C ⧸ I)
  (AlgHom.restrictScalars R f : B ⊗[R] A →ₐ[R] C ⧸ I)
Tactic: apply AlgHom.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ Eq (α := B ⊗[R] A →ₐ[R] C ⧸ I)
    (AlgHom.restrictScalars R (S := B)
        (AlgHom.comp (Ideal.Quotient.mkₐ B I)
          (TensorProduct.productLeftAlgHom (ofId B C)
            (lift I ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) :
      B ⊗[R] A →ₐ[R] C ⧸ I)
    (AlgHom.restrictScalars R f : B ⊗[R] A →ₐ[R] C ⧸ I)
have refine_2 : ∀ (a : B) (b : A),
  Eq (α := C ⧸ I)
    ((AlgHom.restrictScalars R (S := B)
            (AlgHom.comp (Ideal.Quotient.mkₐ B I)
              (TensorProduct.productLeftAlgHom (ofId B C)
                (lift I sorry (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) :
          (a : B ⊗[R] A) → C ⧸ I)
        (a ⊗ₜ[R] b) :
      C ⧸ I)
    ((AlgHom.restrictScalars R f : (a : B ⊗[R] A) → C ⧸ I) (a ⊗ₜ[R] b) : C ⧸ I)
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
⊢ Eq (α := C ⧸ I)
    ((AlgHom.restrictScalars R (S := B)
            (AlgHom.comp (Ideal.Quotient.mkₐ B I)
              (TensorProduct.productLeftAlgHom (ofId B C)
                (lift I ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) :
          (a : B ⊗[R] A) → C ⧸ I)
        (b ⊗ₜ[R] a) :
      C ⧸ I)
    ((AlgHom.restrictScalars R f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
have refine_2 : HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
  (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
Tactic: suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
⊢ HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
      ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
have refine_2 : HSMul.hSMul (β := C ⧸ I) b ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) = (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
Tactic: rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
refine_2 :
  HSMul.hSMul (β := C ⧸ I) b ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
⊢ HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
      ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
have refine_2₁ : Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B ⊗[R] A) b (1 ⊗ₜ[R] a)) : C ⧸ I)
  ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
Tactic: rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R_1 : Type u
A_1 : Type v
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
B_1 : Type u_1
P : Type u_2
C_1 : Type u_3
inst_3 : CommRing B_1
inst_4 : Algebra R_1 B_1
inst_5 : CommRing C_1
inst_6 : Algebra R_1 C_1
inst_7 : CommRing P
inst_8 : Algebra R_1 P
R : Type u_4
inst_9 : CommRing R
A : Type u_5
inst_10 : CommRing A
inst_11 : Algebra R A
B : Type u_6
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : FormallySmooth R A
C : Type (max u_5 u_6)
x : CommRing C
x_1 : Algebra B C
I : Ideal C
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this_1 : Algebra R C :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
refine_2 :
  HSMul.hSMul (β := C ⧸ I) b ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
refine_2₁ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B ⊗[R] A) b (1 ⊗ₜ[R] a)) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
⊢ HMul.hMul (α := C ⧸ I) (β := C ⧸ I) ((algebraMap B (C ⧸ I) : (a : B) → C ⧸ I) b : C ⧸ I)
      ((f : (a : B ⊗[R] A) → C ⧸ I) (1 ⊗ₜ[R] a) : C ⧸ I) =
    (f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a)
have refine_2₂ : Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (HSMul.hSMul (β := B) b 1 ⊗ₜ[R] a) : C ⧸ I)
  ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
Tactic: rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]