awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
γ : Type u_3
β : Type u_4
f : γ ↪ β
simp :
  Eq.{u_3 + 1} (α := SummationFilter γ)
    { filter := Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop } { filter := atTop }
e_filter :
  ∀ (s : Set (Finset γ)),
    Membership.mem (γ := Filter (Finset γ)) (Filter.map (fun (s : Finset β) ↦ s.preimage (⇑f : (a : γ) → β) ⋯) atTop)
        s ↔
      Membership.mem (γ := Filter (Finset γ)) atTop s
e_filter₁ :
  ∀ (s : Set (Finset γ)),
    (∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s) ↔
      ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
e_filter₂ :
  ∀ (s : Set (Finset γ)) (t : Finset β) (ht : ∀ (b : Finset β), t ⊆ b → b.preimage (⇑f : (a : γ) → β) ⋯ ∈ s),
    ∃ (a : Finset γ), ∀ (b : Finset γ), a ⊆ b → b ∈ s
⊢ (unconditional β).comap f = unconditional γ
have e_filter₃ : ∀ (s : Set (Finset γ)) (t : Finset γ) (ht : ∀ (b : Finset γ), t ⊆ b → b ∈ s),
  ∃ (a : Finset β), ∀ (b : Finset β), a ⊆ b → b.preimage (⇑f : (a : γ) → β) sorry ∈ s
Tactic: classical
  simp only [unconditional, comap]
  congr 1 with s
  simp only [mem_map, mem_atTop_sets, ge_iff_le, Finset.le_eq_subset, mem_preimage]
  constructor <;> rintro ⟨t, ht⟩
  · refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
    simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left
  · exact ⟨_, fun b hb ↦ ht _ (Finset.map_subset_iff_subset_preimage.mp hb)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
⊢ L = unconditional β
have haveI : ∀ (this : Fintype β), L = unconditional β
Tactic: haveI := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
have rw : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici Finset.univ)) (pure Finset.univ)
Tactic: rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
rw : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici Finset.univ)) (pure Finset.univ)
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
have rw₁ : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici ⊤)) (pure ⊤)
Tactic: rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
rw : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici Finset.univ)) (pure Finset.univ)
rw₁ : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici ⊤)) (pure ⊤)
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
have rw₂ : Eq (α := Filter (Finset β)) (𝓟 {⊤}) (pure ⊤)
Tactic: rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
rw : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici Finset.univ)) (pure Finset.univ)
rw₁ : Eq.{u_4 + 1} (α := Filter (Finset β)) (𝓟 (Ici ⊤)) (pure ⊤)
rw₂ : Eq (α := Filter (Finset β)) (𝓟 {⊤}) (pure ⊤)
⊢ Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
have rw₃ : Eq.{u_4 + 1} (α := Filter (Finset β)) (pure ⊤) (pure ⊤)
Tactic: rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
⊢ L = unconditional β
have hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
Tactic: have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
⊢ L = unconditional β
have hL : L.filter ≤ atTop
Tactic: have hL := L.le_atTop
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
hL : L.filter ≤ atTop
⊢ L = unconditional β
have hL' : ∅ ∉ L.filter
Tactic: have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL : { filter := F : SummationFilter β }.filter ≤ atTop
hL' : ∅ ∉ { filter := F : SummationFilter β }.filter
⊢ { filter := F : SummationFilter β } = unconditional β
have mk : ∀ (hAtTop : True) (hL : F ≤ pure Finset.univ), { filter := F : SummationFilter β } = { filter := pure Finset.univ }
Tactic: simp only [unconditional, hAtTop] at *
Cleared hypotheses: hAtTop, hL
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ { filter := F : SummationFilter β } = { filter := pure Finset.univ }
have mk : F = pure Finset.univ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ F = pure Finset.univ
have mk : ∀ s ∈ F, Finset.univ ∈ s
Tactic: refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hL' : ∅ ∉ F
hAtTop : True
hL : F ≤ pure Finset.univ
⊢ ∀ s ∈ F, Finset.univ ∈ s
have mk : ∀ (hL' : ∃ s ∈ F, Finset.univ ∉ s), ∅ ∈ F
Tactic: contrapose! hL'
Cleared hypotheses: hL'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
this : Fintype β
F : Filter (Finset β)
inst_1 : { filter := F : SummationFilter β }.LeAtTop
inst_2 : { filter := F : SummationFilter β }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
hL' : ∃ s ∈ F, Finset.univ ∉ s
⊢ ∅ ∈ F
have mk : ∀ (s : Set (Finset β)) (hs : s ∈ F) (hs' : Finset.univ ∉ s), ∅ ∈ F
Tactic: obtain ⟨s, hs, hs'⟩ := hL'
Cleared hypotheses: hL'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
this : Fintype β
hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)
hL : L.filter ≤ atTop
hL' : ∅ ∉ L.filter
⊢ L = unconditional β
have mk : ∀ (F : Filter (Finset β)) [{ filter := F : SummationFilter β }.LeAtTop] [{ filter := F : SummationFilter β }.NeBot]
  (hL : { filter := F : SummationFilter β }.filter ≤ atTop) (hL' : ∅ ∉ { filter := F : SummationFilter β }.filter),
  { filter := F : SummationFilter β } = unconditional β
Tactic: cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
Cleared hypotheses: L, inst_1, inst_2, hL, hL'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
⊢ L = unconditional β
have haveI : ∀ (this : Fintype β), L = unconditional β
Tactic: classical
  haveI := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
haveI haveI₁ haveI₂ : ∀ (this : Fintype β), L = unconditional β
⊢ L = unconditional β
have haveI₃ : ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)), L = unconditional β
Tactic: classical
  haveI := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
