-- Mathlib/RingTheory/Unramified/Finite.lean
theorem iff_exists_tensorProduct [EssFiniteType R S] :
    FormallyUnramified R S ↔ ∃ t : S ⊗[R] S,
      (∀ s, ((1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) * t = 0) ∧ TensorProduct.lmul' R t = 1

Proof state:
case mp.intro.intro.refine_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Tactic:
obtain ⟨x, hx⟩ : e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 := by
  rw [← Ideal.mem_span_singleton, ← he₂]
  exact Ideal.subset_span ⟨s, rfl⟩

Result:
case mp.intro.intro.refine_1.intro
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Proof state:
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
exact Ideal.subset_span ⟨s, rfl⟩

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
⊢ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
refine ⟨1 - e, ?_, ?_⟩

Result:
case mp.intro.intro.refine_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
⊢ ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

case mp.intro.intro.refine_2
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
⊢ 1 - (1 - e) ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Proof state:
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {e}) ↔
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
constructor

Result:
case mp
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {e}) →
    ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

case mpr
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
⊢ (∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) →
    ∃ e, IsIdempotentElem e ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {e}

Proof state:
case mp.intro.intro.refine_1.intro
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Tactic:
rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]

Result:
no goals

Proof state:
case mp.intro.intro.refine_2
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
⊢ 1 - (1 - e) ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]

Result:
no goals

Proof state:
case mp.intro.intro.refine_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
⊢ ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Tactic:
intro s

Result:
case mp.intro.intro.refine_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0

Proof state:
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this✝ : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
this : e ∈ (Submodule.span (S ⊗[R] S) {1 - e}).annihilator
⊢ IsIdempotentElem e

Tactic:
simpa [IsIdempotentElem, mul_sub, sub_eq_zero, eq_comm, -Ideal.submodule_span_eq,
  Submodule.mem_annihilator_span_singleton] using this

Result:
no goals

Proof state:
case h
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - (1 - t)) = 0
ht₂ : 1 - t ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ IsIdempotentElem (1 - t) ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {1 - t}

Tactic:
generalize 1 - t = e at *

Result:
case h
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ IsIdempotentElem e ∧ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.span (S ⊗[R] S) {e}