ι : Type ?u.457146
α : Type ?u.457149
X : Type ?u.457152
M : Type u_1
N : Type ?u.457158
inst✝¹ : TopologicalSpace X
ι' : Sort ?u.457164
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
ι : Type ?u.457146
α : Type ?u.457149
X : Type ?u.457152
M : Type u_1
N : Type ?u.457158
inst✝¹ : TopologicalSpace X
ι' : Sort ?u.457164
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
rw [inf_eq_iInf]
ι : Type ?u.457146
α : Type ?u.457149
X : Type ?u.457152
M : Type u_1
N : Type ?u.457158
inst✝¹ : TopologicalSpace X
ι' : Sort ?u.457164
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
ι : Type ?u.457146
α : Type ?u.457149
X : Type ?u.457152
M : Type u_1
N : Type ?u.457158
inst✝¹ : TopologicalSpace X
ι' : Sort ?u.457164
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M
refine' continuousMul_iInf fun b => _
no goals
ι : Type ?u.457146
α : Type ?u.457149
X : Type ?u.457152
M : Type u_1
N : Type ?u.457158
inst✝¹ : TopologicalSpace X
ι' : Sort ?u.457164
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M
cases b <;> assumption