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
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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
change : HPow.hPow (β := ℕ) P₁.ker 2 ≤ RingHom.ker lift
⊢ ∀ a ∈ HPow.hPow (β := ℕ) P₁.ker 2,
    Eq.{u_5 + 1} (α := P₂.infinitesimal.Ring) ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) a : P₂.infinitesimal.Ring)
      (0 : P₂.infinitesimal.Ring)

Tactic:
change P₁.ker ^ 2 ≤ RingHom.ker lift

Premises used: Algebra.Extension.ker, RingHom.ker
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
rw : ∀ r ∈ P₁.ker, ∀ s ∈ P₁.ker, Membership.mem (γ := Ideal P₁.Ring) (RingHom.ker lift) (r * s)
⊢ HPow.hPow (β := ℕ) P₁.ker 2 ≤ RingHom.ker lift

Tactic:
rw [pow_two, Ideal.mul_le]

Premises used: pow_two, Ideal.mul_le
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ r ∈ P₁.ker,
    Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)

Tactic:
have : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker :=
          fun r hr ↦ (FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ r).trans hr
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this :
  ∀ r ∈ P₁.ker,
    Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
rw :
  HMul.hMul (α := P₂.infinitesimal.Ring) (β := P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) s : P₂.infinitesimal.Ring) ∈
    P₂.infinitesimal.ker * P₂.infinitesimal.ker
⊢ Membership.mem (γ := Ideal P₁.Ring) (RingHom.ker lift) (r * s)

Tactic:
rw [RingHom.mem_ker, map_mul, ← Ideal.mem_bot, ← P₂.ker.cotangentIdeal_square,
          ← ker_infinitesimal, pow_two]

Premises used: Ideal.mem_bot, pow_two, Algebra.Extension.ker, RingHom.mem_ker, Algebra.Extension.ker_infinitesimal, map_mul, 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
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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this :
  ∀ r ∈ P₁.ker,
    Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
⊢ HMul.hMul (α := P₂.infinitesimal.Ring) (β := P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) s : P₂.infinitesimal.Ring) ∈
    P₂.infinitesimal.ker * P₂.infinitesimal.ker

Tactic:
Ideal.mul_mem_mul (this r hr) (this s hs)

Premises used: Set.Mem, Ideal.mul_mem_mul
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this :
  ∀ r ∈ P₁.ker,
    Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
⊢ HMul.hMul (α := P₂.infinitesimal.Ring) (β := P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) s : P₂.infinitesimal.Ring) ∈
    P₂.infinitesimal.ker * P₂.infinitesimal.ker

Tactic:
exact Ideal.mul_mem_mul (this r hr) (this s hs)

Premises used: Ideal.mul_mem_mul
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ (x : R),
    Eq.{u_5 + 1} (α := P₂.infinitesimal.Ring)
      (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
              RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
            (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
          ((algebraMap R P₁.infinitesimal.Ring : (a : R) → P₁.infinitesimal.Ring) x) :
        P₂.infinitesimal.Ring)
      ((algebraMap R P₂.infinitesimal.Ring : (a : R) → P₂.infinitesimal.Ring) ((algebraMap R R : (a : R) → R) x) :
        P₂.infinitesimal.Ring)

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
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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.infinitesimal.Ring
obtain :
  ∀ (x : P₁.Ring),
    Eq (α := A)
      ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
          (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
                  RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
                (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
              ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x) :
            P₂.infinitesimal.Ring) :
        A)
      ((algebraMap A A : (a : A) → A)
          ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A)
              ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x :
                P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) :
            A) :
        A)
⊢ Eq (α := A)
    ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
        (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
                RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
              (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
            x :
          P₂.infinitesimal.Ring) :
      A)
    ((algebraMap A A : (a : A) → A) ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A) x : A) : A)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, 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
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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.Ring
⊢ Eq (α := A)
    ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
        (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
                RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
              (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x) :
          P₂.infinitesimal.Ring) :
      A)
    ((algebraMap A A : (a : A) → A)
        ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x :
              P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) :
          A) :
      A)

Tactic:
FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ x

