awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
f : P →ₐ[R] A
g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)
h : f.kerSquareLift.comp g = AlgHom.id R A
x : A
y : P
hy :
  Eq (α := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)
    ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : P) → P ⧸ RingHom.ker f.toRingHom ^ 2)
        y :
      P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)
    ((g : (a : A) → P ⧸ RingHom.ker f.toRingHom ^ 2) x :
      P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)
⊢ ∃ (a : P), (f : (a : P) → A) a = x

Tactic:
exact ⟨y, congr(f.kerSquareLift $hy).trans congr($h x)⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
rw :
  ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
⊢ FormallySmooth R A

Tactic:
rw [iff_split_surjection f P.algebraMap_surjective]

Premises used: Algebra.Generators.algebraMap_surjective, Algebra.FormallySmooth.iff_split_surjection
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)

Tactic:
have surj : Function.Surjective f.kerSquareLift :=
    Ideal.Quotient.lift_surjective_of_surjective _ _ P.algebraMap_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
rw :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (Ideal.cotangentIdeal (RingHom.ker f.toRingHom)) 2 =
    ⊥
rw₁ rw₂ : Eq (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) ⊥ ⊥
⊢ HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift.toRingHom) 2 =
    ⊥

Tactic:
rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]

Premises used: AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
⊢ HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift.toRingHom) 2 =
    ⊥

Tactic:
have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥ := by
    rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
