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
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
h :
  (∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id
h₁ :
  (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
        (⇑((↑P :
                {S : Type v} →
                  {M : Type (max u_2 v)} →
                    {M₂ : Type v} →
                      [inst : Semiring P] →
                        [inst_8 : Semiring S] →
                          [inst_9 : AddCommMonoid M] →
                            [inst_10 : AddCommMonoid M₂] →
                              [inst_11 : Module P M] →
                                [inst_12 : Module P M₂] →
                                  [inst_13 : Module S M] →
                                    [inst_14 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
              (mapBaseChange R P A)) :
          (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R]) ∧
      ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
        l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
⊢ (Function.Injective (α := Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))) (β := A ⊗[P] Ω[P⁄R])
        (⇑(kerCotangentToTensor R P A) : (a : (RingHom.ker (algebraMap P A)).Cotangent) → A ⊗[P] Ω[P⁄R]) ∧
      ∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
convert!
    (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
          (KaehlerDifferential.mapBaseChange R P A).restrictScalars P)).out
      0 1) using 2

Premises used: Function.Exact.split_tfae', KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, List.TFAE.out, OfNat.ofNat
-- 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
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
h :
  (∃ (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      Eq (α := Ω[A⁄R] →ₗ[A] Ω[A⁄R])
        (mapBaseChange R P A ∘ₗ
          (AddEquiv.toEquiv
                (LinearEquiv.toAddEquiv
                  (LinearMap.extendScalarsOfSurjectiveEquiv hf :
                    (Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) ≃ₗ[P] Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])) :
              (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) → Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])
            a)
        LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id
⊢ (∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id

Tactic:
rw [← (LinearMap.extendScalarsOfSurjectiveEquiv hf).exists_congr_right]

Premises used: Equiv.exists_congr_right, LinearEquiv.toAddEquiv, AddEquiv.toEquiv, LinearMap.extendScalarsOfSurjectiveEquiv
-- 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
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ (∃ (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      Eq (α := Ω[A⁄R] →ₗ[A] Ω[A⁄R])
        (mapBaseChange R P A ∘ₗ
          (AddEquiv.toEquiv
                (LinearEquiv.toAddEquiv
                  (LinearMap.extendScalarsOfSurjectiveEquiv hf :
                    (Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) ≃ₗ[P] Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])) :
              (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) → Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])
            a)
        LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- 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
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
    (⇑((↑P :
            {S : Type v} →
              {M : Type (max u_2 v)} →
                {M₂ : Type v} →
                  [inst : Semiring P] →
                    [inst_8 : Semiring S] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P M] →
                            [inst_12 : Module P M₂] →
                              [inst_13 : Module S M] →
                                [inst_14 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (mapBaseChange R P A)) :
      (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R])

Tactic:
mapBaseChange_surjective R P A hf

Premises used: Quotient.liftOn', AddCon.liftOn, KaehlerDifferential.mapBaseChange_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
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
    (⇑((↑P :
            {S : Type v} →
              {M : Type (max u_2 v)} →
                {M₂ : Type v} →
                  [inst : Semiring P] →
                    [inst_8 : Semiring S] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P M] →
                            [inst_12 : Module P M₂] →
                              [inst_13 : Module S M] →
                                [inst_14 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (mapBaseChange R P A)) :
      (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R])

Tactic:
exact mapBaseChange_surjective R P A hf

Premises used: KaehlerDifferential.mapBaseChange_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
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
h h₁ :
  (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
⊢ (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
        (⇑((↑P :
                {S : Type v} →
                  {M : Type (max u_2 v)} →
                    {M₂ : Type v} →
                      [inst : Semiring P] →
                        [inst_8 : Semiring S] →
                          [inst_9 : AddCommMonoid M] →
                            [inst_10 : AddCommMonoid M₂] →
                              [inst_11 : Module P M] →
                                [inst_12 : Module P M₂] →
                                  [inst_13 : Module S M] →
                                    [inst_14 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
              (mapBaseChange R P A)) :
          (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R]) ∧
      ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
        l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
rw [and_iff_right (by exact mapBaseChange_surjective R P A hf)]

Premises used: and_iff_right
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
⊢ FormallySmooth R A ↔ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
(Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_

Premises used: Algebra.Extension.algebraMap_surjective, Iff.trans, Algebra.FormallySmooth.iff_split_injection
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
refine :
  (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) ↔
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ FormallySmooth R A ↔ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_

Premises used: Algebra.Extension.algebraMap_surjective, Iff.trans, Algebra.FormallySmooth.iff_split_injection
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
r : P.Ring
m : P.ker.Cotangent
e : Cotangent.val (r • m) = r • Cotangent.val m
⊢ Cotangent.val (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl P.ker.Cotangent)) (r • m)) =
    (HSMul.hSMul (α := P.Ring) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) r : P.Ring)
        (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl P.ker.Cotangent)) m)).val

Tactic:
simp
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ Cotangent.val (r • m) = r • Cotangent.val m

Tactic:
rfl
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
mp :
  (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) →
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
mpr :
  (∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id) →
    ∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
⊢ (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) ↔
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
constructor
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l :
  LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
    (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))
hl : l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
⊢ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Premises used: DFunLike.congr_fun, LinearMap.ext, Algebra.Extension.algebraMap_surjective, LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro, LinearMap.extendScalarsOfSurjective
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l :
  LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
    (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))
hl : l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
⊢ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : P.CotangentSpace →ₗ[A] P.Cotangent
hl : l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ ∃ (l :
    LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
      (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
    l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Premises used: LinearEquiv.symm, LinearMap.restrictScalars, DFunLike.congr_fun, LinearMap.ext, Algebra.Extension.Ring, LinearMap.comp, LinearEquiv.toLinearMap, Exists.intro
-- 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 : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : P.CotangentSpace →ₗ[A] P.Cotangent
hl : l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ ∃ (l :
    LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
      (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
    l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩
-- 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
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑f : (a : P) → A)
this : Algebra P A := f.toAlgebra
rw :
  Nonempty
      { g :
        AlgHom.{u, v, u_2} R A
          (P ⧸
            HPow.hPow (α := Ideal P) (β := ℕ)
              (RingHom.ker (F := P →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P A))) 2) //
        AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P A)) g = AlgHom.id R A } ↔
    Nonempty
      { g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2) //
        f.kerSquareLift.comp g = AlgHom.id R A }
