Theorem: Finset.prod_one_add (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, t.prod f
Tactic:
simp_rw [add_comm, Finset.prod_add]
State after:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = ∑ t ∈ s.powerset, t.prod f

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = ∑ t ∈ s.powerset, t.prod f
Tactic:
congr
State after:
case e_f
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ (fun t => (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1) = fun t => t.prod f

State before:
case e_f
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ (fun t => (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1) = fun t => t.prod f
Tactic:
ext t
State after:
case e_f.h
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = t.prod f

State before:
case e_f.h
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = t.prod f
Tactic:
convert mul_one (Finset.prod t fun a => f a)
State after:
case h.e'_2.h.e'_6
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ ∏ i ∈ s \ t, 1 = 1

State before:
case h.e'_2.h.e'_6
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ ∏ i ∈ s \ t, 1 = 1
Tactic:
exact Finset.prod_eq_one (fun i _ => rfl)
State after:
no goals