-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem mul_finprod_cond_ne (a : α) (hf : (mulSupport f).Finite) :
    (f a * ∏ᶠ (i) (_ : i ≠ a), f i) = ∏ᶠ i, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ hf.toFinset \ {a}

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : f a = 1
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Tactic:
rw [ha, one_mul]

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : f a = 1
⊢ ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset, f i

Tactic:
have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a}) := by
  intro x hx
  rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
  exact ⟨fun h => And.intro hx h, fun h => h.2⟩

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ f x ≠ 1 ∧ ¬x = a

Tactic:
exact ⟨fun h => And.intro hx h, fun h => h.2⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Tactic:
by_cases ha : a ∈ mulSupport f

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Tactic:
apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Tactic:
rw [mem_mulSupport, not_not] at ha

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : f a = 1
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
⊢ ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})

Tactic:
intro x hx

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ hf.toFinset \ {a}

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset, f i

Tactic:
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
⊢ f a * ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ {a})
ha : f a = 1
⊢ ∏ i ∈ hf.toFinset.erase a, f i = ∏ i ∈ hf.toFinset, f i

Tactic:
apply Finset.prod_erase _ ha

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ᶠ (i : α), f i

Tactic:
rw [finprod_eq_prod _ hf]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : (mulSupport f).Finite
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset, f i