-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem HasProd.update' {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α]
    [ContinuousMul α] [DecidableEq β] {f : β → α} {a a' : α} (hf : HasProd f a) (b : β) (x : α)
    (hf' : HasProd (update f b x) a') : a * x = a' * f b

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 => f b_1 * if b_1 = b then x else 1) (a * x)
⊢ a * x = a' * f b

Tactic:
simp_rw [this] at h

Result:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 => update f b x b_1 * if b_1 = b then f b else 1) (a * x)
⊢ a * x = a' * f b

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
⊢ a * x = a' * f b

Tactic:
have h := hf.mul (hasProd_ite_eq b x)

Result:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 => f b_1 * if b_1 = b then x else 1) (a * x)
⊢ a * x = a' * f b

Proof state:
case pos
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
hb' : b' = b
⊢ f b' * x = update f b x b' * f b

Tactic:
simpa only [Function.update_apply, hb', eq_self_iff_true] using mul_comm (f b) x

Result:
no goals

Proof state:
case neg
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
hb' : ¬b' = b
⊢ f b' * 1 = update f b x b' * 1

Tactic:
simp only [Function.update_apply, hb', if_false]

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
⊢ (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1

Tactic:
split_ifs with hb'

Result:
case pos
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
hb' : b' = b
⊢ f b' * x = update f b x b' * f b

case neg
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
hb' : ¬b' = b
⊢ f b' * 1 = update f b x b' * 1

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
⊢ ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1

Tactic:
intro b'

Result:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
b' : β
⊢ (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a
b : β
x : α
hf' : HasProd (update f b x) a'
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 => update f b x b_1 * if b_1 = b then f b else 1) (a * x)
⊢ a * x = a' * f b

Tactic:
exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b)))

Result:
no goals