-- Mathlib/RingTheory/Unramified/Finite.lean
lemma finite_of_free_aux (I) [DecidableEq I] (b : Basis I R S)
    (f : I →₀ S) (x : S) (a : I → I →₀ R) (ha : a = fun i ↦ b.repr (b i * x)) :
    (1 ⊗ₜ[R] x * Finsupp.sum f fun i y ↦ y ⊗ₜ[R] b i) =
      Finset.sum (f.support.biUnion fun i ↦ (a i).support) fun k ↦
    Finsupp.sum (b.repr (f.sum fun i y ↦ a i k • y)) fun j c ↦ c • b j ⊗ₜ[R] b k

Proof state:
case e_g.h.h
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i j : I
s : S
⊢ ∀ (i_1 : I), 0 • b i_1 ⊗ₜ[R] b i = 0

Tactic:
intro

Result:
case e_g.h.h
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i j : I
s : S
i✝ : I
⊢ 0 • b i✝ ⊗ₜ[R] b i = 0

Proof state:
case hfg
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y => (b.repr (b i * x)) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) =
      f.sum fun i y => (b.repr y).sum fun j z => (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
exact fun _ _ ↦ rfl

Result:
no goals

Proof state:
case h_add
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i a✝ : I
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • b a✝ ⊗ₜ[R] b i = b₁✝ • b a✝ ⊗ₜ[R] b i + b₂✝ • b a✝ ⊗ₜ[R] b i

Tactic:
simp only [add_smul]

Result:
no goals

Proof state:
case hg
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y => (b.repr (b i * x)) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) =
      f.sum fun i y => (b.repr y).sum fun j z => (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (f.support.biUnion fun i => (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

Tactic:
simp only [a, Finset.mem_sdiff, Finset.mem_biUnion, Finsupp.mem_support_iff, ne_eq, not_not,
  and_imp, forall_exists_index]

Result:
case hg
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y => (b.repr (b i * x)) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) =
      f.sum fun i y => (b.repr y).sum fun j z => (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ (x_1 x_2 : I),
    ¬f x_2 = 0 →
      ¬(b.repr (b x_2 * x)) x_1 = 0 → (b.repr (b i * x)) x_1 = 0 → ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

Proof state:
case h_zero
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i : I
⊢ ∀ (a : I), 0 • b a ⊗ₜ[R] b i = 0

Tactic:
intro

Result:
case h_zero
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i a✝ : I
⊢ 0 • b a✝ ⊗ₜ[R] b i = 0

Proof state:
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y => (b.repr (b i * x)) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) =
      f.sum fun i y => (b.repr y).sum fun j z => (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
⊢ ∀ x_1 ∈ f.support,
    ∑ x ∈ (a x_1).support, ((a x_1) x • f x_1) ⊗ₜ[R] b x =
      ∑ x_2 ∈ f.support.biUnion fun i => (b.repr (b i * x)).support, ((b.repr (b x_1 * x)) x_2 • f x_1) ⊗ₜ[R] b x_2

Tactic:
intros i hi

Result:
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y => (b.repr (b i * x)) k • b.repr y).sum fun j z => z • b j ⊗ₜ[R] b k) =
      f.sum fun i y => (b.repr y).sum fun j z => (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ x_1 ∈ f.support.biUnion fun i => (b.repr (b i * x)).support, ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Proof state:
case e_g.h.h
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i j : I
s : S
⊢ (((a j) i • b.repr s).sum fun j z => z • b j ⊗ₜ[R] b i) = (b.repr s).sum fun j_1 z => (a j) i • z • b j_1 ⊗ₜ[R] b i

case h_zero
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i : I
⊢ ∀ (a : I), 0 • b a ⊗ₜ[R] b i = 0

case h_add
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i : I
⊢ ∀ (a : I) (b₁ b₂ : R), (b₁ + b₂) • b a ⊗ₜ[R] b i = b₁ • b a ⊗ₜ[R] b i + b₂ • b a ⊗ₜ[R] b i

Tactic:
rw [Finsupp.sum_smul_index]

Result:
case e_g.h.h
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i j : I
s : S
⊢ ((b.repr s).sum fun i_1 a_1 => ((a j) i * a_1) • b i_1 ⊗ₜ[R] b i) =
    (b.repr s).sum fun j_1 z => (a j) i • z • b j_1 ⊗ₜ[R] b i

case e_g.h.h
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i j : I
s : S
⊢ ∀ (i_1 : I), 0 • b i_1 ⊗ₜ[R] b i = 0

case h_zero
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i : I
⊢ ∀ (a : I), 0 • b a ⊗ₜ[R] b i = 0

case h_add
R : Type u_3
S : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_2
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
i : I
⊢ ∀ (a : I) (b₁ b₂ : R), (b₁ + b₂) • b a ⊗ₜ[R] b i = b₁ • b a ⊗ₜ[R] b i + b₂ • b a ⊗ₜ[R] b i