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)
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))
    ⋯
this :
  ∀ (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)
simp_rw :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
simp_rw₁ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
simp_rw₂ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (∑ x ∈ f.support, (f : (a : I) → S) x ⊗ₜ[R] (b : (a : I) → S) x)
⊢ (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) 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)) =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
have simp_rw₃ : Eq (α := S ⊗[R] S) (∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1)
  (∑ i ∈ f.support,
    HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] 1) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
Tactic: simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_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 : 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))
    ⋯
this :
  ∀ (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)
simp_rw :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
simp_rw₁ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
simp_rw₂ :
  ∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1 =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (∑ x ∈ f.support, (f : (a : I) → S) x ⊗ₜ[R] (b : (a : I) → S) x)
simp_rw₃ :
  Eq (α := S ⊗[R] S) (∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1)
    (∑ i ∈ f.support,
      HMul.hMul (α := S ⊗[R] S) (β := S ⊗[R] S) (x ⊗ₜ[R] 1) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S))
⊢ (∑ a ∈ f.support,
      Finsupp.sum ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) a : S))) 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)) =
    HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S)
have simp_rw₄ : Eq (α := S ⊗[R] S) (∑ x_1 ∈ f.support, HMul.hMul (β := S) x ((f : (a : I) → S) x_1 : S) ⊗ₜ[R] (b : (a : I) → S) x_1)
  (∑ i ∈ f.support,
    HMul.hMul (β := S) x ((f : (a : I) → S) i : S) ⊗ₜ[R] HMul.hMul (α := S) (β := S) (1 : S) ((b : (a : I) → S) i : S))
Tactic: simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_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 : 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))
    ⋯
this :
  ∀ (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)
⊢ HMul.hMul (α := S ⊗[R] S) (x ⊗ₜ[R] 1) (elem R S) =
    ∑ a_1 ∈ f.support.biUnion fun (i : I) ↦ (a i).support,
      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) ((a i : (a : I) → R) a_1 : R) y) :
          I →₀ R)
        fun (b' : I) (c : R) ↦
        HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) b' ⊗ₜ[R] (b : (a : I) → S) a_1 : S ⊗[R] S)
have ha : a = fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
Tactic: rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
-- 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))) ⋯
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))
    ⋯
⊢ 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 this : F = G
Tactic: have : F = G := by
    apply Finsupp.curryEquiv.symm.injective
    apply (Finsupp.equivCongrLeft (Equiv.prodComm I I)).injective
    apply (b.tensorProduct b).repr.symm.injective
    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]
    have : ∀ i, ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i := by
      intro i
      simp_rw [Finsupp.sum, TensorProduct.smul_tmul', ← TensorProduct.sum_tmul]
      congr 1
      exact b.linearCombination_repr _
    rw [Finsupp.onFinset_sum, Finsupp.onFinset_sum]
    · trans (x ⊗ₜ 1) * elem R S
      · simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_mul]
      · rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
        rfl
    · intro; simp
    · intro; simp
-- 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))
    ⋯
this : F = G
j : I
⊢ HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
    f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
have a₁ : Eq (α := I →₀ R) ((b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S)) : 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)
Tactic: apply b.repr.injective
-- 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))) ⋯
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))
    ⋯
this : F = G
⊢ 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 this₁ : ∀ (j : I),
  HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
    f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
Tactic: have : ∀ j, x * f j = f.sum fun i y ↦ a i j • y := by
    intro j
    apply b.repr.injective
    exact DFunLike.congr_fun this j
-- 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))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
⊢ 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 h : 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))
  (∑ i ∈ f.support,
    HMul.hMul (β := S) x
      ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) : S))
Tactic: rw [← mul_one x, ← @lmul_elem R, hf, map_finsuppSum, Finsupp.sum, Finset.mul_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))) ⋯
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))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
⊢ 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))
    (∑ i ∈ f.support,
      HMul.hMul (β := S) x
        ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) ((f : (a : I) → S) i ⊗ₜ[R] (b : (a : I) → S) i : S ⊗[R] S) : S))
have h : Membership.mem (γ := Submodule R S)
  (Submodule.span R
    (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
      (↑f.support : Set I) (↑f.support : Set I)))
  (∑ x ∈ f.support,
    ∑ x_1 ∈ f.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a x_1 : (a : I) → R) x : R)
        (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) x_1 : S) ((b : (a : I) → S) x : S)))
Tactic: simp only [TensorProduct.lmul'_apply_tmul, Finset.coe_image₂, ← mul_assoc, this,
    Finsupp.sum, Finset.sum_mul, smul_mul_assoc]
-- 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))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (∑ x ∈ f.support,
      ∑ x_1 ∈ f.support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a x_1 : (a : I) → R) x : R)
          (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) x_1 : S) ((b : (a : I) → S) x : S)))
have h : ∀ c ∈ f.support,
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (∑ x ∈ f.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a x : (a : I) → R) c : R)
        (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) x : S) ((b : (a : I) → S) c : S)))
Tactic: apply Submodule.sum_mem
-- 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))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      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
hi : i ∈ f.support
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (∑ x ∈ f.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a x : (a : I) → R) i : R)
        (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) x : S) ((b : (a : I) → S) i : S)))
have h : ∀ c ∈ f.support,
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a c : (a : I) → R) i : R)
      (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) c : S) ((b : (a : I) → S) i : S)))
Tactic: apply Submodule.sum_mem