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

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤

Tactic:
rw [_root_.eq_top_iff]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ⊤ ≤ Submodule.span S (Set.range ⇑(D R S))

Proof state:
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))

Tactic:
have : x ∈ (KaehlerDifferential.ideal R S).restrictScalars S := hx

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
this : x ∈ Submodule.restrictScalars S (ideal R S)
⊢ (ideal R S).toCotangent ⟨x, 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] S
hx : x ∈ ideal R S
this✝ : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
this : ∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
⊢ (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
exact this.choose_spec

Result:
no goals

Proof state:
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
this : x ∈ Submodule.restrictScalars S (ideal R S)
⊢ (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rw [← KaehlerDifferential.submodule_span_range_eq_ideal] at this

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
this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ (ideal R S).toCotangent ⟨x, 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
⊢ ⊤ ≤ Submodule.span S (Set.range ⇑(D R S))

Tactic:
rintro x -

Result:
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))

Proof state:
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
this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
suffices ∃ hx, (KaehlerDifferential.ideal R S).toCotangent ⟨x, hx⟩ ∈
    Submodule.span S (Set.range <| KaehlerDifferential.D R S) by
  exact this.choose_spec

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
this : 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))

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
⊢ (ideal R S).toCotangent ⟨(fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, ⋯⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
apply Submodule.subset_span

Result:
case intro.mk.refine_1.intro.a
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, ⋯⟩ ∈ Set.range ⇑(D R S)

Proof state:
case intro.mk.refine_1
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 ∈ 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))

Tactic:
rintro _ ⟨x, rfl⟩

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
⊢ ∃ (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))

Proof state:
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
this : 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))

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ this

Result:
case intro.mk.refine_1
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 ∈ 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))

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))

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))

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))

Proof state:
case intro.mk.refine_1.intro.a
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, ⋯⟩ ∈ Set.range ⇑(D R S)

Tactic:
exact ⟨x, KaehlerDifferential.DLinearMap_apply R S x⟩

Result:
no goals