-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.multipliable_of_eq_one_or_self (hf : Multipliable f)
    (h : ∀ b, g b = 1 ∨ g b = f b) : Multipliable g

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ filter (fun b => g b = f b) t
⊢ g b = 1

Tactic:
simp only [Finset.mem_filter, and_iff_right hbt] at hb

Result:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : ¬g b = f b
⊢ g b = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
⊢ Multipliable g

Tactic:
exact multipliable_iff_vanishing.2 fun e he ↦
  let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
  ⟨s, fun t ht ↦
    have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
      calc
        ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
          Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
        _ = ∏ b ∈ t, g b := by
         {refine Finset.prod_subset (Finset.filter_subset _ _) ?_
          intro b hbt hb
          simp only [Finset.mem_filter, and_iff_right hbt] at hb
          exact (h b).resolve_right hb}
    eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : ¬g b = f b
⊢ g b = 1

Tactic:
exact (h b).resolve_right hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
⊢ Multipliable g

Tactic:
classical
exact multipliable_iff_vanishing.2 fun e he ↦
  let ⟨s, hs⟩ := multipliable_iff_vanishing.1 hf e he
  ⟨s, fun t ht ↦
    have eq : ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t, g b :=
      calc
        ∏ b ∈ t with g b = f b, f b = ∏ b ∈ t with g b = f b, g b :=
          Finset.prod_congr rfl fun b hb ↦ (Finset.mem_filter.1 hb).2.symm
        _ = ∏ b ∈ t, g b := by
         {refine Finset.prod_subset (Finset.filter_subset _ _) ?_
          intro b hbt hb
          simp only [Finset.mem_filter, and_iff_right hbt] at hb
          exact (h b).resolve_right hb}
    eq ▸ hs _ <| Finset.disjoint_of_subset_left (Finset.filter_subset _ _) ht⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∀ x ∈ t, x ∉ filter (fun b => g b = f b) t → g x = 1

Tactic:
intro b hbt hb

Result:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
b : β
hbt : b ∈ t
hb : b ∉ filter (fun b => g b = f b) t
⊢ g b = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∏ b ∈ filter (fun b => g b = f b) t, g b = ∏ b ∈ t, g b

Tactic:
refine Finset.prod_subset (Finset.filter_subset _ _) ?_

Result:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∀ x ∈ t, x ∉ filter (fun b => g b = f b) t → g x = 1