obtain :
  ∀ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
    (hg :
      AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
        (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
          A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)),
    ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
      f.kerSquareLift.comp g = AlgHom.id R A
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
obtain ⟨g, hg⟩ := H _ sqz (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2
hg :
  AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
      A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
⟨g, AlgHom.ext fun x ↦ congr(f.kerSquareLift.kerLift ($hg x)).trans ?_⟩

Premises used: congrArg, id, AlgHom.ext, AlgHom.kerSquareLift, AlgHom.toRingHom, Exists.intro, RingHom.kerLift, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2
hg :
  AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
      A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
refine :
  ∀ (x : A),
    Eq.{v + 1} (α := A)
      ((f.kerSquareLift.kerLift :
            (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift.toRingHom) → A)
          (((↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
                  A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) :
                (a : A) → (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
              x :
            HasQuotient.Quotient (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (B :=
              Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2))
              (RingHom.ker f.kerSquareLift)) :
        A)
      ((AlgHom.id R A : (a : A) → A) x : A)
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
refine ⟨g, AlgHom.ext fun x ↦ congr(f.kerSquareLift.kerLift ($hg x)).trans ?_⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2
hg :
  AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
      A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
x : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2
⊢ Eq.{v + 1} (α := A)
    ((RingHom.kerLift (↑f.kerSquareLift : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2 →+* A) :
          (a :
              (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸
                RingHom.ker (↑f.kerSquareLift : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2 →+* A)) →
            A)
        ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
              (a : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) →
                (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift)
            x :
          HasQuotient.Quotient
            (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2)
            (B :=
            Ideal
              (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2))
            (RingHom.ker f.kerSquareLift)) :
      A)
    ((Ideal.quotientKerAlgEquivOfSurjective surj :
          (a : (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
        ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
              (a : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) →
                (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift)
            x :
          HasQuotient.Quotient
            (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2)
            (B :=
            Ideal
              (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2))
            (RingHom.ker f.kerSquareLift)) :
      A)

Tactic:
simp only [Ideal.quotientKerAlgEquivOfSurjective_apply]

Premises used: Ideal.quotientKerAlgEquivOfSurjective_apply
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FormallySmooth R A ↔
    ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      HPow.hPow (β := ℕ) I 2 = ⊥ →
        Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
⟨fun _ _ ↦ comp_surjective R A, of_comp_surjective⟩

Premises used: Algebra.FormallySmooth.comp_surjective, Algebra.FormallySmooth.of_comp_surjective, Iff.intro
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ FormallySmooth R B

Tactic:
(iff_split_surjection e.toAlgHom e.surjective).mpr
    ⟨(Ideal.Quotient.mkₐ _ _).comp e.symm, AlgHom.ext e.apply_symm_apply⟩

Premises used: Iff.mpr, AlgEquiv.toAlgHom, AlgEquiv.symm, AlgEquiv.apply_symm_apply, AlgHom.ext, Algebra.FormallySmooth.iff_split_surjection, Exists.intro, AlgHom.comp, Ideal.Quotient.mkₐ, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
B : Type u_6
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ FormallySmooth R A ↔ FormallySmooth R B

Tactic:
⟨fun _ ↦ of_equiv e, fun _ ↦ of_equiv e.symm⟩

Premises used: AlgEquiv.symm, Algebra.FormallySmooth.of_equiv, Iff.intro
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R_1 : Type u
A : Type v
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : Algebra R_1 A
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R_1 B
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
⊢ FormallySmooth R R[X]

Tactic:
.of_equiv (MvPolynomial.uniqueAlgEquiv.{_, 0} R PUnit)

Premises used: MvPolynomial.uniqueAlgEquiv, Algebra.FormallySmooth.of_equiv, PUnit
-- Module: Mathlib.RingTheory.Smooth.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
⊢ FormallySmooth R R

Tactic:
.of_equiv (MvPolynomial.isEmptyAlgEquiv R Empty)

Premises used: Algebra.FormallySmooth.of_equiv, MvPolynomial.isEmptyAlgEquiv, Empty
-- 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 : FormallySmooth R A
inst_8 : FormallySmooth A B
⊢ FormallySmooth R B

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

Premises used: Algebra.FormallySmooth.of_comp_surjective
-- 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 : FormallySmooth R A
inst_8 : FormallySmooth A B
refine :
  ∀ (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
⊢ FormallySmooth R B

Tactic:
refine .of_comp_surjective fun C _ _ I hI f ↦ ?_
-- 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 : 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
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
⊢ ∃ (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))

Premises used: IsScalarTower.toAlgHom, Algebra.FormallySmooth.comp_surjective, AlgHom.comp
-- 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 : 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
obtain :
  ∀ (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
⊢ ∃ (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 }

Premises used: Algebra.FormallySmooth.comp_surjective, AlgHom.toRingHom, AlgHom.congr_fun, AlgHom.mk, Eq.symm
-- 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 : 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 }
⊢ 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' := ⋯ })

Tactic:
apply_fun AlgHom.restrictScalars R at e'

Premises used: AlgHom.restrictScalars
-- 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 : 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' :
  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' := ⋯ })
⊢ ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f

Tactic:
⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩

Premises used: AlgHom.ext, AlgHom.restrictScalars, Exists.intro, rfl, Eq.trans
-- 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 : 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' :
  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' := ⋯ })
⊢ ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f

Tactic:
exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩
-- 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
⊢ FormallySmooth A B

Tactic:
iff_comp_surjective.mpr fun C _ _ I hI f ↦ ?_

Premises used: Iff.mpr, Algebra.FormallySmooth.iff_comp_surjective
-- 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
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
⊢ FormallySmooth A B

Tactic:
refine iff_comp_surjective.mpr fun C _ _ I hI f ↦ ?_

Premises used: Iff.mpr, Algebra.FormallySmooth.iff_comp_surjective
-- 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 := ⋯
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
⊢ ∃ (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)

Premises used: Algebra.FormallySmooth.comp_surjective, AlgHom.restrictScalars
-- 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
suffices : Eq (α := A →ₐ[R] C) (g.comp (IsScalarTower.toAlgHom R A B)) (IsScalarTower.toAlgHom R A C)
⊢ ∃ (a : B →ₐ[A] C), AlgHom.comp (Ideal.Quotient.mkₐ A I) a = f

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)⟩