awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Inv β
h : EventuallyConst f l
⊢ EventuallyConst f⁻¹ l

Tactic:
h.comp Inv.inv

Premises used: Inv.inv, Filter.EventuallyConst.comp
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lb : Filter β
g : β → γ
hg : EventuallyConst g lb
hf : Tendsto f l lb
⊢ EventuallyConst (g ∘ f) l

Tactic:
hg.anti hf

Premises used: Set.Mem, Filter.map, setOf, Filter.EventuallyConst, Set.preimage, Filter.EventuallyConst.anti
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
ι : Type u_5
p : ι → Type u_6
g : α → (x : ι) → p x
h : EventuallyConst g l
i : ι
⊢ EventuallyConst.{u_1, u_6} (β := p i) (fun (x : α) ↦ g x i) l

Tactic:
h.comp <| Function.eval i

Premises used: Function.eval, Filter.EventuallyConst.comp
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f : α → β
g : α → γ
hf : EventuallyConst f l
op : β → γ → δ
hg : EventuallyConst g l
⊢ EventuallyConst.{u_1, u_4} (β := δ) (fun (x : α) ↦ op (f x) (g x)) l

Tactic:
((hf.prod hg).map op.uncurry).anti <|
    (tendsto_map (f := op.uncurry)).comp (tendsto_map.prodMk tendsto_map)

Premises used: Filter.EventuallyConst, Filter.Subsingleton.prod, Filter.Subsingleton.map, Filter.tendsto_map, Filter.Tendsto.prodMk, Filter.Subsingleton.anti, Filter.Tendsto.comp, Function.uncurry
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : α → γ
hf : EventuallyConst f l
hg : EventuallyConst g l
⊢ EventuallyConst (β := β × γ) (fun (x : α) ↦ (f x, g x)) l

Tactic:
hf.comp₂ Prod.mk hg

Premises used: Prod.mk, Filter.EventuallyConst.comp₂
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Mul β
g : α → β
hf : EventuallyConst f l
hg : EventuallyConst g l
⊢ EventuallyConst (f * g) l

Tactic:
hf.comp₂ (· * ·) hg

Premises used: HMul.hMul, Filter.EventuallyConst.comp₂
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
h : EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l
hc : c ≠ 1
⊢ EventuallyConst s l

Tactic:
simpa [Function.comp_def, hc, imp_false] using h.comp (· = c)

Premises used: imp_false, Function.comp_def, Eq, Filter.EventuallyConst.comp
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
h : EventuallyConst s l
c : β
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l

Tactic:
h.comp (if · then c else 1)

Premises used: Set.Mem, Set.mulIndicator, OfNat.ofNat, Filter.EventuallyConst.comp, ite
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
h : EventuallyConst s l
c : β
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l

Tactic:
exact h.comp (if · then c else 1)

Premises used: OfNat.ofNat, Filter.EventuallyConst.comp, ite
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
h : EventuallyConst s l
c : β
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l

Tactic:
classical exact h.comp (if · then c else 1)
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
hc : c ≠ 1
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ EventuallyConst s l

Tactic:
⟨(of_mulIndicator_const · hc), (mulIndicator_const · c)⟩

Premises used: Filter.EventuallyConst.of_mulIndicator_const, Iff.intro, Filter.EventuallyConst.mulIndicator_const
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
inl :
  EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ 1) l ↔
    Eq.{u_2 + 1} (α := β) 1 1 ∨ EventuallyConst s l
inr :
  ∀ (hc : c ≠ 1), EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l

Tactic:
rcases eq_or_ne c 1 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ 1) l ↔
    Eq.{u_2 + 1} (α := β) 1 1 ∨ EventuallyConst s l

Tactic:
simp [mulIndicator_const_iff_of_ne, *]

Premises used: Filter.EventuallyConst.mulIndicator_const_iff_of_ne
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
inst : One β
s : Set α
c : β
hc : c ≠ 1
⊢ EventuallyConst.{u_1, u_2} (β := β) (s.mulIndicator fun (x : α) ↦ c) l ↔ c = 1 ∨ EventuallyConst s l

Tactic:
simp [mulIndicator_const_iff_of_ne, *]

Premises used: Filter.EventuallyConst.mulIndicator_const_iff_of_ne
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SemilatticeSup α
inst_1 : Nonempty α
⊢ (∃ (i : α), True ∧ ∀ y ∈ Ici i, f y = f i) ↔ ∃ (i : α), ∀ (j : α), i ≤ j → f j = f i

Tactic:
simp only [true_and, mem_Ici]

