-- 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) = b.repr (∑ x ∈ f.support, 0)

Tactic:
refine congr_arg b.repr (Finset.sum_congr rfl ?_)

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
⊢ ∀ x ∈ f.support, (a x) j • f x = 0

Proof state:
case ha
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
⊢ a = fun i => b.repr (b i * x)

Tactic:
rfl

Result:
no goals

Proof state:
case e_m
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
⊢ ∑ a ∈ (b.repr (x * f i)).support, (b.repr (x * f i)) a • b a = x * f i

Tactic:
exact b.linearCombination_repr _

Result:
no goals

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

Tactic:
rw [← mul_one x, ← @lmul_elem R, hf, map_finsupp_sum, Finsupp.sum, Finset.mul_sum]

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
⊢ ∑ i ∈ f.support, x * (TensorProduct.lmul' R) (f i ⊗ₜ[R] b i) ∈
    Submodule.span R ↑(Finset.image₂ (fun i j => f i * b j) f.support f.support)

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

Tactic:
simp only [Basis.repr_symm_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight,
  LinearMap.id_coe, id_eq, Basis.tensorProduct_apply, Finsupp.finsuppProdEquiv,
  Equiv.coe_fn_symm_mk, Finsupp.uncurry, map_finsupp_sum,
  Finsupp.linearCombination_single, Basis.tensorProduct_apply, Finsupp.equivCongrLeft_apply,
  Finsupp.linearCombination_equivMapDomain, Equiv.coe_prodComm]

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)) ⋯
⊢ (F.sum fun a b_1 => b_1.sum fun a_1 b_2 => b_2 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)) =
    G.sum fun a b_1 => b_1.sum fun a_1 b_2 => b_2 • (⇑(b.tensorProduct b) ∘ Prod.swap) (a, a_1)