awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
simp_rw :
  (∃ (e : S ⊗[R] S),
      IsIdempotentElem e ∧
        Eq (α := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)) ↔
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Membership.mem (γ := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
⊢ (∃ (e : S ⊗[R] S), IsIdempotentElem e ∧ Eq (α := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (S ⊗[R] S ∙ e)) ↔
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S)

Tactic:
simp_rw [this, ← KaehlerDifferential.span_range_eq_ideal]

Premises used: KaehlerDifferential.span_range_eq_ideal
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
mp :
  (∃ (e : S ⊗[R] S),
      IsIdempotentElem e ∧
        Eq (α := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)) →
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Membership.mem (γ := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
mpr :
  (∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Membership.mem (γ := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)) →
    ∃ (e : S ⊗[R] S),
      IsIdempotentElem e ∧
        Eq (α := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)
⊢ (∃ (e : S ⊗[R] S),
      IsIdempotentElem e ∧
        Eq (α := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)) ↔
    ∃ (t : S ⊗[R] S),
      (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
        Membership.mem (γ := Ideal (S ⊗[R] S))
          (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
⊢ ∃ (t : S ⊗[R] S),
    (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
      Membership.mem (γ := Ideal (S ⊗[R] S))
        (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)

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

Premises used: HSub.hSub, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
mp : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
mp₁ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - (1 - e))
⊢ ∃ (t : S ⊗[R] S),
    (∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0) ∧
      Membership.mem (γ := Ideal (S ⊗[R] S))
        (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)

Tactic:
refine ⟨1 - e, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
s : S
rw :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))
⊢ e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)

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

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
s : S
⊢ Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))

Tactic:
Ideal.subset_span ⟨s, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
s : S
⊢ Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))

Tactic:
exact Ideal.subset_span ⟨s, rfl⟩
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
s : S
mp :
  ∀ (x : S ⊗[R] S) (hx : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) = e * x),
    HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
⊢ HSub.hSub (α := S ⊗[R] 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⟩
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
s : S
x : S ⊗[R] S
hx : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) = e * x
mp : e * x * (1 - e) = 0
mp₁ : (1 - e) * (e * x) = 0
mp₂ : (1 - e) * e * x = 0
mp₃ : (1 * e - e * e) * x = 0
mp₄ : (e - e * e) * x = 0
mp₅ : (e - e) * x = 0
mp₆ : 0 * x = 0
mp₇ mp₈ : Eq.{u_2 + 1} (α := S ⊗[R] S) 0 0
⊢ HSub.hSub (α := S ⊗[R] S) (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]

Premises used: sub_self, MulZeroClass.zero_mul, mul_assoc, sub_mul, mul_comm, IsIdempotentElem.eq, one_mul
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Ideal.span {e})
mp :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
mp₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (Ideal.span {e}) e
mp₂ mp₃ : e ∣ e
⊢ Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - (1 - e))

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

Premises used: sub_sub_cancel, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
h :
  IsIdempotentElem (1 - t) ∧
    Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
      (S ⊗[R] S ∙ (1 - t))
⊢ ∃ (e : S ⊗[R] S),
    IsIdempotentElem e ∧
      Eq (α := Ideal (S ⊗[R] S))
        (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)

Tactic:
use 1 - t
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
⊢ ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - (1 - t)) = 0

Tactic:
rw [← sub_sub_self 1 t] at ht₁

Premises used: OfNat.ofNat, sub_sub_self
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * t = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
ht₃ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - (1 - t)) = 0
⊢ Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)

Tactic:
rw [← sub_sub_self 1 t] at ht₁

Premises used: OfNat.ofNat, sub_sub_self
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - (1 - t)) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (1 - t)
h :
  ∀ (e : S ⊗[R] S) (ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0)
    (ht₂ :
      Membership.mem (γ := Ideal (S ⊗[R] S))
        (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e),
    IsIdempotentElem e ∧
      Eq (α := Ideal (S ⊗[R] S))
        (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) (S ⊗[R] S ∙ e)
⊢ IsIdempotentElem (1 - t) ∧
    Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
      (S ⊗[R] S ∙ (1 - t))

Tactic:
generalize 1 - t = e at *
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
h : IsIdempotentElem e
h₁ :
  Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
⊢ IsIdempotentElem e ∧
    Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
      (S ⊗[R] S ∙ e)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this_1 :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
this : Membership.mem (γ := Ideal (S ⊗[R] S)) (Submodule.annihilator (M := S ⊗[R] S) (S ⊗[R] S ∙ (1 - e))) e
⊢ IsIdempotentElem e

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

Premises used: mul_sub, sub_eq_zero, eq_comm, IsIdempotentElem, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
h : Membership.mem (γ := Ideal (S ⊗[R] S)) (Submodule.annihilator (M := S ⊗[R] S) (S ⊗[R] S ∙ (1 - e))) e
⊢ IsIdempotentElem e

Tactic:
suffices e ∈ (Submodule.span (S ⊗[R] S) {1 - e}).annihilator by
        simpa [IsIdempotentElem, mul_sub, sub_eq_zero, eq_comm,
          Submodule.mem_annihilator_span_singleton] using this
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
⊢ LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (Submodule.annihilator (M := S ⊗[R] S) (S ⊗[R] S ∙ (1 - e)))

Tactic:
simpa only [Ideal.span_le, Set.range_subset_iff,
        Submodule.mem_annihilator_span_singleton, SetLike.mem_coe]

Premises used: Ideal.span_le, SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, Set.range_subset_iff
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
⊢ Membership.mem (γ := Ideal (S ⊗[R] S)) (Submodule.annihilator (M := S ⊗[R] S) (S ⊗[R] S ∙ (1 - e))) e

Tactic:
exact (show Ideal.span _ ≤ _ by simpa only [Ideal.span_le, Set.range_subset_iff,
        Submodule.mem_annihilator_span_singleton, SetLike.mem_coe]) ht₂
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
h :
  LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)
h₁ :
  LE.le (α := Ideal (S ⊗[R] S)) (S ⊗[R] S ∙ e)
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
⊢ Eq (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
h : ∀ (y : S), e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] y) (y ⊗ₜ[R] 1)
⊢ LE.le (α := Ideal (S ⊗[R] S)) (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))
    (S ⊗[R] S ∙ e)

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ht₂,
        Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Set.range_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.submodule_span_eq, SetLike.mem_coe, Set.range_subset_iff, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
⊢ LE.le (α := Ideal (S ⊗[R] S)) (S ⊗[R] S ∙ e)
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)))

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ht₂,
        Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Set.range_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.submodule_span_eq, SetLike.mem_coe, Set.range_subset_iff, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
s : S
h : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) = e * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)
⊢ e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)

Tactic:
use 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1
-- Module: Mathlib.RingTheory.Unramified.Finite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : EssFiniteType R S
this :
  ∀ (t : S ⊗[R] S),
    Eq (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) t : S) (1 : S) ↔
      Membership.mem (γ := Ideal (S ⊗[R] S)) (KaehlerDifferential.ideal R S) (1 - t)
t e : S ⊗[R] S
ht₁ : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ :
  Membership.mem (γ := Ideal (S ⊗[R] S))
    (Ideal.span (Set.range fun (s : S) ↦ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1))) e
s : S
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) = e * HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)

Tactic:
linear_combination ht₁ s