awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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))
rw :
  ∀
    x ∈
      P.toExtension.toKaehler.ker ⊓
        Submodule.span S
          (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)),
    x = 0
⊢ Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))

Tactic:
rw [disjoint_iff, Submodule.eq_bot_iff]

Premises used: disjoint_iff, Submodule.eq_bot_iff
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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
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
⊢ x ∈
      P.toExtension.toKaehler.ker ⊓
        Submodule.span S
          (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)) →
    x = 0

Tactic:
⟨hx, hxs⟩
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
⊢ ∃ (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

Premises used: SetLike.mem_coe, Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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
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
⊢ x = 0

Tactic:
obtain ⟨c, rfl⟩ := hxs

Premises used: rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 (α := Ω[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

Premises used: LinearMap.mem_ker, SetLike.mem_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, map_finsuppSum, map_smul
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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
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
⊢ 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 rfl := (linearIndependent_iff.mp h) c hx

Premises used: linearIndependent_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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))
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:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)

Tactic:
P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_

Premises used: Algebra.Generators.cotangentRestrict_bijective_of_isCompl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)))) ⊤
refine_2 :
  Disjoint P.toExtension.toKaehler.ker
    (Submodule.span S (Set.range fun (x : κ) ↦ (P.cotangentSpaceBasis : (a : ι) → P.toExtension.CotangentSpace) (v x)))
⊢ Function.Bijective (α := P.toExtension.Cotangent) (β := σ →₀ S)
    (⇑(P.cotangentRestrict hu) : (a : P.toExtension.Cotangent) → σ →₀ S)

Tactic:
refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_

Premises used: Algebra.Generators.cotangentRestrict_bijective_of_isCompl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 : κ) ↦ (b : (a : κ) → Ω[S⁄R]) i)) ⊤
⊢ Eq (α := Submodule S Ω[S⁄R]) (Submodule.span S (Set.range fun (i : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v i)))) ⊤

Tactic:
simp_rw [← hb]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 : κ) ↦ (b : (a : κ) → Ω[S⁄R]) i)) ⊤

Tactic:
b.span_eq

Premises used: Module.Basis.span_eq
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 : κ) ↦ (b : (a : κ) → Ω[S⁄R]) i)) ⊤

Tactic:
exact b.span_eq

Premises used: Module.Basis.span_eq
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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_2 : 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)))

Tactic:
apply disjoint_ker_toKaehler_of_linearIndependent

Premises used: Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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_2 : LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (b : (a : κ) → Ω[S⁄R]) k
⊢ LinearIndependent S (M := Ω[S⁄R]) fun (k : κ) ↦ (D R S : (a : S) → Ω[S⁄R]) (P.val (v k))

Tactic:
simp_rw [← hb]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 : κ) ↦ (b : (a : κ) → Ω[S⁄R]) k

Tactic:
b.linearIndependent

Premises used: Module.Basis.linearIndependent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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 : κ) ↦ (b : (a : κ) → Ω[S⁄R]) k

Tactic:
exact b.linearIndependent

Premises used: Module.Basis.linearIndependent
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
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 ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S)
            (⇑b : (a : σ) → P.toExtension.Cotangent))
          i j :
        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)))

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
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 ⋯) : (a : P.toExtension.Cotangent) → σ →₀ S) (⇑b : (a : σ) → P.toExtension.Cotangent))
        i j :
      S)

Tactic:
simp only [Function.comp_apply, hb, Finsupp.linearEquivFunOnFinite_apply, cotangentRestrict_mk]

Premises used: Finsupp.linearEquivFunOnFinite_apply, Algebra.Generators.cotangentRestrict_mk, Function.comp_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)))

Tactic:
have heq : (fun j i ↦ (aeval P.val) (pderiv (P.map i) (P.relation j))) =
      Finsupp.linearEquivFunOnFinite S S _ ∘ P.cotangentRestrict P.map_inj ∘ ⇑b := by
    ext i j
    simp only [Function.comp_apply, hb, Finsupp.linearEquivFunOnFinite_apply, cotangentRestrict_mk]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
heq :
  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)))
hli :
  LinearIndependent S (M := (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)
hsp :
  Eq (α := Submodule S ((i : σ) → S))
    (Submodule.span S
      (Set.range fun (j i : σ) ↦
        (aeval P.val : (a : MvPolynomial ι R) → S)
          ((pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)))
    ⊤
⊢ IsUnit P.jacobian

Tactic:
apply P.isUnit_jacobian_of_linearIndependent_of_span_eq_top

Premises used: Algebra.PreSubmersivePresentation.isUnit_jacobian_of_linearIndependent_of_span_eq_top
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
heq :
  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)))
hli :
  LinearIndependent (ι := σ) S (M := (i : σ) → S)
    (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)))
⊢ LinearIndependent S (M := (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)

Tactic:
rw [heq]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Free
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)
heq :
  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)))
⊢ LinearIndependent (ι := σ) S (M := (i : σ) → S)
    (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)))

Tactic:
(b.linearIndependent.map' _ (LinearMap.ker_eq_bot_of_injective h.injective)).map' _
      (Finsupp.linearEquivFunOnFinite S S σ).ker

Premises used: Finsupp.linearEquivFunOnFinite, LinearIndependent.map', Function.Bijective.injective, Module.Basis.linearIndependent, LinearMap.ker_eq_bot_of_injective, LinearEquiv.ker