-- 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)) ⋯
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

Tactic:
trans (x ⊗ₜ 1) * elem R S

Result:
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 ⊗ₜ[R] 1 * elem R S

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 ⊗ₜ[R] 1 * elem R S =
    ∑ 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:
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
⊢ Module.Finite R S

Tactic:
let b : Basis I R S := Module.Free.chooseBasis R S

Result:
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
⊢ Module.Finite R S

Proof state:
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
⊢ ∃ a, elem R S = a.sum fun i x => x ⊗ₜ[R] b i

Tactic:
let b' := ((Basis.singleton PUnit.{1} S).tensorProduct b).reindex (Equiv.punitProd I)

Result:
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)
⊢ ∃ a, elem R S = a.sum fun i x => x ⊗ₜ[R] b i