awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 ι σ
i : ι
hi : i ∉ Set.range P.map
contrapose contrapose₁ :
  ∀ (hi : i ∉ Set.range P.map),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
contrapose₂ contrapose₃ contrapose₄ :
  ∀
    (hi :
      ¬Eq (α := P.toExtension.Cotangent)
          ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
              ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
            P.toExtension.Cotangent)
          (0 : P.toExtension.Cotangent)),
    i ∈ Set.range P.map
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)
have contrapose₅ : ∀
  (hi :
    ¬∀ (i_1 : σ),
        Eq.{u_2 + 1} (α := S)
          ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                    ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
                  ι →₀ S) :
                (a : ι) → S)
              (P.map i_1) :
            S)
          ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) 0 i_1 : S)),
  i ∈ Set.range P.map
Tactic: classical
  contrapose hi
  rw [sectionCotangent_eq_iff] at hi
  simp only [Basis.repr_self, map_zero, Pi.zero_apply, Finsupp.single_apply] at hi
  grind
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 ι σ
i : ι
hi : i ∉ Set.range P.map
contrapose contrapose₁ :
  ∀ (hi : i ∉ Set.range P.map),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
contrapose₂ contrapose₃ contrapose₄ :
  ∀
    (hi :
      ¬Eq (α := P.toExtension.Cotangent)
          ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
              ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
            P.toExtension.Cotangent)
          (0 : P.toExtension.Cotangent)),
    i ∈ Set.range P.map
contrapose₅ :
  ∀
    (hi :
      ¬∀ (i_1 : σ),
          Eq.{u_2 + 1} (α := S)
            ((((P.cotangentSpaceBasis.repr : (a : P.toExtension.CotangentSpace) → ι →₀ S)
                      ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
                    ι →₀ S) :
                  (a : ι) → S)
                (P.map i_1) :
              S)
            ((P.cotangentComplexAux : (a : P.toExtension.Cotangent) → σ → S) 0 i_1 : S)),
    i ∈ Set.range P.map
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) i) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)
have contrapose₆ : ∀ (hi : ¬∀ (i_1 : σ), Eq.{u_2 + 1} (α := S) (if i = P.map i_1 then 1 else 0) 0), i ∈ Set.range P.map
Tactic: classical
  contrapose hi
  rw [sectionCotangent_eq_iff] at hi
  simp only [Basis.repr_self, map_zero, Pi.zero_apply, Finsupp.single_apply] at hi
  grind
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ Basis κ S Ω[S⁄R]
have hsa : ∀ (i : κ),
  Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)
Tactic: apply P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P)
    Extension.exact_cotangentComplex_toKaehler Extension.toKaehler_surjective hf (b := P.map)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
hsa :
  ∀ (i : κ),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
⊢ Basis κ S Ω[S⁄R]
have hlib : 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: apply P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P)
    Extension.exact_cotangentComplex_toKaehler Extension.toKaehler_surjective hf (b := P.map)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
hsa :
  ∀ (i : κ),
    Eq (α := P.toExtension.Cotangent)
      ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
        P.toExtension.Cotangent)
      (0 : P.toExtension.Cotangent)
hlib :
  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))
⊢ Basis κ S Ω[S⁄R]
have hab : Codisjoint (Set.range f) (Set.range P.map)
Tactic: apply P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P)
    Extension.exact_cotangentComplex_toKaehler Extension.toKaehler_surjective hf (b := P.map)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 : κ
⊢ Eq (α := P.toExtension.Cotangent)
    ((P.sectionCotangent : (a : P.toExtension.CotangentSpace) → P.toExtension.Cotangent)
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (f i)) :
      P.toExtension.Cotangent)
    (0 : P.toExtension.Cotangent)
have hsa : f i ∉ Set.range P.map
Tactic: apply sectionCotangent_zero_of_notMem_range _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 := 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))
have 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 sorry) : (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: simp only [sectionCotangent, LinearMap.coe_comp, Function.comp_assoc, LinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 := 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)))))
have apply : LinearIndependent S (M := σ → S)
  (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
    (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map sorry) : (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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
    (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))))
have h : Eq (α := σ → σ → S)
  (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
    (Function.comp (β := ι →₀ S) (⇑(Finsupp.lcomapDomain P.map sorry) : (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: convert! (Pi.basisFun S σ).linearIndependent
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ 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)
have 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 sorry) : (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: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
    (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)
have h : Eq.{u_2 + 1} (α := S)
  ((((Finsupp.lcomapDomain P.map sorry : (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 only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
⊢ 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)
have 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 sorry) : (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: classical
    ext i j
    simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
    simp [Finsupp.single_eq_pi_single]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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)
have h₁ : ∀ (i j : σ),
  Eq.{u_2 + 1} (α := S)
    ((((Finsupp.lcomapDomain P.map sorry : (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: classical
    ext i j
    simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
    simp [Finsupp.single_eq_pi_single]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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 (Set.range (ι := (↑(Set.range P.map)ᶜ : Type u_3)) (Subtype.val (p := fun (x : ι) ↦ x ∈ (Set.range P.map)ᶜ)))
    (Set.range P.map)
have rw : IsCompl {x : ι | x ∈ (Set.range P.map)ᶜ} (Set.range P.map)
Tactic: rw [Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Free S Ω[S⁄R]
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), Free S Ω[S⁄R]
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Subsingleton (H1Cotangent R S)
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1), Finite w → ∀ (P : SubmersivePresentation R S w w_1), Subsingleton (H1Cotangent R S)
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
have 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})
Tactic: obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
have rw : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑P.dimension : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
Tactic: rw [P.rank_kaehlerDifferential, hP]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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})
⊢ Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})
have rw₁ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑n : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
Tactic: rw [P.rank_kaehlerDifferential, hP]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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})
have refine : ∀ (h : Module.rank S Ω[S⁄R] = (↑n : Cardinal.{u_2})), IsStandardSmoothOfRelativeDimension n R S
Tactic: refine ⟨fun h ↦ IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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})
⊢ IsStandardSmoothOfRelativeDimension n R S
have obtain : ∀ (w w_1 : Type) (w_2 : Finite w_1),
  Finite w → ∀ (P : SubmersivePresentation R S w w_1), IsStandardSmoothOfRelativeDimension n R S
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
have refine : P.dimension = n
Tactic: refine ⟨_, _, _, ‹_›, ⟨P, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ P.dimension = n
have a : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑P.dimension : Cardinal.{u_2}) (↑n : Cardinal.{u_2})
Tactic: apply Nat.cast_injective (R := Cardinal)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have inl : Subsingleton S → Subsingleton.{u_2 + 1} Ω[S⁄R]
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (goal)
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]
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have inr : Nontrivial S → Subsingleton.{u_2 + 1} Ω[S⁄R]
Tactic: cases subsingleton_or_nontrivial S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.StandardSmoothCotangent (hypothesis)
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
⊢ Subsingleton.{u_2 + 1} Ω[S⁄R]
have this : IsStandardSmooth R S
Tactic: haveI : IsStandardSmooth R S := IsStandardSmoothOfRelativeDimension.isStandardSmooth 0