awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
i : κ
⊢ f i ∉ Set.range P.map

Tactic:
simp [← hcompl.compl_eq]

Premises used: IsCompl.compl_eq
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
hlib :
  LinearIndependent S (M := P.toExtension.Cotangent)
    (Function.comp (β := σ → S) (⇑P.cotangentEquiv.symm : (a : σ → S) → P.toExtension.Cotangent)
      (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
          (Function.comp (β := P.toExtension.CotangentSpace)
            (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
            ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map)))))
⊢ LinearIndependent S (M := P.toExtension.Cotangent)
    (Function.comp (β := P.toExtension.CotangentSpace)
      (⇑P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
      ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))

Tactic:
simp only [sectionCotangent, LinearMap.coe_comp, Function.comp_assoc, LinearEquiv.coe_coe]

Premises used: LinearMap.coe_comp, Algebra.SubmersivePresentation.sectionCotangent, LinearEquiv.coe_coe, Function.comp_assoc
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
apply :
  LinearIndependent S (M := σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))))
⊢ LinearIndependent S (M := P.toExtension.Cotangent)
    (Function.comp (β := σ → S) (⇑P.cotangentEquiv.symm : (a : σ → S) → P.toExtension.Cotangent)
      (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
          (Function.comp (β := P.toExtension.CotangentSpace)
            (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
            ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map)))))

Tactic:
apply LinearIndependent.map' _ _ P.cotangentEquiv.symm.ker

Premises used: LinearEquiv.symm, Algebra.SubmersivePresentation.cotangentEquiv, LinearIndependent.map', LinearEquiv.ker
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ LinearIndependent (ι := σ) S (M := σ → S) (⇑(Pi.basisFun S σ) : (a : σ) → σ → S)

Tactic:
(Pi.basisFun S σ).linearIndependent

Premises used: Module.Basis.linearIndependent, Pi.basisFun
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
h :
  Eq (α := σ → σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))))
    (⇑(Pi.basisFun S σ) : (a : σ) → σ → S)
⊢ LinearIndependent S (M := σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))))

Tactic:
convert! (Pi.basisFun S σ).linearIndependent

Premises used: Module.Basis.linearIndependent, Pi.basisFun
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
h :
  ∀ (i j : σ),
    Eq.{u_2 + 1} (α := S)
      (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
          (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
            (Function.comp (β := P.toExtension.CotangentSpace)
              (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map)))
          i j :
        S)
      ((Pi.basisFun S σ : (a : σ) → σ → S) i j : S)
⊢ Eq (α := σ → σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))))
    (⇑(Pi.basisFun S σ) : (a : σ) → σ → S)

Tactic:
ext i j
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
i j : σ
h :
  Eq.{u_2 + 1} (α := S)
    ((((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S) (Finsupp.single (P.map i) 1) : σ →₀ S) : (a : σ) → S) j :
      S)
    (Pi.single (M := fun (j : σ) ↦ S) i 1 j : S)
⊢ Eq.{u_2 + 1} (α := S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
          (Function.comp (β := P.toExtension.CotangentSpace)
            (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
            ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map)))
        i j :
      S)
    ((Pi.basisFun S σ : (a : σ) → σ → S) i j : S)

Tactic:
simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]

Premises used: Finsupp.linearEquivFunOnFinite_apply, Pi.basisFun_apply, Function.comp_apply, Module.Basis.repr_self
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
i j : σ
⊢ Eq.{u_2 + 1} (α := S)
    ((((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S) (Finsupp.single (P.map i) 1) : σ →₀ S) : (a : σ) → S) j :
      S)
    (Pi.single (M := fun (j : σ) ↦ S) i 1 j : S)

Tactic:
simp [Finsupp.single_eq_pi_single]

Premises used: Finsupp.single_eq_pi_single
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
h :
  ∀ (i j : σ),
    Eq.{u_2 + 1} (α := S)
      (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
          (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
            (Function.comp (β := P.toExtension.CotangentSpace)
              (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
              ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map)))
          i j :
        S)
      ((Pi.basisFun S σ : (a : σ) → σ → S) i j : S)
h₁ :
  ∀ (i j : σ),
    Eq.{u_2 + 1} (α := S)
      ((((Finsupp.lcomapDomain P.map ⋯ : (a : ι →₀ S) → σ →₀ S) (Finsupp.single (P.map i) 1) : σ →₀ S) : (a : σ) → S)
          j :
        S)
      (Pi.single (M := fun (j : σ) ↦ S) i 1 j : S)
⊢ Eq (α := σ → σ → S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map ⋯) : (a : ι →₀ S) → σ →₀ S)
        (Function.comp (β := P.toExtension.CotangentSpace)
          (⇑P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
          ((⇑P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) ∘ P.map))))
    (⇑(Pi.basisFun S σ) : (a : σ) → σ → S)

