awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
refine : P.dimension = n
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
refine ⟨_, _, _, ‹_›, ⟨P, ?_⟩⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
a : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑P.dimension : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
⊢ P.dimension = n

Tactic:
apply Nat.cast_injective (R := Cardinal)

Premises used: Nat.cast_injective
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
a a₁ a₂ a₃ : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
⊢ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑P.dimension : Cardinal.{u_2}) (↑n : Cardinal.{u_2})

Tactic:
rwa [← P.rank_kaehlerDifferential]

Premises used: Algebra.SubmersivePresentation.rank_kaehlerDifferential
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
inl : Subsingleton S → Subsingleton.{u_2 + 1} Ω[S⁄R]
inr : Nontrivial S → Subsingleton.{u_2 + 1} Ω[S⁄R]
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
cases subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
h : Subsingleton S
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
Module.subsingleton S _

Premises used: Module.subsingleton
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
h : Subsingleton S
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
exact Module.subsingleton S _

Premises used: Module.subsingleton
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
h : Nontrivial S
⊢ IsStandardSmooth R S

Tactic:
haveI : IsStandardSmooth R S := IsStandardSmoothOfRelativeDimension.isStandardSmooth 0
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
h : Nontrivial S
this : IsStandardSmooth R S
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
Module.subsingleton_of_rank_zero
    (IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential 0)

Premises used: Module.subsingleton_of_rank_zero, OfNat.ofNat, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmoothOfRelativeDimension 0 R S
h : Nontrivial S
this : IsStandardSmooth R S
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]

Tactic:
exact Module.subsingleton_of_rank_zero
    (IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential 0)

Premises used: Module.subsingleton_of_rank_zero, OfNat.ofNat, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmooth R S
rw : Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)
⊢ FormallySmooth R S

Tactic:
rw [Algebra.formallySmooth_iff]

Premises used: Algebra.formallySmooth_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmooth R S
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)

Tactic:
⟨inferInstance, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardSmooth R S
⊢ Module.Projective S Ω[S⁄R] ∧ Subsingleton (H1Cotangent R S)

Tactic:
exact ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
h : Nontrivial S
obtain : ∀ (n : ℕ) (P : Generators R S (Fin n)), IsStandardSmooth R S
⊢ IsStandardSmooth R S

Tactic:
obtain ⟨n, ⟨P⟩⟩ := (FiniteType.iff_exists_generators (R := R) (S := S)).mp inferInstance

Premises used: inferInstance, Algebra.FiniteType.iff_exists_generators, Iff.mp
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
hb :
  Subset (α := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R]))
    (Set.range (ι := S) (⇑(D R S) : (a : S) → Ω[S⁄R]))
h : Nontrivial S
n : ℕ
P : Generators R S (Fin n)
choose :
  ∀
    (f' :
      ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S)
    (hf' :
      ∀ ⦃a : Ω[S⁄R]⦄
        (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
        (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a),
    IsStandardSmooth R S
⊢ IsStandardSmooth R S

Tactic:
choose f' hf' using hb
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
i : I
⊢ Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])

Tactic:
simp [P, hf']
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
⊢ ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])

Tactic:
have hb (i : I) : b i = D R S (P.val (Sum.inr i)) := by simp [P, hf']
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)

Tactic:
have : Function.Bijective (P.cotangentRestrict _) :=
    P.cotangentRestrict_bijective_of_basis_kaehlerDifferential Sum.inl_injective
      Set.isCompl_range_inl_range_inr.symm b hb
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this }
⊢ Finite I

Tactic:
have : Finite I := Module.Finite.finite_basis b
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
obtain :
  ∀ (Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n))
    (bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent) (hcomp : Q.val ∘ Sum.inr = P.val)
    (hbcot :
      ∀ (r : Unit ⊕ Fin n),
        Eq (α := Q.toExtension.Cotangent)
          ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
              (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
            Q.toExtension.Cotangent)),
    IsStandardSmooth R S
