α : Type u_1
β : Type ?u.5450
A : Type ?u.5453
B : Type ?u.5456
M : Type u_2
N : Type ?u.5462
P : Type ?u.5465
R : Type ?u.5468
S : Type ?u.5471
G : Type ?u.5474
M₀ : Type ?u.5477
G₀ : Type ?u.5480
ι : Sort ?u.5483
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ (∀ (x : α), ¬x ∈ ∅ → f x = 1) ↔ ∀ (a : α), f a = OfNat.ofNat 1 a
α : Type u_1
β : Type ?u.5450
A : Type ?u.5453
B : Type ?u.5456
M : Type u_2
N : Type ?u.5462
P : Type ?u.5465
R : Type ?u.5468
S : Type ?u.5471
G : Type ?u.5474
M₀ : Type ?u.5477
G₀ : Type ?u.5480
ι : Sort ?u.5483
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ mulSupport f = ∅ ↔ f = 1
simp_rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
no goals
α : Type u_1
β : Type ?u.5450
A : Type ?u.5453
B : Type ?u.5456
M : Type u_2
N : Type ?u.5462
P : Type ?u.5465
R : Type ?u.5468
S : Type ?u.5471
G : Type ?u.5474
M₀ : Type ?u.5477
G₀ : Type ?u.5480
ι : Sort ?u.5483
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : α → M
⊢ (∀ (x : α), ¬x ∈ ∅ → f x = 1) ↔ ∀ (a : α), f a = OfNat.ofNat 1 a
simp