awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Basic
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 :
  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))
⊢ Eq (α := A →ₐ[R] C) (g.comp (IsScalarTower.toAlgHom R A B)) (IsScalarTower.toAlgHom R A C)

Tactic:
apply Algebra.FormallyUnramified.comp_injective _ hI

Premises used: Algebra.FormallyUnramified.comp_injective
-- Module: Mathlib.RingTheory.Smooth.Basic
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 :
  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))
⊢ 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:
rw [← AlgHom.comp_assoc, hg]

Premises used: AlgHom.comp_assoc
-- Module: Mathlib.RingTheory.Smooth.Basic
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 (AlgHom.restrictScalars R f) (IsScalarTower.toAlgHom R A B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A C))

Tactic:
AlgHom.ext f.commutes

Premises used: AlgHom.ext, AlgHom.commutes
-- Module: Mathlib.RingTheory.Smooth.Basic
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 (AlgHom.restrictScalars R f) (IsScalarTower.toAlgHom R A B))
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) (IsScalarTower.toAlgHom R A C))

Tactic:
exact AlgHom.ext f.commutes

Premises used: AlgHom.ext
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
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))
⊢ FormallySmooth 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]

Premises used: Algebra.ofId, Algebra.FormallySmooth.iff_split_surjection
-- Module: Mathlib.RingTheory.Smooth.Basic
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))
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
⊢ (∃ (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
-- Module: Mathlib.RingTheory.Smooth.Basic
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
hg : AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.Basic
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
hg : AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2 :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Injective.{u_6 + 1, u_4 + 1} (α := A) (β :=
    R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2)
    (⇑(↑(↑e : A →ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2) : A →+* R ⧸ RingHom.ker (algebraMap R A) ^ 2) :
      (a : A) → R ⧸ RingHom.ker (algebraMap R A) ^ 2)

Tactic:
e.injective

Premises used: AlgEquiv.injective
-- Module: Mathlib.RingTheory.Smooth.Basic
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
hg : AlgHom.comp (AlgHom.kerSquareLift (ofId R A)) g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2 :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Injective.{u_6 + 1, u_4 + 1} (α := A) (β :=
    R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2)
    (⇑(↑(↑e : A →ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2) : A →+* R ⧸ RingHom.ker (algebraMap R A) ^ 2) :
      (a : A) → R ⧸ RingHom.ker (algebraMap R A) ^ 2)

Tactic:
exact e.injective

Premises used: AlgEquiv.injective
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
H : IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
e : (R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2) ≃ₐ[R] A :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
H : IsIdempotentElem (M := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A))
e : (R ⧸ HPow.hPow (α := Ideal R) (β := ℕ) (RingHom.ker (F := R →+* A) (algebraMap R A)) 2) ≃ₐ[R] A :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ (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:
exact ⟨e.symm.toAlgHom, AlgHom.ext <| h.forall.mpr fun x ↦ by simp⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
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)

Tactic:
.of_comp_surjective fun C _ _ I hI f ↦ ?_

Premises used: Algebra.FormallySmooth.of_comp_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
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
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
⊢ FormallySmooth B (B ⊗[R] A)

Tactic:
refine .of_comp_surjective fun C _ _ I hI f ↦ ?_
-- Module: Mathlib.RingTheory.Smooth.Basic
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))
⊢ IsScalarTower R B C

Tactic:
haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.Smooth.Basic
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

Tactic:
⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) ?_, ?_⟩

Premises used: Algebra.ofId, Exists.intro, Algebra.TensorProduct.productLeftAlgHom
-- Module: Mathlib.RingTheory.Smooth.Basic
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
refine_2 :
  AlgHom.comp (Ideal.Quotient.mkₐ B I)
      (TensorProduct.productLeftAlgHom (ofId B C)
        (lift I ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight))) =
    f
⊢ ∃ (a : B ⊗[R] A →ₐ[B] C), AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f

Tactic:
refine ⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) ?_, ?_⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
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 →ₐ[R] C

Tactic:
exact FormallySmooth.lift I ⟨2, hI⟩ ((f.restrictScalars R).comp TensorProduct.includeRight)

Premises used: AlgHom.restrictScalars, Algebra.FormallySmooth.lift, Exists.intro, AlgHom.comp, OfNat.ofNat, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.Smooth.Basic
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_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 ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) :
      B ⊗[R] A →ₐ[R] C ⧸ I)
    (AlgHom.restrictScalars R f : B ⊗[R] A →ₐ[R] C ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ B I)
      (TensorProduct.productLeftAlgHom (ofId B C)
        (lift I ⋯ (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight))) =
    f

Tactic:
apply AlgHom.restrictScalars_injective R

Premises used: AlgHom.restrictScalars_injective
-- Module: Mathlib.RingTheory.Smooth.Basic
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_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 ⋯ (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)
⊢ 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)

Tactic:
apply TensorProduct.ext'

Premises used: Algebra.TensorProduct.ext'
-- Module: Mathlib.RingTheory.Smooth.Basic
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_2 : IsScalarTower R B C
b : B
a : A
this :
  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)
⊢ 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)

Tactic:
simpa [Algebra.ofId_apply]

Premises used: Algebra.ofId_apply
-- Module: Mathlib.RingTheory.Smooth.Basic
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 :
  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)
⊢ 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)

Tactic:
suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
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)
refine_2₃ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) ((b * 1) ⊗ₜ[R] a) : C ⧸ I)
    ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[R] a) : C ⧸ I)
refine_2₄ refine_2₅ :
  Eq (α := C ⧸ I) ((f : (a : B ⊗[R] A) → C ⧸ I) (b ⊗ₜ[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)

Tactic:
rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul', Algebra.smul_def, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
⊢ FormallySmooth R Rₘ

Tactic:
.of_comp_surjective fun Q _ _ I e f ↦ ?_

Premises used: Algebra.FormallySmooth.of_comp_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
Rₘ : Type u_6
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
refine :
  ∀ (Q : Type (max u_4 u_6)) (x : CommRing Q) (x_1 : Algebra R Q) (I : Ideal Q) (e : HPow.hPow (β := ℕ) I 2 = ⊥)
    (f : Rₘ →ₐ[R] Q ⧸ I), ∃ (a : Rₘ →ₐ[R] Q), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
⊢ FormallySmooth R Rₘ

Tactic:
refine .of_comp_surjective fun Q _ _ I e f ↦ ?_