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 : 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)
⊢ Submodule.FG.{u_1, u_2} (R := R) (M := S) ⊤
have h : Eq (α := Submodule R S)
  (Submodule.span R
    (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
          f.support f.support) :
      Set S))
  ⊤
Tactic: use Finset.image₂ (fun i j ↦ f i * b j) f.support f.support
-- 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)
⊢ Eq (α := Submodule R S)
    (Submodule.span R
      (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
            f.support f.support) :
        Set S))
    ⊤
have h : LE.le (α := Submodule R S) ⊤
  (Submodule.span R
    (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
          f.support f.support) :
      Set S))
Tactic: rw [← top_le_iff]
-- 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 : 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj : j ∉ f.support.biUnion fun (i : I) ↦ (a i).support
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
      I →₀ R)
    (0 : I →₀ R)
have hj₁ : ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
Tactic: simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and,
      not_not] at hj
Cleared hypotheses: hj
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
      I →₀ R)
    (0 : I →₀ R)
have simp : Eq (α := I →₀ R)
  ((b.repr : (a : S) → I →₀ R)
      (∑ x ∈ f.support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
    I →₀ R)
  (0 : I →₀ R)
Tactic: simp only [Finsupp.sum]
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    (0 : I →₀ R)
have trans : Eq (α := I →₀ R)
  ((b.repr : (a : S) → I →₀ R)
      (∑ x ∈ f.support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
    I →₀ R)
  ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)
Tactic: trans b.repr (f.support.sum (fun _ ↦ 0))
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
trans :
  Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    (0 : I →₀ R)
have trans₁ : Eq (α := I →₀ R) ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R) (0 : I →₀ R)
Tactic: trans b.repr (f.support.sum (fun _ ↦ 0))
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (∑ x ∈ f.support,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S)) :
      I →₀ R)
    ((b.repr : (a : S) → I →₀ R) (∑ x ∈ f.support, 0) : I →₀ R)
have refine : ∀ x ∈ f.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0
Tactic: refine congr_arg b.repr (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
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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
⊢ ∀ x ∈ f.support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0
have simp : ∀ (x : I),
  Ne (α := S) ((f : (a : I) → S) x : S) (0 : S) →
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) j : R) ((f : (a : I) → S) x : S) = 0
Tactic: simp only [Finsupp.mem_support_iff]
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
i : I
hi : Ne (α := S) ((f : (a : I) → S) i : S) (0 : S)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) j : R) ((f : (a : I) → S) i : S) = 0
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 ((f : (a : I) → S) i : S) = 0
Tactic: rw [hj i hi, zero_smul]
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
j : I
hj :
  ∀ (x : I), ¬Eq (α := S) ((f : (a : I) → S) x : S) (0 : S) → Eq.{u_1 + 1} (α := R) ((a x : (a : I) → R) j : R) (0 : R)
i : I
hi : Ne (α := S) ((f : (a : I) → S) i : S) (0 : S)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) 0 ((f : (a : I) → S) i : S) = 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a i : (a : I) → R) j : R) ((f : (a : I) → S) i : S) = 0
have rw₁ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [hj i hi, zero_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
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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(Finset.image₂ (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
            f.support f.support) :
        Set S))
    x
have hG : ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
  Eq (α := I →₀ R)
    ((b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
      I →₀ R)
    (0 : I →₀ R)
Tactic: have hG : ∀ j ∉ (Finset.biUnion f.support fun i ↦ (a i).support),
      b.repr (f.sum (fun i y ↦ a i j • y)) = 0 := by
    intro j hj
    simp only [Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_exists, not_and,
      not_not] at hj
    simp only [Finsupp.sum]
    trans b.repr (f.support.sum (fun _ ↦ 0))
    · refine congr_arg b.repr (Finset.sum_congr rfl ?_)
      simp only [Finsupp.mem_support_iff]
      intro i hi
      rw [hj i hi, zero_smul]
    · simp only [Finset.sum_const_zero, map_zero]
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ F = G
have a₁ : Eq (α := Finsupp.{u_2, u_1} (I × I) R)
  ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F : Finsupp.{u_2, u_1} (I × I) R)
  ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G : Finsupp.{u_2, u_1} (I × I) R)
Tactic: apply Finsupp.curryEquiv.symm.injective
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F : Finsupp.{u_2, u_1} (I × I) R)
    ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G : Finsupp.{u_2, u_1} (I × I) R)
have a₁ : Eq (α := Finsupp.{u_2, u_1} (I × I) R)
  ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
      ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F) :
    Finsupp.{u_2, u_1} (I × I) R)
  ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
      ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G) :
    Finsupp.{u_2, u_1} (I × I) R)
Tactic: apply (Finsupp.equivCongrLeft (Equiv.prodComm I I)).injective
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ Eq (α := Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F) :
      Finsupp.{u_2, u_1} (I × I) R)
    ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G) :
      Finsupp.{u_2, u_1} (I × I) R)
have a₁ : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
        (a : I × I →₀ R) → S ⊗[R] S)
      ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F)) :
    S ⊗[R] S)
  (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
        (a : I × I →₀ R) → S ⊗[R] S)
      ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
        ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G)) :
    S ⊗[R] S)
Tactic: apply (b.tensorProduct b).repr.symm.injective
-- 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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) F)) :
      S ⊗[R] S)
    (((LinearEquiv.symm (Basis.repr (b.tensorProduct b)) : Finsupp.{u_2, u_1} (I × I) R ≃ₗ[R] S ⊗[R] S) :
          (a : I × I →₀ R) → S ⊗[R] S)
        ((Finsupp.equivCongrLeft (Equiv.prodComm I I) : (a : I × I →₀ R) → I × I →₀ R)
          ((Equiv.symm Finsupp.curryEquiv : (a : I →₀ I →₀ R) → I × I →₀ R) G)) :
      S ⊗[R] S)
have a₁ : Eq (α := S ⊗[R] S)
  (F.sum fun (a : I) (f : I →₀ R) ↦
    f.sum fun (b' : I) (c : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
  (G.sum fun (a : I) (f : I →₀ R) ↦
    f.sum fun (b' : I) (c : R) ↦
      HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a : S ⊗[R] S))
Tactic: suffices (F.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) =
        G.sum fun a f ↦ f.sum fun b' c ↦ c • b b' ⊗ₜ[R] b a by
      simpa [Finsupp.linearCombination_apply, Finsupp.sum_uncurry_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
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)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
i : I
⊢ Eq (α := S ⊗[R] S)
    (Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))) fun (j : I) (k : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) k ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) :
      S ⊗[R] S)
    (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
have simp_rw : Eq (α := S ⊗[R] S)
  ((∑
        a ∈
          Finsupp.support.{u_2, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S))),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) i : S)) : I →₀ R) : (a : I) → R) a :
            R)
          ((b : (a : I) → S) a : S)) ⊗ₜ[R]
      (b : (a : I) → S) i :
    S ⊗[R] S)
  (HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S)
Tactic: simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]