Premises used: Set.mem_Ici, true_and
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
rw : (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
⊢ EventuallyConst f atTop ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
rw [eventuallyConst_atTop]

Premises used: Filter.eventuallyConst_atTop
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
⊢ (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
refine_1 : ∀ (n : ℕ) (h : ∀ (j : ℕ), n ≤ j → f j = f n) (m : ℕ) (hm : n ≤ m), f (m + 1) = f m
refine_2 : ∀ (n : ℕ) (h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m) (m : ℕ) (hm : n ≤ m), f m = f n
⊢ (∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

Tactic:
(h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm

Premises used: Nat.le_succ, HAdd.hAdd, LE.le.trans, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

Tactic:
exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm

Premises used: Nat.le_succ, HAdd.hAdd, LE.le.trans, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n

Tactic:
rfl
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m_1 m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n

Tactic:
(h m hm).trans ihm

Premises used: Eq.trans
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m_1 m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n

Tactic:
exact (h m hm).trans ihm

Premises used: Eq.trans
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
refine_2 : f n = f n
refine_2₁ : ∀ (m : ℕ) (hm : n ≤ m) (ihm : f m = f n), f (m + 1) = f n
⊢ f m = f n

Tactic:
induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
p : Prop
⊢ IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p

Tactic:
Or.elim

Premises used: IsExtrOn, IsMaxOn, IsMinOn, IsExtrFilter, Or.elim
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
⊢ IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, IsMinFilter, IsMinOn, Set.Subset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
⊢ IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a

Tactic:
Iff.rfl

Premises used: Set.Mem, IsMaxOn, Filter.Eventually, Iff.rfl, setOf, Set.Subset, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
a : α
⊢ IsMinOn f univ a ↔ ∀ (x : α), f a ≤ f x

Tactic:
univ_subset_iff.trans eq_univ_iff_forall

Premises used: Set.univ_subset_iff, Set.Mem, Filter.Eventually, Set.eq_univ_iff_forall, setOf, IsMinFilter, IsMinOn, Set.Subset, Iff.trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
a : α
⊢ IsMaxOn f univ a ↔ ∀ (x : α), f x ≤ f a

Tactic:
univ_subset_iff.trans eq_univ_iff_forall

Premises used: Set.univ_subset_iff, Set.Mem, IsMaxOn, Filter.Eventually, Set.eq_univ_iff_forall, setOf, Set.Subset, Iff.trans, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
h : IsMinOn f s a
⊢ f a ∈ lowerBounds (f '' s)

Tactic:
simpa [mem_lowerBounds] using h

Premises used: mem_lowerBounds
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
rw : ∀ (b : β), b ≤ f a ↔ Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ s, f x_1 = x}) b
⊢ IsGLB {x : β | ∃ x_1 ∈ s, f x_1 = x} (f a)

Tactic:
rw [isGLB_iff_le_iff]

Premises used: isGLB_iff_le_iff
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
simp : b ≤ f a ↔ ∀ a ∈ s, b ≤ f a
⊢ b ≤ f a ↔ Membership.mem (γ := Set β) (lowerBounds {x : β | ∃ x_1 ∈ s, f x_1 = x}) b

Tactic:
simp only [mem_lowerBounds, mem_setOf_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, forall_exists_index, mem_lowerBounds, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ ∀ a ∈ s, b ≤ f a

Tactic:
⟨fun hba x hx ↦ le_trans hba (hfsa hx), fun hb ↦ hb a ha⟩

Premises used: Iff.intro, le_trans
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ ∀ a ∈ s, b ≤ f a

Tactic:
exact ⟨fun hba x hx ↦ le_trans hba (hfsa hx), fun hb ↦ hb a ha⟩
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMaxOn f s a
⊢ IsLUB {x : β | ∃ x_1 ∈ s, f x_1 = x} (f a)

Tactic:
IsMinOn.isGLB (α := αᵒᵈ) (β := βᵒᵈ) ha hfsa

Premises used: IsMinOn.isGLB, lowerBounds, Set.Mem, setOf, upperBounds, IsLeast, IsLUB, OrderDual
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
h : IsMaxOn f s a
⊢ f a ∈ upperBounds (f '' s)

Tactic:
simpa [mem_upperBounds] using h

Premises used: mem_upperBounds
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
h : IsMinFilter f l a
⊢ Tendsto f l (𝓟 (Ici (f a)))

Tactic:
tendsto_principal.2 h

Premises used: Iff.mpr, Filter.tendsto_principal
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
h : IsMaxFilter f l a
⊢ Tendsto f l (𝓟 (Iic (f a)))

Tactic:
tendsto_principal.2 h

Premises used: Iff.mpr, Filter.tendsto_principal
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
⊢ IsMinFilter f l a → IsExtrFilter f l a

Tactic:
Or.inl

Premises used: IsExtrFilter, Or.inl
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
⊢ IsMaxFilter f l a → IsExtrFilter f l a

Tactic:
Or.inr

Premises used: IsExtrFilter, Or.inr
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
h : IsMinOn f s a
⊢ IsExtrOn f s a

Tactic:
IsMinFilter.isExtr h

Premises used: IsExtrOn, IsMinFilter.isExtr
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
h : IsMaxOn f s a
⊢ IsExtrOn f s a

Tactic:
IsMaxFilter.isExtr h

Premises used: IsExtrOn, IsMaxFilter.isExtr
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
a : α
b : β
⊢ IsMinFilter.{u, v} (β := β) (fun (x : α) ↦ b) l a

Tactic:
univ_mem' fun _ => le_rfl

Premises used: le_rfl, Filter.Eventually, IsMinFilter, Filter.univ_mem'
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
a : α
b : β
⊢ IsMaxFilter.{u, v} (β := β) (fun (x : α) ↦ b) l a

Tactic:
univ_mem' fun _ => le_rfl

Premises used: le_rfl, Filter.Eventually, Filter.univ_mem', IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
l : Filter α
a : α
b : β
⊢ IsExtrFilter.{u, v} (β := β) (fun (x : α) ↦ b) l a

Tactic:
isMinFilter_const.isExtr

Premises used: IsMinFilter.isExtr, isMinFilter_const
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
s : Set α
a : α
b : β
⊢ IsMinOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isMinFilter_const

Premises used: IsMinOn, isMinFilter_const
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
s : Set α
a : α
b : β
⊢ IsMaxOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isMaxFilter_const

Premises used: IsMaxOn, isMaxFilter_const
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
s : Set α
a : α
b : β
⊢ IsExtrOn.{u, v} (β := β) (fun (x : α) ↦ b) s a

Tactic:
isExtrFilter_const

Premises used: IsExtrOn, isExtrFilter_const
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
l : Filter α
a : α
β : Type u_1
inst : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
⊢ ∀ (a_1 : α), f a ≤ f a_1 → f a_1 ≤ f a → f a_1 = f a

Tactic:
grind
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
l : Filter α
a : α
β : Type u_1
inst : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f a ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f a) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = (fun (x : α) ↦ f a) x) x} x}
            x}
      a_1
