awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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), 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)
have 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)
Tactic: simp_rw [this, ← KaehlerDifferential.span_range_eq_ideal]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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),
      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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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)
have mp : ∀ (s : S), HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
Tactic: refine ⟨1 - e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ ∃ (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)
have 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))
Tactic: refine ⟨1 - e, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ e ∣ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1)
have 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))
Tactic: rw [← Ideal.mem_span_singleton, ← he₂]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have 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
Tactic: obtain ⟨x, hx⟩ : e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 := by
        rw [← Ideal.mem_span_singleton, ← he₂]
        exact Ideal.subset_span ⟨s, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp : e * x * (1 - e) = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₁ : (1 - e) * (e * x) = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₂ : (1 - e) * e * x = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₃ : (1 * e - e * e) * x = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₄ : (e - e * e) * x = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₅ : (e - e) * x = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₆ : 0 * x = 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * (1 - e) = 0
have mp₇ : Eq.{u_2 + 1} (α := S ⊗[R] S) 0 0
Tactic: rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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})
⊢ 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))
have 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
Tactic: rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ 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))
have mp₁ : Membership.mem (γ := Ideal (S ⊗[R] S)) (Ideal.span {e}) e
Tactic: rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ 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))
have mp₂ : e ∣ e
Tactic: rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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)
⊢ ∃ (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)
have 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))
Tactic: use 1 - t
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (hypothesis)
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)
⊢ 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))
have ht₃ : ∀ (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₁
Cleared hypotheses: ht₁, ht₂
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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)
⊢ 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))
have 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)
Tactic: generalize 1 - t = e at *
Cleared hypotheses: ht₁, ht₂
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ 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)
have h : IsIdempotentElem e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
⊢ IsIdempotentElem e
have h : Membership.mem (γ := Ideal (S ⊗[R] S)) (Submodule.annihilator (M := S ⊗[R] S) (S ⊗[R] S ∙ (1 - e))) 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