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

Proof state:
case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x y : S ⊗[R] S
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
hy : y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 + (y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1) ∈
    Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
exact add_mem hx hy

Result:
no goals

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 ∈ ↑(Submodule.restrictScalars S (ideal R S))

Tactic:
exact KaehlerDifferential.one_smul_sub_smul_one_mem_ideal _ _

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
⊢ x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
have : x - TensorProduct.lmul' (S := S) R x ⊗ₜ[R] (1 : S) = x := by
  rw [hx, TensorProduct.zero_tmul, sub_zero]

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
this : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 = x
⊢ x ∈ 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
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
⊢ x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 = x

Tactic:
rw [hx, TensorProduct.zero_tmul, sub_zero]

Result:
no goals

Proof state:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1) ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
refine Submodule.smul_mem _ x ?_

Result:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
case a.refine_2.a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1

Tactic:
exact Set.mem_range_self y

Result:
no goals

Proof state:
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 (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
⊢ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ Submodule.restrictScalars S (ideal R S)

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.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S ⊗[R] S),
    x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
intro x y hx hy

Result:
case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x y : S ⊗[R] S
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
hy : y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
apply Submodule.subset_span

Result:
case a.refine_2.a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
x y : S
this : x ⊗ₜ[R] y - (x * y) ⊗ₜ[R] 1 = x • (1 ⊗ₜ[R] y - y ⊗ₜ[R] 1)
⊢ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1 ∈ 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
x : S ⊗[R] S
⊢ x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

Result:
case a.refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ 0 - (TensorProduct.lmul' R) 0 ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

case a.refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S),
    x ⊗ₜ[R] y - (TensorProduct.lmul' R) (x ⊗ₜ[R] y) ⊗ₜ[R] 1 ∈
      Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ ∀ (x y : S ⊗[R] S),
    x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
      y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
        x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span 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
⊢ Submodule.restrictScalars S (ideal R S) ≤ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
rintro x (hx : _ = _)

Result:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
⊢ x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
case a.refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ 0 - (TensorProduct.lmul' R) 0 ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
rw [map_zero, TensorProduct.zero_tmul, sub_zero]

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