⊢ FormallySmooth R A ↔
    ∃ (g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)),
      f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
rw [iff_split_injection hf, ← nonempty_subtype, ← nonempty_subtype,
    (retractionKerCotangentToTensorEquivSection hf).nonempty_congr]

Premises used: nonempty_subtype, Equiv.nonempty_congr, Algebra.FormallySmooth.iff_split_injection, retractionKerCotangentToTensorEquivSection
-- 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
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑f : (a : P) → A)
this : Algebra P A := f.toAlgebra
⊢ Nonempty
      { g :
        AlgHom.{u, v, u_2} R A
          (P ⧸
            HPow.hPow (α := Ideal P) (β := ℕ)
              (RingHom.ker (F := P →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P A))) 2) //
        AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P A)) g = AlgHom.id R A } ↔
    Nonempty
      { g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2) //
        f.kerSquareLift.comp g = AlgHom.id R A }

Tactic:
rfl
-- 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
⊢ FormallySmooth R A

Tactic:
(iff_split_surjection f fun x ↦ ?_).mpr ⟨g, h⟩

Premises used: Iff.mpr, Algebra.FormallySmooth.iff_split_surjection, Exists.intro
-- 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
refine : ∀ (x : A), ∃ (a : P), (f : (a : P) → A) a = x
⊢ FormallySmooth R A

Tactic:
refine (iff_split_surjection f fun x ↦ ?_).mpr ⟨g, h⟩

Premises used: Iff.mpr, Algebra.FormallySmooth.iff_split_surjection, Exists.intro
-- 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:
⟨y, congr(f.kerSquareLift $hy).trans congr($h x)⟩

Premises used: congrArg, id, AlgHom.kerSquareLift, Exists.intro, DFunLike.coe, Eq.trans