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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
i j : I
s : S
e_g :
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (i_1 : I) (a_1 : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) (HMul.hMul (α := R) ((a j : (a : I) → R) i : R) a_1)
        ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    ((HSMul.hSMul (α := R) (β := I →₀ R) ((a j : (a : I) → R) i : R) ((b.repr : (a : S) → I →₀ R) s : I →₀ R)).sum
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) s) fun (j_1 : I) (z : R) ↦
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
        (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)))
have e_g₁ : ∀ (i_1 : I),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S ⊗[R] S) 0 ((b : (a : I) → S) i_1 ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) =
    0
Tactic: rw [Finsupp.sum_smul_index]
-- 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ f.support,
      ∑ x_1 ∈ (a x).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1)
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦
              HSMul.hSMul.{u_1, u_2, u_2} (α := R)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have h₁ : ∀ (k : I),
  Eq (α := S ⊗[R] S)
    (Finsupp.sum
      (f.sum fun (i : I) (y : S) ↦
        HSMul.hSMul (α := R) (β := I →₀ R) ((a i : (a : I) → R) k : R) ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
      fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
    (f.sum fun (i : I) (y : S) ↦
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) k : R)
          (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
Tactic: have h₁ : ∀ k,
    (Finsupp.sum (Finsupp.sum f fun i y ↦ a i k • b.repr y) fun j z ↦ z • b j ⊗ₜ[R] b k) =
      (f.sum fun i y ↦ (b.repr y).sum fun j z ↦ a i k • z • b j ⊗ₜ[R] b k) := by
    intro i
    rw [Finsupp.sum_sum_index]
    · congr
      ext j s
      rw [Finsupp.sum_smul_index]
      · simp only [mul_smul, Finsupp.sum, ← Finset.smul_sum]
      intro; simp only [zero_smul]
    · intro; simp only [zero_smul]
    · intros; simp only [add_smul]
-- 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R) ((a i : (a : I) → R) k : R) ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) k : R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ f.support,
      ∑ x_1 ∈ (a x).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1)
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦
              HSMul.hSMul.{u_1, u_2, u_2} (α := R)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have h₂ : ∀ (x : S),
  ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
        ((b : (a : I) → S) a : S) =
    x
Tactic: have h₂ : ∀ (x : S), ((b.repr x).support.sum fun a ↦ b.repr x a • b a) = x := by
    simpa only [Finsupp.linearCombination_apply, Finsupp.sum] using b.linearCombination_repr
-- 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ f.support,
      ∑ x_1 ∈ (a x).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1)
    (∑ x_1 ∈ f.support,
      ∑
        x_2 ∈
          f.support.biUnion fun (i : I) ↦
            Finsupp.support.{u_4, u_1} (M := R)
              ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_1 : S) x) : I →₀ R) : (a : I) → R)
                x_2 :
              R)
            ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
          (b : (a : I) → S) x_2)
have apply : ∀ x_1 ∈ f.support,
  Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ (a x_1).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x_1 : (a : I) → R) x : R) ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
        (b : (a : I) → S) x)
    (∑
      x_2 ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_1 : S) x) : I →₀ R) : (a : I) → R)
              x_2 :
            R)
          ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
        (b : (a : I) → S) x_2)
Tactic: apply Finset.sum_congr 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ (a i).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x)
    (∑
      x_1 ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) x_1 :
            R)
          ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1)
have h : (a i).support ⊆
  f.support.biUnion fun (i : I) ↦
    Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))
Tactic: apply Finset.sum_subset_zero_on_sdiff
-- 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
h :
  (a i).support ⊆
    f.support.biUnion fun (i : I) ↦
      Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ (a i).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) x : R) ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x)
    (∑
      x_1 ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) x_1 :
            R)
          ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1)
have hg : ∀
  x_1 ∈
    (f.support.biUnion fun (i : I) ↦
        Finsupp.support.{u_4, u_1} (M := R)
          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))) \
      (a i).support,
  Eq (α := S ⊗[R] S)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) x_1 :
            R)
          ((f : (a : I) → S) i : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1 :
      S ⊗[R] S)
    (0 : S ⊗[R] S)
Tactic: apply Finset.sum_subset_zero_on_sdiff
-- 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
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
i : I
hi : i ∈ f.support
⊢ ∀
    x_1 ∈
      (f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x))) \
        (a i).support,
    Eq (α := S ⊗[R] S)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                x_1 :
              R)
            ((f : (a : I) → S) i : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1 :
        S ⊗[R] S)
      (0 : S ⊗[R] S)
have hg : ∀ (x_1 x_2 : I),
  ¬Eq.{u_2 + 1} (α := S) ((f : (a : I) → S) x_2 : S) (0 : S) →
    ¬Eq.{u_1 + 1} (α := R)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_2 : S) x) : I →₀ R) : (a : I) → R)
              x_1 :
            R)
          (0 : R) →
      Eq.{u_1 + 1} (α := R)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) x_1 :
            R)
          (0 : R) →
        Eq (α := S ⊗[R] S)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
                ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R)
                    x_1 :
                  R)
                ((f : (a : I) → S) i : S) ⊗ₜ[R]
              (b : (a : I) → S) x_1 :
            S ⊗[R] S)
          (0 : S ⊗[R] S)
Tactic: simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not,
      and_imp, forall_exists_index]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
s : S
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) = HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S)
have rw : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) - HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S) = 0
Tactic: rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
s : S
rw : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) - HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S) = 0
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) = HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S)
have rw₁ : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * elem R S = 0
Tactic: rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
s : S
rw : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) - HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S) = 0
rw₁ : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (s ⊗ₜ[R] 1) * elem R S = 0
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] s) (elem R S) = HMul.hMul (α := S ⊗[R] S) (s ⊗ₜ[R] 1) (elem R S)
have rw₂ : Eq.{u_2 + 1} (α := S ⊗[R] S) 0 0
Tactic: rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
⊢ ∃ (a : I →₀ S), Eq (α := S ⊗[R] S) (elem R S) (a.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
have h : Eq (α := S ⊗[R] S) (elem R S)
  (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
Tactic: use b'.repr (elem R S)
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
| elem R S
have rw : Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
  HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S)
Tactic: rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
⊢ Eq (α := S ⊗[R] S) (elem R S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
have h : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
    HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S))
  (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
Tactic: conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := Basis.reindex (Basis.tensorProduct (Basis.singleton PUnit.{1} S) b) (Equiv.punitProd I)
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (a : S) ↦
      HSMul.hSMul (β := S ⊗[R] S) a ((b' : (a : I) → S ⊗[R] S) i : S ⊗[R] S))
    (Finsupp.sum ((b'.repr : (a : S ⊗[R] S) → I →₀ S) (elem R S)) fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
have h : ∀ (x : I) (i : S), HSMul.hSMul (β := S ⊗[R] S) i ((b' : (a : I) → S ⊗[R] S) x : S ⊗[R] S) = i ⊗ₜ[R] (b : (a : I) → S) x
Tactic: congr! with _ i x
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
⊢ Module.Finite R S
have have : ∀ (f : I →₀ S) (hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)),
  Module.Finite R S
Tactic: have ⟨f, hf⟩ : ∃ (a : I →₀ S), elem R S = a.sum (fun i x ↦ x ⊗ₜ b i) := by
    let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
    use b'.repr (elem R S)
    conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]
    congr! with _ i x
    simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']
-- 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 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
⊢ Module.Finite R S
have fg_top : Submodule.FG.{u_1, u_2} (R := R) (M := S) ⊤
Tactic: constructor