haveI haveI₁ haveI₂ : ∀ (this : Fintype β), L = unconditional β
haveI₃ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)), L = unconditional β
⊢ L = unconditional β
have haveI₄ : ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)) (hL : L.filter ≤ atTop),
  L = unconditional β
Tactic: classical
  haveI := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
β : Type u_4
inst : Finite β
L : SummationFilter β
inst_1 : L.LeAtTop
inst_2 : L.NeBot
haveI haveI₁ haveI₂ : ∀ (this : Fintype β), L = unconditional β
haveI₃ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)), L = unconditional β
haveI₄ :
  ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ))
    (hL : L.filter ≤ atTop), L = unconditional β
⊢ L = unconditional β
have haveI₅ : ∀ (this : Fintype β) (hAtTop : Eq.{u_4 + 1} (α := Filter (Finset β)) atTop (pure Finset.univ)) (hL : L.filter ≤ atTop)
  (hL' : ∅ ∉ L.filter), L = unconditional β
Tactic: classical
  haveI := Fintype.ofFinite β
  have hAtTop : (atTop : Filter (Finset β)) = pure Finset.univ := by
    rw [(isTop_iff_eq_top.mpr rfl).atTop_eq (a := Finset.univ), ← Finset.top_eq_univ,
      Ici_top, principal_singleton]
  have hL := L.le_atTop
  have hL' : ∅ ∉ L.filter := empty_mem_iff_bot.not.mpr <| NeBot.ne_bot.ne'
  cases L with | mk F =>
  simp only [unconditional, hAtTop] at *
  congr 1
  refine eq_of_le_of_ge hL (pure_le_iff.mpr ?_)
  contrapose! hL'
  obtain ⟨s, hs, hs'⟩ := hL'
  simpa [inter_singleton_eq_empty.mpr hs'] using inter_mem hs (le_pure_iff.mp hL)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
n : ℕ
⊢ Finset.Iic n = Finset.range (n + 1)
have h : ∀ (x : ℕ), x ∈ Finset.Iic n ↔ x ∈ Finset.range (n + 1)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (hypothesis)
Goal:
⊢ (conditional ℕ).filter = Filter.map Finset.range atTop
have this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
Tactic: have (n : ℕ) : Finset.Iic n = Finset.range (n + 1) := by ext x; simp [Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ (conditional ℕ).filter = Filter.map Finset.range atTop
have simp : Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop
Tactic: simp only [conditional_filter_eq_map_Iic, funext this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop
have a : Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop ≤ Filter.map Finset.range atTop
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
a : Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop ≤ Filter.map Finset.range atTop
⊢ Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop
have a₁ : Filter.map Finset.range atTop ≤ Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop (Filter.map Finset.range atTop)
have a : ∀ (s : Set (Finset ℕ)), (∃ (a : ℕ), ∀ b ≥ a, Finset.range b ∈ s) → ∃ (a : ℕ), ∀ b ≥ a, Finset.range (b + 1) ∈ s
Tactic: simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Tendsto Finset.range atTop (Filter.map (fun (x : ℕ) ↦ Finset.range (x + 1)) atTop)
have a : ∀ (s : Set (Finset ℕ)), (∃ (a : ℕ), ∀ b ≥ a, Finset.range (b + 1) ∈ s) → ∃ (a : ℕ), ∀ b ≥ a, Finset.range b ∈ s
Tactic: simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.SummationFilter (goal)
Goal:
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
s : Set (Finset ℕ)
a : ℕ
ha : ∀ b ≥ a, Finset.range (b + 1) ∈ s
b : ℕ
hb : b ≥ a + 1
⊢ Finset.range b ∈ s
have h : b = b - 1 + 1
Tactic: convert! ha (b - 1) (by lia)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Determinant (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousMul 𝕜
v : 𝕜
⊢ det (M := 𝕜) (toSpanSingleton 𝕜 v) = v
have rw : HMul.hMul (α := 𝕜) ((ContinuousLinearMap.id 𝕜 𝕜 : (a : 𝕜) → 𝕜) 1 : 𝕜) v = v
Tactic: rw [← smulRight_id, det_smulRight]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TopDualPairing (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Continuous (Y := 𝕜) fun (x : (E →L[𝕜] 𝕜) × E) ↦
    match (motive := (E →L[𝕜] 𝕜) × E → 𝕜) x with
    | (x, y) => (((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y
have this : IsModuleTopology 𝕜 E
Tactic: haveI : IsModuleTopology 𝕜 E := isModuleTopologyOfFiniteDimensional
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TopDualPairing (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
this : IsModuleTopology 𝕜 E
⊢ Continuous (Y := 𝕜) fun (x : (E →L[𝕜] 𝕜) × E) ↦
    match (motive := (E →L[𝕜] 𝕜) × E → 𝕜) x with
    | (x, y) => (((topDualPairing 𝕜 E : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜) x : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) y
have this₁ : IsModuleTopology 𝕜 (E →L[𝕜] 𝕜)
Tactic: haveI : IsModuleTopology 𝕜 (E →L[𝕜] 𝕜) := isModuleTopologyOfFiniteDimensional
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TopDualPairing (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Function.Bijective (β := (E →L[𝕜] 𝕜) →L[𝕜] 𝕜) fun (y : E) ↦
    { toLinearMap := (LinearMap.flip (topDualPairing 𝕜 E) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜) y, cont := ⋯ }
have refine : Function.Bijective (α := E) (β := (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
  (⇑(LinearMap.flip (topDualPairing 𝕜 E)) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
Tactic: refine LinearMap.toContinuousLinearMap.bijective.comp ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.TopDualPairing (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_2
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : FiniteDimensional 𝕜 E
inst_8 : T2Space E
⊢ Function.Bijective (α := E) (β := (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
    (⇑(LinearMap.flip (topDualPairing 𝕜 E)) : (a : E) → (E →L[𝕜] 𝕜) →ₗ[𝕜] 𝕜)
have rw : Function.Bijective (α := E →L[𝕜] 𝕜) (β := E →ₗ[𝕜] 𝕜) (⇑(topDualPairing 𝕜 E) : (a : E →L[𝕜] 𝕜) → E →ₗ[𝕜] 𝕜)
Tactic: rw [LinearMap.flip_bijective_iff₁]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := 𝕜) (fun (x : α) ↦ f x * g x) l atTop
have refine : EventuallyLE.{u_2, u_1} (β := 𝕜) l (fun (x : α) ↦ f x * (C / 2)) fun (x : α) ↦ f x * g x
Tactic: refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ EventuallyLE.{u_2, u_1} (β := 𝕜) l (fun (x : α) ↦ f x * (C / 2)) fun (x : α) ↦ f x * g x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ C / 2 < g x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 ≤ f x) x} x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦ LE.le.{u_1} (α := 𝕜) ((fun (x : α) ↦ f x * (C / 2)) x) ((fun (x : α) ↦ f x * g x) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ C / 2 < g x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 ≤ f x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦ LE.le.{u_1} (α := 𝕜) ((fun (x : α) ↦ f x * (C / 2)) x) ((fun (x : α) ↦ f x * g x) x))
                      x}
                  x}
            x}
      a
⊢ EventuallyLE.{u_2, u_1} (β := 𝕜) l (fun (x : α) ↦ f x * (C / 2)) fun (x : α) ↦ f x * g x
have h₁ : ∀ (a : α), C / 2 < g a → 0 ≤ f a → f a * (C / 2) ≤ f a * g a
Tactic: filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (𝓝[>] 0)⁻¹ atTop
have rw : Eq.{u_1 + 1} (α := Filter 𝕜) atTop⁻¹⁻¹ atTop
Tactic: rw [← inv_atTop₀, inv_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
rw : Eq.{u_1 + 1} (α := Filter 𝕜) atTop⁻¹⁻¹ atTop
⊢ Eq.{u_1 + 1} (α := Filter 𝕜) (𝓝[>] 0)⁻¹ atTop
have rw₁ : Eq.{u_1 + 1} (α := Filter 𝕜) atTop atTop
Tactic: rw [← inv_atTop₀, inv_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun (x : 𝕜) ↦ f x⁻¹) atTop l
⊢ Tendsto f (𝓝[>] 0) l
have h₁ : f = (fun (x : 𝕜) ↦ f x⁻¹) ∘ fun (x : 𝕜) ↦ x⁻¹
Tactic: convert! h.comp tendsto_inv_nhdsGT_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
have lift : ∀ (N : ℕ) (h : (↑N : ℤ) = -n), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
Tactic: lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : (↑N : ℤ) = -n
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
have rw : ∀ (N : ℕ) (hn : 0 < N) (h : (↑N : ℤ) = -n), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ n) atTop (𝓝 0)
Tactic: rw [← neg_pos, ← h, Nat.cast_pos] at hn
Cleared hypotheses: hn, N, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Field (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
inst : Semifield 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst_5 : ContinuousMul 𝕜
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'
have refine_1 : ∀ (x : 𝕜) (hx : x < 1), ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
Tactic: refine ⟨fun x hx => ?_, fun x hx => ?_⟩