awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
hf : Function.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(LinearMap.linearProjOfIsCompl (E := ι →₀ S) (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
              (F := σ →₀ S) (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
            f :
          P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
      (a : P.toExtension.Cotangent) → σ →₀ S)
have hker : Disjoint g.ker (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
Tactic: apply LinearMap.linearProjOfIsCompl_comp_bijective_of_exact hfg
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
hf : Function.Injective (α := P.toExtension.Cotangent) (β := ι →₀ S) (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S)
hker : Disjoint g.ker (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(LinearMap.linearProjOfIsCompl (E := ι →₀ S) (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
              (F := σ →₀ S) (Finsupp.lmapDomain S S u) ⋯ ⋯ ∘ₗ
            f :
          P.toExtension.Cotangent →ₗ[S] σ →₀ S) :
      (a : P.toExtension.Cotangent) → σ →₀ S)
have hmap : Submodule.map g (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) = ⊤
Tactic: apply LinearMap.linearProjOfIsCompl_comp_bijective_of_exact hfg
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
⊢ Disjoint g.ker (Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1))
have hker : (P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
    Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1) =
  ⊥
Tactic: simp only [disjoint_iff, g]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
⊢ (P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
      Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1) =
    ⊥
have hker : Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
    ((P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
      Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) =
  Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
Tactic: apply Submodule.map_injective_of_injective (f := P.cotangentSpaceBasis.repr.symm.toLinearMap)
      P.cotangentSpaceBasis.repr.symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
      ((P.toExtension.toKaehler ∘ₗ
            (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
        Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
have hker : P.toExtension.toKaehler.ker ⊓
    Submodule.span S
      (Set.range fun (x : κ) ↦
        ((↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
            (a : ι →₀ S) → P.toExtension.CotangentSpace)
          (Finsupp.single (v x) 1)) =
  Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
Tactic: rw [Submodule.map_inf P.cotangentSpaceBasis.repr.symm.toLinearMap
        P.cotangentSpaceBasis.repr.symm.injective, Submodule.map_span, ← Set.range_comp,
        Function.comp_def, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
hk :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
inst_3 : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S :=
  (↑P.cotangentSpaceBasis.repr : P.toExtension.CotangentSpace →ₗ[S] ι →₀ S) ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] :=
  P.toExtension.toKaehler ∘ₗ (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
hfg :
  Function.Exact (M := P.toExtension.Cotangent) (N := ι →₀ S) (P := Ω[S⁄R])
    (⇑f : (a : P.toExtension.Cotangent) → ι →₀ S) (⇑g : (a : ι →₀ S) → Ω[S⁄R])
hker :
  P.toExtension.toKaehler.ker ⊓
      Submodule.span S
        (Set.range fun (x : κ) ↦
          ((↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
              (a : ι →₀ S) → P.toExtension.CotangentSpace)
            (Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
⊢ Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)
      ((P.toExtension.toKaehler ∘ₗ
            (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace)).ker ⊓
        Submodule.span S (Set.range fun (x : κ) ↦ Finsupp.single (v x) 1)) =
    Submodule.map (↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) ⊥
have hker₁ : Function.Surjective (α := ι →₀ S) (β := P.toExtension.CotangentSpace)
  (⇑(↑P.cotangentSpaceBasis.repr.symm : (ι →₀ S) →ₗ[S] P.toExtension.CotangentSpace) :
    (a : ι →₀ S) → P.toExtension.CotangentSpace)
Tactic: rw [Submodule.map_inf P.cotangentSpaceBasis.repr.symm.toLinearMap
        P.cotangentSpaceBasis.repr.symm.injective, Submodule.map_span, ← Set.range_comp,
        Function.comp_def, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
⊢ Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
have rw : ∀
  x ∈
    P.toExtension.toKaehler.ker ⊓
      Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)),
  x = 0
Tactic: rw [disjoint_iff, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
x : P.toExtension.CotangentSpace
⊢ x ∈
      P.toExtension.toKaehler.ker ⊓
        Submodule.span S
          (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)) →
    x = 0
have this : ∀ (hx : x ∈ (↑P.toExtension.toKaehler.ker : Set P.toExtension.CotangentSpace))
  (hxs :
    x ∈
      (↑(Submodule.span S
            (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x))) :
        Set P.toExtension.CotangentSpace)),
  x = 0
Tactic: ⟨hx, hxs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ (↑P.toExtension.toKaehler.ker : Set P.toExtension.CotangentSpace)
hxs :
  x ∈
    (↑(Submodule.span S
          (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x))) :
      Set P.toExtension.CotangentSpace)
⊢ x = 0
have hxs₁ : ∃ (c : κ →₀ S),
  (c.sum fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace)) =
    x
Tactic: rw [SetLike.mem_coe, Finsupp.mem_span_range_iff_exists_finsupp] at hxs
Cleared hypotheses: hxs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ (↑P.toExtension.toKaehler.ker : Set P.toExtension.CotangentSpace)
hxs :
  ∃ (c : κ →₀ S),
    (c.sum fun (i : κ) (a : S) ↦
        HSMul.hSMul (β := P.toExtension.CotangentSpace) a
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace)) =
      x
⊢ x = 0
have obtain : ∀ (c : κ →₀ S)
  (hx :
    (c.sum fun (i : κ) (a : S) ↦
        HSMul.hSMul (β := P.toExtension.CotangentSpace) a
          ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace)) ∈
      (↑P.toExtension.toKaehler.ker : Set P.toExtension.CotangentSpace)),
  Eq (α := P.toExtension.CotangentSpace)
    (c.sum fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace))
    0
Tactic: obtain ⟨c, rfl⟩ := hxs
Cleared hypotheses: x, hx, hxs
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
c : κ →₀ S
hx :
  (c.sum fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace)) ∈
    (↑P.toExtension.toKaehler.ker : Set P.toExtension.CotangentSpace)
⊢ Eq (α := P.toExtension.CotangentSpace)
    (c.sum fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace))
    0
have hx₁ : Eq (α := Ω[S⁄R])
  (c.sum fun (a : κ) (b : S) ↦ HSMul.hSMul (β := Ω[S⁄R]) b ((D R S : (a : S) → Ω[S⁄R]) (P.val (v a)) : Ω[S⁄R])) 0
Tactic: simp only [SetLike.mem_coe, LinearMap.mem_ker, map_finsuppSum, map_smul,
    toKaehler_cotangentSpaceBasis] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
c : κ →₀ S
hx :
  Eq (α := Ω[S⁄R])
    (c.sum fun (a : κ) (b : S) ↦ HSMul.hSMul (β := Ω[S⁄R]) b ((D R S : (a : S) → Ω[S⁄R]) (P.val (v a)) : Ω[S⁄R])) 0
⊢ Eq (α := P.toExtension.CotangentSpace)
    (c.sum fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace))
    0
have obtain : ∀
  (hx :
    Eq.{u_2 + 1} (α := Ω[S⁄R])
      (Finsupp.sum 0 fun (a : κ) (b : S) ↦
        HSMul.hSMul (β := Ω[S⁄R]) b ((D R S : (a : S) → Ω[S⁄R]) (P.val (v a)) : Ω[S⁄R]))
      0),
  Eq (α := P.toExtension.CotangentSpace)
    (Finsupp.sum 0 fun (i : κ) (a : S) ↦
      HSMul.hSMul (β := P.toExtension.CotangentSpace) a
        ((P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v i) : P.toExtension.CotangentSpace))
    0
Tactic: obtain rfl := (linearIndependent_iff.mp h) c hx
Cleared hypotheses: c, hx
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb :
  ∀ (k : κ),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (P.val (v k)) : Ω[S⁄R])
