-- Mathlib/RingTheory/Unramified/Finite.lean
/-- An unramified free algebra is finitely generated. Iversen I.2.8 -/
lemma finite_of_free [Module.Free R S] : Module.Finite R S

Proof state:
case a.a.a
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
⊢ (∑ x_1 ∈ f.support, (b.repr (x * f x_1)).sum fun a b_1 => b_1 • b a ⊗ₜ[R] b x_1) =
    ∑ x ∈ f.support.biUnion fun i => (a i).support,
      (b.repr (f.sum fun i y => (a i) x • y)).sum fun a b_1 => b_1 • b a ⊗ₜ[R] b x

case a.a.a.hg
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
⊢ ∀ (a : I), (Finsupp.sum 0 fun a_1 b_1 => b_1 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)) = 0

case a.a.a.hg
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
⊢ ∀ (a : I), (Finsupp.sum 0 fun a_1 b_1 => b_1 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)) = 0

Tactic:
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 _

Result:
case a.a.a
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k => k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ (∑ x_1 ∈ f.support, (b.repr (x * f x_1)).sum fun a b_1 => b_1 • b a ⊗ₜ[R] b x_1) =
    ∑ x ∈ f.support.biUnion fun i => (a i).support,
      (b.repr (f.sum fun i y => (a i) x • y)).sum fun a b_1 => b_1 • b a ⊗ₜ[R] b x

case a.a.a.hg
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
⊢ ∀ (a : I), (Finsupp.sum 0 fun a_1 b_1 => b_1 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)) = 0

case a.a.a.hg
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
⊢ ∀ (a : I), (Finsupp.sum 0 fun a_1 b_1 => b_1 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)) = 0

Proof state:
case h
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
⊢ elem R S = (b'.repr (elem R S)).sum fun i x => x ⊗ₜ[R] b i

Tactic:
conv_lhs => rw [← b'.linearCombination_repr (elem R S), Finsupp.linearCombination_apply]

Result:
case h
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
b' : Basis I S (S ⊗[R] S) := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)
⊢ ((b'.repr (elem R S)).sum fun i a => a • b' i) = (b'.repr (elem R S)).sum fun i x => x ⊗ₜ[R] b i

Proof state:
case h.a.a.h.a
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Module.Free R S
I : Type u_3 := Module.Free.ChooseBasisIndex R S
b : Basis I R S := Module.Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i => b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j => b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i => (a i).support, b.repr (f.sum fun i y => (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i => (a i).support) (fun j => b.repr (f.sum fun i y => (a i) j • y)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = f.sum fun i y => (a i) j • y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
⊢ f j * b i ∈ Set.image2 (fun i j => f i * b j) ↑f.support ↑f.support

Tactic:
use j, hj, i, hi

Result:
no goals