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

Tactic:
congr! with _ i x

Result:
case h.h.e'_7.h.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)
x✝ : I
i : S
⊢ i • b' x✝ = i ⊗ₜ[R] b x✝

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
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
⊢ ∀ (j : I), x * f j = f.sum fun i y => (a i) j • y

Tactic:
intro j

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 : F = G
j : I
⊢ x * f j = f.sum fun i y => (a i) j • y

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
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
⊢ Submodule.span R ↑(Finset.image₂ (fun i j => f i * b j) f.support f.support) = ⊤

Tactic:
rw [← top_le_iff]

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
f : I →₀ S
hf : elem R S = f.sum fun i x => x ⊗ₜ[R] b i
⊢ ⊤ ≤ Submodule.span R ↑(Finset.image₂ (fun i j => f i * b j) f.support f.support)

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
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
⊢ x ∈ Submodule.span R ↑(Finset.image₂ (fun i j => f i * b j) f.support f.support)

Tactic:
let G : I →₀ I →₀ R := Finsupp.onFinset (Finset.biUnion f.support (fun i ↦ (a i).support))
  (fun j ↦ b.repr (f.sum (fun i y ↦ a i j • y)))
  (fun j ↦ not_imp_comm.mp (hG j))

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
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 ∈ Submodule.span R ↑(Finset.image₂ (fun i j => f i * b j) f.support f.support)

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
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)) ⋯
⊢ ∀ (i : I), ((b.repr (x * f i)).sum fun j k => k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i

Tactic:
intro 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
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)) ⋯
i : I
⊢ ((b.repr (x * f i)).sum fun j k => k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i