-- Mathlib/Data/ENNReal/Operations.lean
lemma prod_inv_distrib {ι : Type*} {f : ι → ℝ≥0∞} {s : Finset ι}
    (hf : s.toSet.Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) : (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Proof state:
case cons
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (∏ i ∈ Finset.cons i s hi, f i)⁻¹ = ∏ i ∈ Finset.cons i s hi, (f i)⁻¹

Tactic:
simp [← ih (hf.mono <| by simp)]

Result:
case cons
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = ⊤
j : ι
hj : j ∈ s
⊢ j ∈ ↑(Finset.cons i s hi)

Tactic:
simp [hj]

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ j ∈ ↑(Finset.cons i s hi)

Tactic:
simp [hj]

Result:
no goals

Proof state:
case cons
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹

Tactic:
refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
  (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)

Result:
case cons.refine_1
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ f j ≠ ⊤

case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = ⊤
j : ι
hj : j ∈ s
⊢ f j ≠ 0

Proof state:
case cons.refine_1
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ f j ≠ ⊤

Tactic:
exact imp_iff_not_or.2 (hf (by simp) (by simp [hj]) <| .symm <| ne_of_mem_of_not_mem hj hi) hi₀

Result:
no goals

Proof state:
case empty
ι : Type u_1
f : ι → ℝ≥0∞
hf : (↑∅).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (∏ i ∈ ∅, f i)⁻¹ = ∏ i ∈ ∅, (f i)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = ⊤
j : ι
hj : j ∈ s
⊢ f j ≠ 0

Tactic:
exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹

Tactic:
induction' s using Finset.cons_induction with i s hi ih

Result:
case empty
ι : Type u_1
f : ι → ℝ≥0∞
hf : (↑∅).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (∏ i ∈ ∅, f i)⁻¹ = ∏ i ∈ ∅, (f i)⁻¹

case cons
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ (∏ i ∈ Finset.cons i s hi, f i)⁻¹ = ∏ i ∈ Finset.cons i s hi, (f i)⁻¹

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
hi₀ : f i = ⊤
j : ι
hj : j ∈ s
⊢ i ∈ ↑(Finset.cons i s hi)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
f : ι → ℝ≥0∞
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤
⊢ ↑s ⊆ ↑(Finset.cons i s hi)

Tactic:
simp

Result:
no goals