Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: case hker
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : 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 : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ P.toExtension.toKaehler.ker ⊓
      Submodule.span S (Set.range fun x ↦ ↑P.cotangentSpaceBasis.repr.symm (Finsupp.single (v x) 1)) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥

pp: case hker.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : 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 : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑↑P.cotangentSpaceBasis.repr.symm

Tactic:
]

Goal state after:
case hker
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : 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 : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ P.toExtension.toKaehler.ker ⊓
      Submodule.span S (Set.range fun x ↦ ↑P.cotangentSpaceBasis.repr.symm (Finsupp.single (v x) 1)) =
    Submodule.map ↑P.cotangentSpaceBasis.repr.symm ⊥

case hker.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : 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 : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := P.toExtension.toKaehler ∘ₗ ↑P.cotangentSpaceBasis.repr.symm
hfg : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑↑P.cotangentSpaceBasis.repr.symm