Premises used: Quotient.liftOn', AddCon.liftOn, IsScalarTower.toAlgHom, Algebra.Extension.Ring, Algebra.FormallySmooth.liftOfSurjective_apply, Algebra.Extension.infinitesimal
-- 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.Ring
⊢ Eq (α := A)
    ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
        (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
                RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
              (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x) :
          P₂.infinitesimal.Ring) :
      A)
    ((algebraMap A A : (a : A) → A)
        ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x :
              P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) :
          A) :
      A)

Tactic:
exact FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ x

Premises used: IsScalarTower.toAlgHom, Algebra.Extension.Ring, Algebra.FormallySmooth.liftOfSurjective_apply, Algebra.Extension.infinitesimal
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
h :
  ∀ (x : P₁.H1Cotangent),
    Eq.{u_5 + 1} (α := P₂.H1Cotangent)
      (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
          x :
        P₂.H1Cotangent)
      ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
⊢ (↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) = map f

Tactic:
ext1 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
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)

Tactic:
(LinearEquiv.symm_apply_eq _).mpr ?_

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
h :
  Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
    (((↑(LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.ofBijective (map P₁.toInfinitesimal) ⋯)
                (equiv (P₁.homInfinitesimal P₂) (P₂.homInfinitesimal P₁))) :
            P₁.H1Cotangent →ₗ[A] P₂.infinitesimal.H1Cotangent) :
          (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
        x :
      P₂.infinitesimal.H1Cotangent)
    ((LinearEquiv.ofBijective (map P₂.toInfinitesimal) ⋯ : (a : P₂.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
        ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x) :
      P₂.infinitesimal.H1Cotangent)
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)

Tactic:
refine (LinearEquiv.symm_apply_eq _).mpr ?_

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
rw :
  Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)

Tactic:
rw [← equivOfFormallySmooth_toLinearMap, LinearEquiv.coe_coe]

Premises used: Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap, LinearEquiv.coe_coe
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
⊢ (equivOfFormallySmooth P₁ P₂).symm = equivOfFormallySmooth P₂ P₁

Tactic:
rfl

Premises used: Algebra.Extension.H1Cotangent.equivOfFormallySmooth, LinearEquiv.symm, Classical.choose, LinearEquiv.trans, 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.{u_4, u, v} R A
inst_3 : FormallySmooth.{u, u_4} R P.Ring
rw : Subsingleton.{u_4 + 1} P.H1Cotangent ↔ Subsingleton (H1Cotangent R A)
rw₁ rw₂ : Subsingleton (H1Cotangent R A) ↔ Subsingleton (H1Cotangent R A)
⊢ Function.Injective (α := P.Cotangent) (β := P.CotangentSpace)
      (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) ↔
    Subsingleton (H1Cotangent R A)

Tactic:
rw [← Algebra.Extension.subsingleton_h1Cotangent,
    P.equivH1CotangentOfFormallySmooth.subsingleton_congr]

Premises used: Algebra.Extension.subsingleton_h1Cotangent, Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, Algebra.Extension.equivH1CotangentOfFormallySmooth, AddEquiv.toEquiv
-- 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.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]) ↔
    Subsingleton (H1Cotangent R A)

Tactic:
let P' : Algebra.Extension R A := ⟨P, _, Function.surjInv_eq hf⟩
  have : Algebra.FormallySmooth R P'.Ring := ‹_›
  P'.cotangentComplex_injective_iff

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Ideal.Cotangent, Function.surjInv, Function.surjInv_eq, Algebra.Extension.mk, Algebra.Extension.cotangentComplex_injective_iff, Submodule.quotientRel, Algebra.Extension.Cotangent
-- 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)
rw :
  (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
⊢ FormallySmooth R A ↔
    ∃ (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 [formallySmooth_iff, and_comm,
    Module.Projective.iff_split_of_projective (KaehlerDifferential.mapBaseChange R P A)
      (mapBaseChange_surjective R P A hf), ← kerCotangentToTensor_injective_iff hf]

Premises used: KaehlerDifferential.mapBaseChange_surjective, and_comm, KaehlerDifferential.mapBaseChange, Module.Projective.iff_split_of_projective, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, Algebra.formallySmooth_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.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]) ∧
      ∃ (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) ↔
    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:
(((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
          (KaehlerDifferential.mapBaseChange R P A).restrictScalars P)).out
      0 1)

Premises used: Function.Exact.split_tfae', KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, List.TFAE.out, OfNat.ofNat