-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.span_range_derivation :
    Submodule.span S (Set.range <| KaehlerDifferential.D R S) = ⊤

Proof state:
case intro.mk.refine_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : x ∈ ideal R S
this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (a : S),
    ∀ x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1),
      (∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
        ∃ (hx : a • x ∈ ideal R S), (ideal R S).toCotangent ⟨a • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rintro r x - ⟨hx₁, hx₂⟩

Result:
case intro.mk.refine_4.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
r : S
x : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (ideal R S).toCotangent ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : r • x ∈ ideal R S), (ideal R S).toCotangent ⟨r • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Proof state:
case intro.mk.refine_1.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ ∃ (hx : (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈ ideal R S),
    (ideal R S).toCotangent ⟨(fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩

Result:
case intro.mk.refine_1.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ (ideal R S).toCotangent ⟨(fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, ⋯⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Proof state:
case intro.mk.refine_3.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x y : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (ideal R S).toCotangent ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
hy₁ : y ∈ ideal R S
hy₂ : (ideal R S).toCotangent ⟨y, hy₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : x + y ∈ ideal R S), (ideal R S).toCotangent ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact ⟨add_mem hx₁ hy₁, Submodule.add_mem _ hx₂ hy₂⟩

Result:
no goals

Proof state:
case intro.mk.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : x ∈ ideal R S
this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (x y : S ⊗[R] S),
    x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        (∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
          (∃ (hx : y ∈ ideal R S), (ideal R S).toCotangent ⟨y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) →
            ∃ (hx : x + y ∈ ideal R S), (ideal R S).toCotangent ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rintro x y - - ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩

Result:
case intro.mk.refine_3.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x y : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (ideal R S).toCotangent ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
hy₁ : y ∈ ideal R S
hy₂ : (ideal R S).toCotangent ⟨y, hy₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : x + y ∈ ideal R S), (ideal R S).toCotangent ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : Ω[S⁄R]
⊢ x ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x

Result:
case intro.mk
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : x ∈ ideal R S
⊢ (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Proof state:
case intro.mk.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : x ∈ ideal R S
this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∃ (hx : 0 ∈ ideal R S), (ideal R S).toCotangent ⟨0, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact ⟨zero_mem _, Submodule.zero_mem _⟩

Result:
no goals

Proof state:
case intro.mk.refine_4.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx : x✝ ∈ ideal R S
this : x✝ ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
r : S
x : S ⊗[R] S
hx₁ : x ∈ ideal R S
hx₂ : (ideal R S).toCotangent ⟨x, hx₁⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ ∃ (hx : r • x ∈ ideal R S), (ideal R S).toCotangent ⟨r • x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact ⟨((KaehlerDifferential.ideal R S).restrictScalars S).smul_mem r hx₁,
  Submodule.smul_mem _ r hx₂⟩

Result:
no goals