Tactic:
classical
    ext i j
    simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
    simp [Finsupp.single_eq_pi_single]

Premises used: Finsupp.linearEquivFunOnFinite_apply, Pi.basisFun_apply, Function.comp_apply, Finsupp.single_eq_pi_single, Module.Basis.repr_self
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ Codisjoint (Set.range f) (Set.range P.map)

Tactic:
hcompl.2

Premises used: IsCompl.codisjoint
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ Codisjoint (Set.range f) (Set.range P.map)

Tactic:
exact hcompl.2

Premises used: IsCompl.codisjoint
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
k : κ
⊢ Eq.{u_2 + 1} (α := Ω[S⁄R]) ((P.basisKaehlerOfIsCompl hf hcompl : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R])
    ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) (P.val (f k)) : Ω[S⁄R])

Tactic:
simp [basisKaehlerOfIsCompl]

Premises used: Algebra.SubmersivePresentation.basisKaehlerOfIsCompl
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
rw : IsCompl {x : ι | x ∈ (Set.range P.map)ᶜ} (Set.range P.map)
⊢ IsCompl (Set.range (ι := (↑(Set.range P.map)ᶜ : Type u_3)) (Subtype.val (p := fun (x : ι) ↦ x ∈ (Set.range P.map)ᶜ)))
    (Set.range P.map)

Tactic:
rw [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ IsCompl {x : ι | x ∈ (Set.range P.map)ᶜ} (Set.range P.map)

Tactic:
IsCompl.symm isCompl_compl

Premises used: isCompl_compl, IsCompl.symm
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ IsCompl {x : ι | x ∈ (Set.range P.map)ᶜ} (Set.range P.map)

Tactic:
exact IsCompl.symm isCompl_compl

Premises used: isCompl_compl, IsCompl.symm
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
k : (↑(Set.range P.map)ᶜ : Type u_3)
⊢ Eq.{u_2 + 1} (α := Ω[S⁄R]) ((P.basisKaehler : (a : (↑(Set.range P.map)ᶜ : Type u_3)) → Ω[S⁄R]) k : Ω[S⁄R])
    ((KaehlerDifferential.D R S : (a : S) → Ω[S⁄R]) (P.val (↑k : ι)) : Ω[S⁄R])

Tactic:
simp [basisKaehler]

Premises used: Algebra.SubmersivePresentation.basisKaehler
-- 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 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Free S Ω[S⁄R]

Tactic:
Module.Free.of_basis P.basisKaehler

Premises used: Module.Free.of_basis, Algebra.SubmersivePresentation.basisKaehler
-- 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 : Finite σ
inst_4 : Nontrivial S
inst_5 : Finite ι
P : SubmersivePresentation R S ι σ
⊢ Module.rank S Ω[S⁄R] = (↑P.dimension : Cardinal.{u_2})

Tactic:
simp only [rank_eq_card_basis P.basisKaehler, Fintype.card_compl_set,
    Presentation.dimension, Nat.card_eq_fintype_card, Set.card_range_of_injective P.map_inj]

Premises used: rank_eq_card_basis, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.map_inj, Set.card_range_of_injective, Fintype.card_compl_set, Algebra.Presentation.dimension, Algebra.SubmersivePresentation.basisKaehler, Nat.card_eq_fintype_card
-- 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
r : R
inst_3 : IsLocalization.Away r S
⊢ Free.{u_2, u_1} S (Cotangent (Generators.toExtension (Generators.localizationAway S r)))

Tactic:
inferInstanceAs <|
    Module.Free S ((SubmersivePresentation.localizationAway S r).toExtension.Cotangent)

Premises used: _private.0.Algebra.instFreeCotangentToExtensionUnitLocalizationAway._proof_1
-- 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
r : R
inst_3 : IsLocalization.Away r S
⊢ Eq (α := Cotangent (toExtension (localizationAway S r))) (cMulXSubOneCotangent S r)
    ((Cotangent.mk : (a : ↥(localizationAway S r).toExtension.ker) → (localizationAway S r).toExtension.Cotangent)
      (Subtype.mk (p := fun (x : Extension.Ring (toExtension (localizationAway S r))) ↦
        Membership.mem (γ := Ideal (Extension.Ring (toExtension (localizationAway S r))))
          (Extension.ker (toExtension (localizationAway S r))) x)
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1)
        ⋯))

Tactic:
rfl