h₃ : ∀ (a_1 : α), f a ≤ f a_1 → f a_1 ≤ f a → f a_1 = f a
⊢ f =ᶠ[l] fun (x : α) ↦ f a

Tactic:
filter_upwards [h₁, h₂] using by grind
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
⊢ IsMinFilter (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) l a ↔ IsMaxFilter f l a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
⊢ IsMaxFilter (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) l a ↔ IsMinFilter f l a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsMinFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
⊢ IsExtrFilter (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) l a ↔ IsExtrFilter f l a

Tactic:
or_comm

Premises used: IsMinFilter, IsExtrFilter, or_comm, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
⊢ IsMinOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s a ↔ IsMaxOn f s a

Tactic:
Iff.rfl

Premises used: IsMaxOn, Iff.rfl, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
⊢ IsMaxOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s a ↔ IsMinOn f s a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsMinFilter, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
⊢ IsExtrOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s a ↔ IsExtrOn f s a

Tactic:
or_comm

Premises used: IsExtrOn, IsMinFilter, IsExtrFilter, or_comm, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
l' : Filter α
h : IsMinFilter f l a
hl : l' ≤ l
⊢ IsMinFilter f l' a

Tactic:
hl h

Premises used: Filter.Eventually, IsMinFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
l' : Filter α
h : IsMaxFilter f l a
hl : l' ≤ l
⊢ IsMaxFilter f l' a

Tactic:
hl h

Premises used: Filter.Eventually, IsMaxFilter
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
l' : Filter α
h : IsExtrFilter f l a
hl : l' ≤ l
⊢ IsExtrFilter f l' a

Tactic:
h.elim (fun h => (h.filter_mono hl).isExtr) fun h => (h.filter_mono hl).isExtr

