-- 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:
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)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (∑ x ∈ f.support, (a x) j • f x) = 0

Tactic:
trans b.repr (f.support.sum (fun _ ↦ 0))

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)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (∑ x ∈ f.support, (a x) j • f x) = b.repr (∑ x ∈ f.support, 0)

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)) ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (∑ x ∈ f.support, 0) = 0

Proof state:
case 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)) ⋯
⊢ (Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.finsuppProdEquiv.symm F) =
    (Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.finsuppProdEquiv.symm G)

Tactic:
apply (b.tensorProduct b).repr.symm.injective

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)) ⋯
⊢ (b.tensorProduct b).repr.symm ((Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.finsuppProdEquiv.symm F)) =
    (b.tensorProduct b).repr.symm ((Finsupp.equivCongrLeft (Equiv.prodComm I I)) (Finsupp.finsuppProdEquiv.symm G))

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

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

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)) ⋯
this✝ : F = G
this : ∀ (j : I), x * f j = 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:
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✝

Tactic:
simp [b', Basis.tensorProduct, TensorProduct.smul_tmul']

Result:
no goals