awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
b : Finset β
h : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
⊢ ∃ (i : Finset α),
    True ∧
      Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
        ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)

Tactic:
⟨v, trivial, ?_⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
b : Finset β
h : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
refine :
  Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici v)
    ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
⊢ ∃ (i : Finset α),
    True ∧
      Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
        ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)

Tactic:
refine ⟨v, trivial, ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
b : Finset β
h : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
⊢ Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici v)
    ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)

Tactic:
simpa [Finset.image_subset_iff] using hv

Premises used: Finset.image_subset_iff
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
refine :
  ∀ (b : Finset β),
    True →
      ∃ (i : Finset α),
        True ∧
          Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
            ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
refine₁ :
  ∀ (b : Finset β),
    True →
      ∀ (v : Finset α)
        (hv :
          ∀ (v' : Finset α),
            v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)),
        ∃ (i : Finset α),
          True ∧
            Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
              ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
refine₂ :
  ∀ (b : Finset β),
    True →
      ∀ (v : Finset α)
        (hv :
          ∀ (v' : Finset α),
            v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)),
        Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici v)
          ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)

Tactic:
classical
    refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_
    let ⟨v, hv⟩ := h_eq b
    refine ⟨v, trivial, ?_⟩
    simpa [Finset.image_subset_iff] using hv

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map, Finset.image_subset_iff
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
haveI :
  ∀ (this : DecidableEq β),
    Eq.{u_3 + 1} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
      (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)
⊢ Eq.{u_3 + 1} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
    (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)

Tactic:
haveI := Classical.decEq β
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
a :
  LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
    (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)
a₁ :
  LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)
    (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
⊢ Eq.{u_3 + 1} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
    (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
    (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)

Tactic:
map_atTop_finsetProd_le_of_prod_eq fun s => ?_

Premises used: Filter.map_atTop_finsetProd_le_of_prod_eq
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
a :
  ∀ (s : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (g b))
⊢ LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)
    (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)

Tactic:
refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_

Premises used: Filter.map_atTop_finsetProd_le_of_prod_eq
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
⊢ LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)
    (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)

Tactic:
map_atTop_finsetProd_le_of_prod_eq fun s => ?_

Premises used: Filter.map_atTop_finsetProd_le_of_prod_eq
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
a :
  ∀ (s : Finset α),
    ∃ (v : Finset β),
      ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ b ∈ v', f b)
⊢ LE.le.{u_3} (α := Filter M) (Filter.map (fun (s : Finset β) ↦ ∏ i ∈ s, f i) atTop)
    (Filter.map (fun (s : Finset α) ↦ ∏ i ∈ s, f (g i)) atTop)

Tactic:
refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_

Premises used: Filter.map_atTop_finsetProd_le_of_prod_eq
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ (v : Finset α),
    ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (g b))

Tactic:
⟨s.preimage g hg.injOn, fun t ht => ?_⟩

Premises used: Function.Injective.injOn, Finset.preimage, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
a :
  ∀ (t : Finset α) (ht : s.preimage g ⋯ ⊆ t),
    ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ t, f (g b))
⊢ ∃ (v : Finset α),
    ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ v', f (g b))

Tactic:
refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ t, f (g b))

Tactic:
⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩

Premises used: And.intro, Exists.intro, Union.union, Finset.subset_union_right, Finset.image
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
a : Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ b ∈ t, f (g b))
⊢ ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ t, f (g b))

Tactic:
refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
a : Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ x ∈ image g t, f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ b ∈ t, f (g b))

Tactic:
rw [← Finset.prod_image hg.injOn]

Premises used: Function.Injective.injOn, Finset.prod_image
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ x ∈ image g t, f x)

Tactic:
(prod_subset subset_union_left ?_).symm

Premises used: Finset.subset_union_left, Finset.prod_subset, Eq.symm
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
a : ∀ x ∈ image g t ∪ s, x ∉ image g t → f x = 1
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ x ∈ image g t, f x)

Tactic:
refine (prod_subset subset_union_left ?_).symm

Premises used: Finset.subset_union_left, Finset.prod_subset, Eq.symm
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
a : ∀ (x : β), (∃ a ∈ t, g a = x) ∨ x ∈ s → (¬∃ a ∈ t, g a = x) → f x = 1
⊢ ∀ x ∈ image g t ∪ s, x ∉ image g t → f x = 1

Tactic:
simp only [Finset.mem_union, Finset.mem_image]

Premises used: Finset.mem_image, Finset.mem_union
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∀ (x : β), (∃ a ∈ t, g a = x) ∨ x ∈ s → (¬∃ a ∈ t, g a = x) → f x = 1

Tactic:
fun y hy hyt => hf y (mt ?_ hyt)

Premises used: mt
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
a : ∀ (y : β) (hy : (∃ a ∈ t, g a = y) ∨ y ∈ s) (hyt : ¬∃ a ∈ t, g a = y), y ∈ Set.range g → ∃ a ∈ t, g a = y
⊢ ∀ (x : β), (∃ a ∈ t, g a = x) ∨ x ∈ s → (¬∃ a ∈ t, g a = x) → f x = 1

Tactic:
refine fun y hy hyt => hf y (mt ?_ hyt)

Premises used: mt
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
x : α
hy : (∃ a ∈ t, g a = g x) ∨ g x ∈ s
hyt : ¬∃ a ∈ t, g a = g x
⊢ ∃ a ∈ t, g a = g x