inst_3 : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict hu) : (a : P.toExtension.Cotangent) → σ →₀ S)
have refine_1 : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
Tactic: refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb :
  ∀ (k : κ),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (P.val (v k)) : Ω[S⁄R])
inst_3 : Subsingleton (H1Cotangent R S)
refine_1 :
  Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict hu) : (a : P.toExtension.Cotangent) → σ →₀ S)
have refine_2 : Disjoint P.toExtension.toKaehler.ker
  (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
Tactic: refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb :
  ∀ (k : κ),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (P.val (v k)) : Ω[S⁄R])
inst_3 : Subsingleton (H1Cotangent R S)
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤
have refine_1 : Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (b : (a : κ) → Ω[S⁄R]) i)) ⊤
Tactic: simp_rw [← hb]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb :
  ∀ (k : κ),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (P.val (v k)) : Ω[S⁄R])
inst_3 : Subsingleton (H1Cotangent R S)
⊢ Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
have refine_2 : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
Tactic: apply disjoint_ker_toKaehler_of_linearIndependent
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb :
  ∀ (k : κ),
    Eq.{u_2 + 1} (α := Ω[S⁄R]) ((b : (a : κ) → Ω[S⁄R]) k : Ω[S⁄R]) ((D R S : (a : S) → Ω[S⁄R]) (P.val (v k)) : Ω[S⁄R])
inst_3 : Subsingleton (H1Cotangent R S)
⊢ LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))
have refine_2 : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (b : (a : κ) → Ω[S⁄R]) k
Tactic: simp_rw [← hb]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Free (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
σ : Type u_4
P : PreSubmersivePresentation R S ι σ
inst_3 : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb :
  ∀ (r : σ),
    Eq (α := P.toExtension.Cotangent) ((b : (a : σ) → P.toExtension.Cotangent) r : P.toExtension.Cotangent)
      ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent)
          (Subtype.mk (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) (P.relation r) ⋯) :
        P.toExtension.Cotangent)
h :
  Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
⊢ Eq (α := (j i : σ) → S)
    (fun (j i : σ) ↦
      (aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R))
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
      (Function.comp (β := P.toExtension.Cotangent) (⇑(P.cotangentRestrict ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
        (⇑b : (a : σ) → P.toExtension.Cotangent)))
have h₁ : ∀ (i j : σ),
  Eq.{u_2 + 1} (α := S)
    ((aeval P.val : (a : MvPolynomial ι R) → S)
        ((pderiv (P.map j) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation i) : MvPolynomial ι R) :
      S)
    (Function.comp (β := σ →₀ S) (⇑(Finsupp.linearEquivFunOnFinite S S σ) : (a : σ →₀ S) → σ → S)
        (Function.comp (β := P.toExtension.Cotangent)
          (⇑(P.cotangentRestrict sorry) : (a : P.toExtension.Cotangent) → σ →₀ S) (⇑b : (a : σ) → P.toExtension.Cotangent))
        i j :
      S)
Tactic: ext i j