Premises used: rfl
-- 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
r : R
inst_3 : IsLocalization.Away r S
x : Unit
⊢ Eq.{u_1 + 1} (α :=
    Cotangent
      (Generators.toExtension
        (Presentation.toGenerators
          (PreSubmersivePresentation.toPresentation (toPreSubmersivePresentation (localizationAway S r))))))
    ((basisCotangent (localizationAway S r) : (a : Unit) → (localizationAway S r).toExtension.Cotangent) x :
      Cotangent
        (Generators.toExtension
          (Presentation.toGenerators
            (PreSubmersivePresentation.toPresentation (toPreSubmersivePresentation (localizationAway S r))))))
    (Generators.cMulXSubOneCotangent S r : Cotangent (Generators.toExtension (Generators.localizationAway S r)))

Tactic:
basisCotangent_apply _ _

Premises used: Set.Mem, Algebra.SubmersivePresentation.basisCotangent_apply, Algebra.Generators.localizationAway
-- 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
r : R
inst_3 : IsLocalization.Away r S
x : Unit
⊢ Eq.{u_1 + 1} (α := Cotangent (toExtension (localizationAway S r)))
    ((basisCotangentAway S r : (a : Unit) → (localizationAway S r).toExtension.Cotangent) x :
      Cotangent (toExtension (localizationAway S r)))
    (cMulXSubOneCotangent S r : Cotangent (toExtension (localizationAway S r)))

Tactic:
SubmersivePresentation.basisCotangent_apply _ _

Premises used: Set.Mem, Algebra.SubmersivePresentation.basisCotangent_apply, Algebra.Generators.localizationAway
-- 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
obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), Free S Ω[S⁄R]
⊢ Free S Ω[S⁄R]

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- 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
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ Free S Ω[S⁄R]

Tactic:
P.free_kaehlerDifferential

Premises used: Algebra.SubmersivePresentation.free_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
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ Free S Ω[S⁄R]

Tactic:
exact P.free_kaehlerDifferential

Premises used: Algebra.SubmersivePresentation.free_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
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w → ∀ (P : SubmersivePresentation R S w w_1), Subsingleton (H1Cotangent R S)
⊢ Subsingleton (H1Cotangent R S)

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- 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
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ Subsingleton (H1Cotangent R S)

Tactic:
P.equivH1Cotangent.symm.toEquiv.subsingleton

Premises used: LinearEquiv.symm, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Generators.equivH1Cotangent, LinearEquiv.toEquiv, Equiv.subsingleton, Algebra.Presentation.toGenerators
-- 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
w w_1 : Type
w_2 : Finite w_1
left : Finite w
P : SubmersivePresentation R S w w_1
⊢ Subsingleton (H1Cotangent R S)

Tactic:
exact P.equivH1Cotangent.symm.toEquiv.subsingleton

Premises used: LinearEquiv.symm, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Generators.equivH1Cotangent, LinearEquiv.toEquiv, Equiv.subsingleton, Algebra.Presentation.toGenerators
-- 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
n : ℕ
inst_4 : IsStandardSmoothOfRelativeDimension n R S
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w →
      ∀ (P : SubmersivePresentation R S w w_1) (hP : P.dimension = n), Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
⊢ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})

Tactic:
obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Premises used: Algebra.IsStandardSmoothOfRelativeDimension
-- 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
n : ℕ
inst_4 : IsStandardSmoothOfRelativeDimension n R S
w w_1 : Type
w_2 : Finite w_1
w_3 : Finite w
P : SubmersivePresentation R S w w_1
hP : P.dimension = n
rw : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑P.dimension : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
rw₁ rw₂ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑n : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
⊢ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})

Tactic:
rw [P.rank_kaehlerDifferential, hP]

Premises used: Algebra.SubmersivePresentation.rank_kaehlerDifferential
-- 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 : ℕ
⊢ IsStandardSmoothOfRelativeDimension n R S ↔ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})

Tactic:
⟨fun h ↦ IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential _, fun h ↦ ?_⟩

Premises used: Iff.intro, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential
-- 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 : ℕ
refine : ∀ (h : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})), IsStandardSmoothOfRelativeDimension n R S
⊢ IsStandardSmoothOfRelativeDimension n R S ↔ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})

Tactic:
refine ⟨fun h ↦ IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential _, fun h ↦ ?_⟩
-- 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})
obtain :
  ∀ (w w_1 : Type) (w_2 : Finite w_1),
    Finite w → ∀ (P : SubmersivePresentation R S w w_1), IsStandardSmoothOfRelativeDimension n R S
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›

Premises used: Algebra.IsStandardSmooth
-- 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
⊢ IsStandardSmoothOfRelativeDimension n R S

Tactic:
⟨_, _, _, ‹_›, ⟨P, ?_⟩⟩

Premises used: Exists.intro, Algebra.IsStandardSmoothOfRelativeDimension.mk