Premises used: IsMinFilter.filter_mono, IsMaxFilter.filter_mono, IsMinFilter.isExtr, IsMaxFilter.isExtr, Or.elim
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
h : IsMinFilter f l a
l' : Filter α
⊢ IsMinFilter f (l ⊓ l') a

Tactic:
h.filter_mono inf_le_left

Premises used: IsMinFilter.filter_mono, inf_le_left
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
h : IsMaxFilter f l a
l' : Filter α
⊢ IsMaxFilter f (l ⊓ l') a

Tactic:
h.filter_mono inf_le_left

Premises used: IsMaxFilter.filter_mono, inf_le_left
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
l : Filter α
a : α
h : IsExtrFilter f l a
l' : Filter α
⊢ IsExtrFilter f (l ⊓ l') a

Tactic:
h.filter_mono inf_le_left

Premises used: inf_le_left, IsExtrFilter.filter_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsMinOn f t a
h : s ⊆ t
⊢ IsMinOn f s a

Tactic:
hf.filter_mono <| principal_mono.2 h

Premises used: Iff.mpr, IsMinFilter.filter_mono, Filter.principal_mono, IsMinOn
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsMaxOn f t a
h : s ⊆ t
⊢ IsMaxOn f s a

Tactic:
hf.filter_mono <| principal_mono.2 h

Premises used: Iff.mpr, Filter.principal_mono, IsMaxOn, IsMaxFilter.filter_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
t : Set α
hf : IsExtrOn f t a
h : s ⊆ t
⊢ IsExtrOn f s a

Tactic:
hf.filter_mono <| principal_mono.2 h

Premises used: Iff.mpr, IsExtrOn, Filter.principal_mono, IsExtrFilter.filter_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
hf : IsMinOn f s a
t : Set α
⊢ IsMinOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: IsMinOn.on_subset, Set.inter_subset_left
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
hf : IsMaxOn f s a
t : Set α
⊢ IsMaxOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: Set.inter_subset_left, IsMaxOn.on_subset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
inst : Preorder β
f : α → β
s : Set α
a : α
hf : IsExtrOn f s a
t : Set α
⊢ IsExtrOn f (s ∩ t) a

Tactic:
hf.on_subset inter_subset_left

Premises used: IsExtrOn.on_subset, Set.inter_subset_left
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsMinFilter f l a
g : β → γ
hg : Monotone g
⊢ IsMinFilter (g ∘ f) l a

Tactic:
mem_of_superset hf fun _x hx => hg hx

Premises used: Filter.Eventually, IsMinFilter, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsMaxFilter f l a
g : β → γ
hg : Monotone g
⊢ IsMaxFilter (g ∘ f) l a

Tactic:
mem_of_superset hf fun _x hx => hg hx

Premises used: Filter.Eventually, IsMaxFilter, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsExtrFilter f l a
g : β → γ
hg : Monotone g
⊢ IsExtrFilter (g ∘ f) l a

Tactic:
hf.elim (fun hf => (hf.comp_mono hg).isExtr) fun hf => (hf.comp_mono hg).isExtr

Premises used: IsMaxFilter.comp_mono, IsMinFilter.comp_mono, IsMinFilter.isExtr, IsMaxFilter.isExtr, Or.elim
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsMinFilter f l a
g : β → γ
hg : Antitone g
⊢ IsMaxFilter (g ∘ f) l a

Tactic:
hf.dual.comp_mono fun _ _ h => hg h

Premises used: IsMinFilter.dual, IsMaxFilter.comp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsMaxFilter f l a
g : β → γ
hg : Antitone g
⊢ IsMinFilter (g ∘ f) l a

Tactic:
hf.dual.comp_mono fun _ _ h => hg h

Premises used: IsMinFilter.comp_mono, IsMaxFilter.dual
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
l : Filter α
a : α
hf : IsExtrFilter f l a
g : β → γ
hg : Antitone g
⊢ IsExtrFilter (g ∘ f) l a

Tactic:
hf.dual.comp_mono fun _ _ h => hg h

Premises used: IsExtrFilter.comp_mono, IsExtrFilter.dual
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsMinOn f s a
g : β → γ
hg : Monotone g
⊢ IsMinOn (g ∘ f) s a

Tactic:
IsMinFilter.comp_mono hf hg

Premises used: IsMinOn, IsMinFilter.comp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsMaxOn f s a
g : β → γ
hg : Monotone g
⊢ IsMaxOn (g ∘ f) s a

Tactic:
IsMaxFilter.comp_mono hf hg

Premises used: IsMaxOn, IsMaxFilter.comp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsExtrOn f s a
g : β → γ
hg : Monotone g
⊢ IsExtrOn (g ∘ f) s a

Tactic:
IsExtrFilter.comp_mono hf hg

Premises used: IsExtrOn, IsExtrFilter.comp_mono
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsMinOn f s a
g : β → γ
hg : Antitone g
⊢ IsMaxOn (g ∘ f) s a

Tactic:
IsMinFilter.comp_antitone hf hg

Premises used: IsMaxOn, IsMinFilter.comp_antitone
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsMaxOn f s a
g : β → γ
hg : Antitone g
⊢ IsMinOn (g ∘ f) s a

Tactic:
IsMaxFilter.comp_antitone hf hg

Premises used: IsMinOn, IsMaxFilter.comp_antitone
-- Module: Mathlib.Order.Filter.Extr
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder β
inst_1 : Preorder γ
f : α → β
s : Set α
a : α
hf : IsExtrOn f s a
g : β → γ
hg : Antitone g
⊢ IsExtrOn (g ∘ f) s a

Tactic:
IsExtrFilter.comp_antitone hf hg

Premises used: IsExtrOn, IsExtrFilter.comp_antitone