Tactic:
⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩

Premises used: Iff.mpr, Or.resolve_left, Finset.mem_preimage, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
x : α
hy : (∃ a ∈ t, g a = g x) ∨ g x ∈ s
hyt : ¬∃ a ∈ t, g a = g x
⊢ ∃ a ∈ t, g a = g x

Tactic:
exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
⊢ ∃ (v : Finset β),
    ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ b ∈ v', f b)

Tactic:
⟨s.image g, fun t ht => ?_⟩

Premises used: Exists.intro, Finset.image
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
a :
  ∀ (t : Finset β) (ht : image g s ⊆ t),
    ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ b ∈ t, f b)
⊢ ∃ (v : Finset β),
    ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ b ∈ v', f b)

Tactic:
refine ⟨s.image g, fun t ht => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
t : Finset β
ht : image g s ⊆ t
a : ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ x ∈ t.preimage g ⋯, f (g x))
⊢ ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ b ∈ t, f b)

Tactic:
simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]

Premises used: Function.Injective.injOn, Finset.prod_preimage
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
t : Finset β
ht : image g s ⊆ t
⊢ ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ x ∈ t.preimage g ⋯, f (g x))

Tactic:
⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩

Premises used: Finset.image_subset_iff_subset_preimage, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset α
t : Finset β
ht : image g s ⊆ t
⊢ ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ x ∈ t.preimage g ⋯, f (g x))

Tactic:
exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
⊢ Eq.{u_6 + 1} (α := Filter α) atTop ⊤

Tactic:
top_unique fun s hs x => ?_

Premises used: top_unique
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
refine : ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) atTop s) (x : α), x ∈ s
⊢ Eq.{u_6 + 1} (α := Filter α) atTop ⊤

Tactic:
refine top_unique fun s hs x => ?_

Premises used: top_unique
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
s : Set α
hs : Membership.mem (γ := Filter α) atTop s
x : α
rw : ∀ (x : α) (hs : Ici x ⊆ s), x ∈ s
⊢ x ∈ s

Tactic:
rw [atTop, ciInf_subsingleton x, mem_principal] at hs

Premises used: ciInf_subsingleton, Filter.atTop, Filter.mem_principal
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s

Tactic:
hs self_mem_Ici

Premises used: Set.self_mem_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s

Tactic:
exact hs self_mem_Ici

Premises used: Set.self_mem_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
⊢ Eq.{u_6 + 1} (α := Filter α) atBot ⊤

Tactic:
@Subsingleton.atTop_eq αᵒᵈ _ _

Premises used: Filter.Subsingleton.atTop_eq, Set.Mem, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
⊢ Nonempty α

Tactic:
have : Nonempty α := nonempty_of_neBot l
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this : Nonempty α
⊢ Nonempty β

Tactic:
have : Nonempty β := .map g ‹_›
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this_1 : Nonempty α
this : Nonempty β
rw : BddAbove (range f)
rw₁ : BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
rw [← csInf_upperBounds_range, ← csInf_upperBounds_range,
    ← hf.upperBounds_range_comp_tendsto_atTop hg, Function.comp_def]

Premises used: csInf_upperBounds_range, Monotone.upperBounds_range_comp_tendsto_atTop, Function.comp_def
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this_1 : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

Tactic:
hb
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this_1 : Nonempty α
this : Nonempty β
⊢ BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))

Tactic:
hb.mono <| range_comp_subset_range _ _

Premises used: Set.range_comp_subset_range, BddAbove.mono
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
this_1 : Nonempty α
this : Nonempty β
⊢ BddAbove (range f)

Tactic:
exacts [hb, hb.mono <| range_comp_subset_range _ _]

Premises used: Set.range_comp_subset_range, BddAbove.mono
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
hb : BddBelow (range f)
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.dual.ciSup_comp_tendsto_atTop hb hg

Premises used: iInf, Monotone.dual, OrderDual, Monotone.ciSup_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Antitone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
hf.dual_left.ciSup_comp_tendsto_atTop hb hg

Premises used: Antitone.dual_left, OrderDual, Monotone.ciSup_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Antitone f
hb : BddBelow (range f)
g : α → β
hg : Tendsto g l atTop
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.dual.ciSup_comp_tendsto_atBot hb hg

Premises used: iInf, Antitone.dual, Antitone.ciSup_comp_tendsto_atBot, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : BddAbove (range f)
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
hf.ciSup_comp_tendsto_atTop hb hg

Premises used: Monotone.ciSup_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : BddAbove (range f)
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
exact hf.ciSup_comp_tendsto_atTop hb hg

Premises used: Monotone.ciSup_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
rw : ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]

Premises used: iSup, csSup_of_not_bddAbove
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
hb : ¬BddAbove (range f)
rwa : ¬Set.Nonempty.{u_5} (α := γ) (upperBounds (range fun (a : α) ↦ f (g a)))
rwa₁ : ¬(upperBounds (range (f ∘ g))).Nonempty
rwa₂ rwa₃ rwa₄ rwa₅ : ¬(upperBounds (range f)).Nonempty
⊢ ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))

Tactic:
rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

Premises used: BddAbove, Monotone.upperBounds_range_comp_tendsto_atTop, Function.comp_def