[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : One α
f : Filter α
s : Set α
inst✝¹ : One β
inst✝ : OneHomClass F α β
φ : F
⊢ map (↑φ) 1 = 1
[PROOFSTEP]
rw [Filter.map_one', map_one, pure_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
hs : s ∈ f
⊢ s⁻¹ ∈ f⁻¹
[PROOFSTEP]
rwa [mem_inv, inv_preimage, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f✝ g : Filter α
s : Set α
src✝ : Inv (Filter α) := instInv
f : Filter α
⊢ map (Inv.inv ∘ Inv.inv) f = f
[PROOFSTEP]
rw [inv_involutive.comp_self, map_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : InvolutiveInv α
f g : Filter α
s : Set α
⊢ f⁻¹ ≤ g ↔ f ≤ g⁻¹
[PROOFSTEP]
rw [← Filter.inv_le_inv_iff, inv_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hs : s ∈ f
⊢ 1 ∈ f ^ 0
[PROOFSTEP]
exact one_mem_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s ^ (n + 1) ∈ f ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ : ℕ
hs : s ∈ f
n : ℕ
⊢ s * s ^ n ∈ f ^ (n + 1)
[PROOFSTEP]
exact mul_mem_mul hs (pow_mem_pow hs n)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ n : ℕ
hn : n ≠ 0
⊢ ⊥ ^ n = ⊥
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn), pow_succ, bot_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ f * ⊤ = ⊤
[PROOFSTEP]
refine' top_le_iff.1 fun s => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ f * ⊤ → s ∈ ⊤
[PROOFSTEP]
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ t₁, t₁ ∈ f ∧ t₁ * univ ⊆ s) → s = univ
[PROOFSTEP]
rintro ⟨t, ht, hs⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : t * univ ⊆ s
⊢ s = univ
[PROOFSTEP]
rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n : ℕ
hf : 1 ≤ f
⊢ ⊤ * f = ⊤
[PROOFSTEP]
refine' top_le_iff.1 fun s => _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ s ∈ ⊤ * f → s ∈ ⊤
[PROOFSTEP]
simp only [mem_mul, mem_top, exists_and_left, exists_eq_left]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s : Set α
⊢ (∃ x, x ∈ f ∧ univ * x ⊆ s) → s = univ
[PROOFSTEP]
rintro ⟨t, ht, hs⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s✝ : Set α
a : α
m n : ℕ
hf : 1 ≤ f
s t : Set α
ht : t ∈ f
hs : univ * t ⊆ s
⊢ s = univ
[PROOFSTEP]
rwa [univ_mul_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : Monoid α
f g : Filter α
s : Set α
a : α
m n✝ n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤
[PROOFSTEP]
rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨fun hfg => _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
obtain ⟨t₁, t₂, h₁, h₂, h⟩ : (1 : Set α) ∈ f * g := hfg.symm.subst one_mem_one
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
have hfg : (f * g).NeBot := hfg.symm.subst one_neBot
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
rw [(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff, Set.mul_eq_one_iff] at h 
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : NeBot (f * g)
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, h⟩ := h
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
[PROOFSTEP]
refine' ⟨a, b, _, _, h⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ f = pure a
[PROOFSTEP]
rwa [← hfg.of_mul_left.le_pure_iff, le_pure_iff]
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : NeBot (f * g)
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ g = pure b
[PROOFSTEP]
rwa [← hfg.of_mul_right.le_pure_iff, le_pure_iff]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1
[PROOFSTEP]
rintro ⟨a, b, rfl, rfl, h⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1
[PROOFSTEP]
rw [pure_mul_pure, h, pure_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
src✝³ : Monoid (Filter α) := Filter.monoid
src✝² : InvolutiveInv (Filter α) := Filter.instInvolutiveInv
src✝¹ : Div (Filter α) := Filter.instDiv
src✝ : Pow (Filter α) ℤ := Filter.instZPow
s t : Filter α
h : s * t = 1
⊢ s⁻¹ = t
[PROOFSTEP]
obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
src✝³ : Monoid (Filter α) := Filter.monoid
src✝² : InvolutiveInv (Filter α) := Filter.instInvolutiveInv
src✝¹ : Div (Filter α) := Filter.instDiv
src✝ : Pow (Filter α) ℤ := Filter.instZPow
a b : α
hab : a * b = 1
h : pure a * pure b = 1
⊢ (pure a)⁻¹ = pure b
[PROOFSTEP]
rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
[PROOFSTEP]
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
[PROOFSTEP]
refine' ⟨a, ha, ⟨a, b, h, pure_injective _⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1
[PROOFSTEP]
rw [← pure_mul_pure, ← ha, ← hb]
[GOAL]
case mp.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1
[PROOFSTEP]
exact u.inv_mul
[GOAL]
case mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
[PROOFSTEP]
rintro ⟨a, rfl, ha⟩
[GOAL]
case mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝ : DivisionMonoid α
g : Filter α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)
[PROOFSTEP]
exact ha.filter
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ 1 ≤ f / g ↔ ¬Disjoint f g
[PROOFSTEP]
refine' ⟨fun h hfg => _, _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
⊢ False
[PROOFSTEP]
obtain ⟨s, hs, t, ht, hst⟩ := hfg.le_bot (mem_bot : ∅ ∈ ⊥)
[GOAL]
case refine'_1.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False
[PROOFSTEP]
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ ¬Disjoint f g → 1 ≤ f / g
[PROOFSTEP]
rintro h s ⟨t₁, t₂, h₁, h₂, hs⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : ¬Disjoint f g
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
[PROOFSTEP]
exact hs (Set.one_mem_div_iff.2 fun ht => h <| disjoint_of_disjoint_of_mem ht h₁ h₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
⊢ 1 ≤ f / f
[PROOFSTEP]
rintro s ⟨t₁, t₂, h₁, h₂, hs⟩
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ := Set.not_disjoint_iff.1 (h.not_disjoint h₁ h₂)
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ s ∈ 1
[PROOFSTEP]
rw [mem_one, ← div_self' a]
[GOAL]
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
h : NeBot f
s t₁ t₂ : Set α
h₁ : t₁ ∈ f
h₂ : t₂ ∈ f
hs : t₁ / t₂ ⊆ s
a : α
ha₁ : a ∈ t₁
ha₂ : a ∈ t₂
⊢ a / a ∈ s
[PROOFSTEP]
exact hs (Set.div_mem_div ha₁ ha₂)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Group α
inst✝¹ : DivisionMonoid β
inst✝ : MonoidHomClass F α β
m : F
f g f₁ g₁ : Filter α
f₂ g₂ : Filter β
⊢ IsUnit f ↔ ∃ a, f = pure a
[PROOFSTEP]
simp only [isUnit_iff, Group.isUnit, and_true_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ (a • b) • f = a • b • f
[PROOFSTEP]
simp only [← map_smul, map_map, smul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
b : β
f : Filter γ
⊢ map (fun b_1 => a • b • b_1) f = map ((fun b => a • b) ∘ fun b_1 => b • b_1) f
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
⊢ (a • f) • g = a • f • g
[PROOFSTEP]
refine' (map_map₂_distrib_left fun _ _ => _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
f : Filter β
g : Filter γ
x✝¹ : β
x✝ : γ
⊢ (fun x x_1 => x • x_1) a (x✝¹ • x✝) = (fun x x_1 => x • x_1) a x✝¹ • x✝
[PROOFSTEP]
exact (smul_assoc a _ _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ map (fun b => 1 • b) f = f
[PROOFSTEP]
simp_rw [one_smul, map_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
f : Filter β
⊢ 1 • f = f
[PROOFSTEP]
simp only [← map_smul, one_smul, map_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
a b : α
f : Filter β
⊢ (a * b) • f = a • b • f
[PROOFSTEP]
simp only [← map_smul, map_map, Function.comp, ← mul_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ pure ((fun x x_1 => x • x_1) x✝ 0) = 0
[PROOFSTEP]
dsimp only
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
x✝ : α
⊢ pure (x✝ • 0) = 0
[PROOFSTEP]
rw [smul_zero, pure_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1
[PROOFSTEP]
rw [smul_one, singleton_one]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
⊢ 0 • g ≤ 0
[PROOFSTEP]
refine' fun s hs => mem_smul_filter.2 _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s ∈ g
[PROOFSTEP]
convert @univ_mem _ g
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x x_1 => x • x_1) 0 ⁻¹' s = univ
[PROOFSTEP]
refine' eq_univ_iff_forall.2 fun a => _
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x x_1 => x • x_1) 0 ⁻¹' s
[PROOFSTEP]
dsimp only
[GOAL]
case h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s
[PROOFSTEP]
rwa [mem_preimage, zero_smul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ (fun x x_1 => x • x_1) 0 '' s ∈ 0
[PROOFSTEP]
simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
f : Filter α
g : Filter β
hg : NeBot g
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0
[PROOFSTEP]
exact zero_mem_zero
