case empty
K : Type u_3
L : Type u_2
L' : Type ?u.112045
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_1
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i in ∅, f i) = ∏ i in ∅, ↑(f i)

case insert
K : Type u_3
L : Type u_2
L' : Type ?u.112045
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_1
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
i : ι
s : Finset ι
hi : ¬i ∈ s
H : ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
⊢ ↑(∏ i in insert i s, f i) = ∏ i in insert i s, ↑(f i)
K : Type u_3
L : Type u_2
L' : Type ?u.112045
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_1
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i : ι, f i) = ∏ i : ι, ↑(f i)
induction' (Finset.univ : Finset ι) using Finset.induction_on with i s hi H
no goals
case empty
K : Type u_3
L : Type u_2
L' : Type ?u.112045
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_1
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
⊢ ↑(∏ i in ∅, f i) = ∏ i in ∅, ↑(f i)
simp
no goals
case insert
K : Type u_3
L : Type u_2
L' : Type ?u.112045
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field L'
inst✝² : Algebra K L
inst✝¹ : Algebra K L'
S : IntermediateField K L
ι : Type u_1
inst✝ : Fintype ι
f : ι → { x // x ∈ S }
i : ι
s : Finset ι
hi : ¬i ∈ s
H : ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
⊢ ↑(∏ i in insert i s, f i) = ∏ i in insert i s, ↑(f i)
rw [Finset.prod_insert hi, MulMemClass.coe_mul, H, Finset.prod_insert hi]