-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.span_range_eq_ideal :
    Ideal.span (Set.range fun s : S => (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) =
      KaehlerDifferential.ideal R S

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ ideal R S

Tactic:
rw [Ideal.span_le]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆ ↑(ideal R S)

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.restrictScalars S (ideal R S) ≤
    Submodule.restrictScalars S (Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Tactic:
rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S (Submodule.span (S ⊗[R] S) (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ideal R S ≤ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
change (KaehlerDifferential.ideal R S).restrictScalars S ≤ (Ideal.span _).restrictScalars S

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.restrictScalars S (ideal R S) ≤
    Submodule.restrictScalars S (Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ⊆ ↑(ideal R S)

Tactic:
rintro _ ⟨s, rfl⟩

Result:
case a.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(ideal R S)

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S
      (Submodule.span (S ⊗[R] S) ↑(Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)))

Tactic:
exact Submodule.subset_span

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S (Submodule.span (S ⊗[R] S) (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Tactic:
conv_rhs => rw [← Submodule.span_span_of_tower S]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S
      (Submodule.span (S ⊗[R] S) ↑(Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = ideal R S

Tactic:
apply le_antisymm

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ ideal R S

case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ideal R S ≤ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
case a.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
⊢ (fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) s ∈ ↑(ideal R S)

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Result:
no goals