case h
α : Type u_2
β : Type ?u.9120
A : Type ?u.9123
B : Type ?u.9126
M : Type u_1
N : Type ?u.9132
P : Type ?u.9135
R : Type ?u.9138
S : Type ?u.9141
G : Type ?u.9144
M₀ : Type ?u.9147
G₀ : Type ?u.9150
ι : Sort ?u.9153
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ
α : Type u_2
β : Type ?u.9120
A : Type ?u.9123
B : Type ?u.9126
M : Type u_1
N : Type ?u.9132
P : Type ?u.9135
R : Type ?u.9138
S : Type ?u.9141
G : Type ?u.9144
M₀ : Type ?u.9147
G₀ : Type ?u.9150
ι : Sort ?u.9153
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
⊢ (mulSupport fun x => c) = univ
ext x
no goals
case h
α : Type u_2
β : Type ?u.9120
A : Type ?u.9123
B : Type ?u.9126
M : Type u_1
N : Type ?u.9132
P : Type ?u.9135
R : Type ?u.9138
S : Type ?u.9141
G : Type ?u.9144
M₀ : Type ?u.9147
G₀ : Type ?u.9150
ι : Sort ?u.9153
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
c : M
hc : c ≠ 1
x : α
⊢ (x ∈ mulSupport fun x => c) ↔ x ∈ univ
simp [hc]