awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (α := { x : α // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw₂ : Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto (fun (x : { x : α // x ∈ Ioi a }) ↦ f (↑x : α)) atTop l
Tactic: rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw : Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto f (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) l
Tactic: rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) l
⊢ Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw₁ : Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto (α := { x : α // x ∈ Ici a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop l
Tactic: rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (α := { x : α // x ∈ Ici a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop l
⊢ Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l
have rw₂ : Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
  Tendsto (fun (x : { x : α // x ∈ Ici a }) ↦ f (↑x : α)) atTop l
Tactic: rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
k a : ℕ
h : a ≥ k
⊢ a ≤ (fun (x : ℕ) ↦ x - k) a + k
have rw : a ≤ a
Tactic: rw [Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
k b : ℕ
h : b ≥ 0
⊢ b ≤ (fun (x : ℕ) ↦ x + k) b - k
have rw : b ≤ b
Tactic: rw [Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto (α := ℕ) (f ∘ fun (n : ℕ) ↦ n + k) atTop l ↔ Tendsto f atTop l
have rw : Tendsto f (map (fun (n : ℕ) ↦ n + k) atTop) l ↔ Tendsto f atTop l
Tactic: rw [← tendsto_map'_iff, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
rw : Tendsto f (map (fun (n : ℕ) ↦ n + k) atTop) l ↔ Tendsto f atTop l
⊢ Tendsto (α := ℕ) (f ∘ fun (n : ℕ) ↦ n + k) atTop l ↔ Tendsto f atTop l
have rw₁ : Tendsto f atTop l ↔ Tendsto f atTop l
Tactic: rw [← tendsto_map'_iff, map_add_atTop_eq_nat]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
k : ℕ
hk : 0 < k
a b : ℕ
h : b ≥ 1
⊢ a / k ≤ b ↔ a ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b
have rw : a ≤ k * b + (k - 1) ↔ a ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b
Tactic: rw [Nat.div_le_iff_le_mul_add_pred hk]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
k : ℕ
hk : 0 < k
b : ℕ
h : b ≥ 1
⊢ b ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b / k
have rw : k - 1 < k
Tactic: rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeInf α
f g : β → α
F : Filter β
hf : Tendsto f F atTop
hg : Tendsto g F atTop
⊢ Tendsto.{u_7, u_6} (β := α) (fun (x : β) ↦ f x ⊓ g x) F atTop
have rw : ∀ (hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a) (hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a) (b : α),
  ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a
Tactic: rw [Filter.tendsto_atTop] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeSup α
f g : β → α
F : Filter β
hf : Tendsto f F atBot
hg : Tendsto g F atBot
⊢ Tendsto.{u_7, u_6} (β := α) (fun (x : β) ↦ f x ⊔ g x) F atBot
have rw : ∀ (hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b) (hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b) (b : α),
  ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b
Tactic: rw [Filter.tendsto_atBot] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False
have this : ∀ (x : α), f x ≤ M
Tactic: have : ∀ x, f x ≤ M := by aesop
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this : ∀ (x : α), f x ≤ M
⊢ False
have this₁ : ∅ = f ⁻¹' Ioi M
Tactic: have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_gt)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this_1 : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ False
have apply : ∅ ∈ l
Tactic: apply Filter.empty_notMem l
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Basic (goal)
Goal:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
have choose : ∀ (ns : (a : ℕ) → ℕ) (hge : ∀ (a : ℕ), ns a ≥ a) (hns : ∀ (a : ℕ), p (x (ns a))),
  ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
Tactic: choose ns hge hns using frequently_atTop.1 h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)
have 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)
Tactic: refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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
⊢ ∃ (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)
have let : ∀ (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: let ⟨v, hv⟩ := h_eq b
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
have 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)
Tactic: refine ⟨v, trivial, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)
have 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)
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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)
have 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)
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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)
have 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)
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
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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
⊢ 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)
have 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)
Tactic: haveI := Classical.decEq β
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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 β
⊢ 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)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
⊢ 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)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
have 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))
Tactic: refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
have 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)
Tactic: refine map_atTop_finsetProd_le_of_prod_eq fun s => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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))
have a : ∀ (t : Finset α) (ht : s.preimage g sorry ⊆ t),
  ∃ (u' : Finset β), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f x) (∏ b ∈ t, f (g b))
Tactic: refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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))
have a : Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ b ∈ t, f (g b))
Tactic: refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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) (∏ b ∈ t, f (g b))
have a : Eq.{u_3 + 1} (α := M) (∏ x ∈ image g t ∪ s, f x) (∏ x ∈ image g t, f x)
Tactic: rw [← Finset.prod_image hg.injOn]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
have a : ∀ x ∈ image g t ∪ s, x ∉ image g t → f x = 1
Tactic: refine (prod_subset subset_union_left ?_).symm
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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 ∈ image g t ∪ s, x ∉ image g t → f x = 1
have a : ∀ (x : β), (∃ a ∈ t, g a = x) ∨ x ∈ s → (¬∃ a ∈ t, g a = x) → f x = 1
Tactic: simp only [Finset.mem_union, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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
have 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
Tactic: refine fun y hy hyt => hf y (mt ?_ hyt)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)
have 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)
Tactic: refine ⟨s.image g, fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.BigOperators (goal)
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)) (∏ b ∈ t, f b)
have a : ∃ (u' : Finset α), s ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', f (g x)) (∏ x ∈ t.preimage g sorry, f (g x))
Tactic: simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
⊢ Eq.{u_6 + 1} (α := Filter α) atTop ⊤
have refine : ∀ (s : Set α) (hs : Membership.mem (γ := Filter α) atTop s) (x : α), x ∈ s
Tactic: refine top_unique fun s hs x => ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
Goal:
α : Type u_6
inst : Subsingleton α
inst_1 : Preorder α
s : Set α
hs : Membership.mem (γ := Filter α) atTop s
x : α
⊢ x ∈ s
have rw : ∀ (x : α) (hs : Ici x ⊆ s), x ∈ s
Tactic: rw [atTop, ciInf_subsingleton x, mem_principal] at hs
Cleared hypotheses: hs, x
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
have this : Nonempty α
Tactic: have : Nonempty α := nonempty_of_neBot l
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (hypothesis)
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 α
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
have this₁ : Nonempty β
Tactic: have : Nonempty β := .map g ‹_›
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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)
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
have rw₁ : BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
Tactic: rw [← csInf_upperBounds_range, ← csInf_upperBounds_range,
    ← hf.upperBounds_range_comp_tendsto_atTop hg, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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)
have rw : ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
Tactic: rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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)
⊢ ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
have rwa : ¬Set.Nonempty.{u_5} (α := γ) (upperBounds (range fun (a : α) ↦ f (g a)))
Tactic: rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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)))
⊢ ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
have rwa₁ : ¬(upperBounds (range (f ∘ g))).Nonempty
Tactic: rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]