⊢ IsStandardSmooth R S

Tactic:
obtain ⟨Q, bcot, hcomp, hbcot⟩ := P.exists_presentation_of_basis_cotangent bcot'

Premises used: Algebra.Generators.exists_presentation_of_basis_cotangent
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
⊢ IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)

Tactic:
simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]

Premises used: eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
⊢ IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)

Tactic:
have hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map) := by
    simp [P', ← eq_compl_iff_isCompl, Set.ext_iff, Set.mem_compl_iff]
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)
hb₁ :
  ∀ (k : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) k : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P'.val ((Sum.inr ∘ Sum.inr) k)) : Ω[S⁄R])
⊢ Function.Bijective (α := P'.toExtension.Cotangent) (β := Unit ⊕ Fin n →₀ S)
    (⇑(P'.cotangentRestrict ⋯) : (a : P'.toExtension.Cotangent) → Unit ⊕ Fin n →₀ S)

Tactic:
apply P'.cotangentRestrict_bijective_of_basis_kaehlerDifferential P'.map_inj hcompl b

Premises used: Algebra.PreSubmersivePresentation.toPresentation, Algebra.PreSubmersivePresentation.map_inj, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, Algebra.Presentation.toGenerators
-- Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Subsingleton (H1Cotangent R S)
I : Type u_3
b : Module.Basis I S Ω[S⁄R]
h : Nontrivial S
n : ℕ
P_1 : Generators R S (Fin n)
f' : ⦃a : Ω[S⁄R]⦄ → Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a → S
hf' :
  ∀ ⦃a : Ω[S⁄R]⦄ (a_1 : Membership.mem (γ := Set Ω[S⁄R]) (Set.range.{u_2, u_3 + 1} (ι := I) (⇑b : (a : I) → Ω[S⁄R])) a),
    (D R S : (a : S) → Ω[S⁄R]) (f' a_1) = a
P : Generators.{u_3, u_1, u_2} R S (Fin n ⊕ I) := P_1.extend fun (i : I) ↦ f' ⋯
hb :
  ∀ (i : I),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) i : Ω[S⁄R])
      ((D R S : (a : S) → Ω[S⁄R]) (P.val (Sum.inr i)) : Ω[S⁄R])
this_1 :
  Function.Bijective (α := P.toExtension.Cotangent) (β := Fin n →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → Fin n →₀ S)
bcot' : Module.Basis (Fin n) S P.toExtension.Cotangent :=
  { repr := LinearEquiv.ofBijective (P.cotangentRestrict ⋯) this_1 }
this : Finite I
Q : Presentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n)
bcot : Module.Basis (Unit ⊕ Fin n) S Q.toExtension.Cotangent
hcomp : Q.val ∘ Sum.inr = P.val
hbcot :
  ∀ (r : Unit ⊕ Fin n),
    Eq (α := Q.toExtension.Cotangent)
      ((bcot : (a : Unit ⊕ Fin n) → Q.toExtension.Cotangent) r : Q.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥Q.toExtension.ker) → Q.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : Q.toExtension.Ring) ↦ x ∈ Q.toExtension.ker) (Q.relation r) ⋯) :
        Q.toExtension.Cotangent)
P' : PreSubmersivePresentation.{0, u_3, u_1, u_2} R S (Unit ⊕ Fin n ⊕ I) (Unit ⊕ Fin n) :=
  let __spread.0 := Q;
  { toPresentation := __spread.0, map := Sum.map _root_.id Sum.inl, map_inj := ⋯ }
hcompl : IsCompl (Set.range (Sum.inr ∘ Sum.inr)) (Set.range P'.map)
k : I
⊢ Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : I) → Ω[S⁄R]) k : Ω[S⁄R])
    ((D R S : (a : S) → Ω[S⁄R]) (P'.val ((Sum.inr ∘ Sum.inr) k)) : Ω[S⁄R])

Tactic:
simp only [hb, ← hcomp, P', Function.comp_def]

Premises used: Function.comp_def