awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
inst_7 : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a
have f₁ : f j * f i = ∏ k ∈ {j, i}, f k
Tactic: calc
    f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
inst_7 : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a
have f₁ : f j * f i = ∏ k ∈ {j, i}, f k
Tactic: classical
  calc
    f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂
have pos : ∀ (hL : L.NeBot), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
pos : ∀ (hL : L.NeBot), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂
have neg : ∀ (hL : ¬L.NeBot), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ a₂
have pos : ∀ (hf : Multipliable f L), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hf : Multipliable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
pos : ∀ (hf : Multipliable f L), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂
have neg : ∀ (hf : ¬Multipliable f L), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hf : Multipliable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ a₂
have pos : ∀ (hf : (mulSupport f).Finite), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hf : f.mulSupport.Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
pos : ∀ (hf : (mulSupport f).Finite), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂
have neg : ∀ (hf : ¬(mulSupport f).Finite), ∏'[L] (i : ι), f i ≤ a₂
Tactic: by_cases hf : f.mulSupport.Finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂
have neg : ∏ᶠ (b : ι), f b ≤ a₂
Tactic: rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have pos : ∀ (hg : Multipliable g L), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
Tactic: by_cases hg : Multipliable g L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
pos : ∀ (hg : Multipliable g L), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have neg : ∀ (hg : ¬Multipliable g L), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
Tactic: by_cases hg : Multipliable g L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have neg : ∀ (hL : ¬L.NeBot), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g L
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have neg : LE.le.{u_3} (α := α) 1 1
Tactic: rw [tprod_eq_one_of_not_multipliable hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have pos : ∀ (hf : Multipliable f L), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
Tactic: by_cases hf : Multipliable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
pos : ∀ (hf : Multipliable f L), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have neg : ∀ (hf : ¬Multipliable f L), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
Tactic: by_cases hf : Multipliable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have neg : ∀ (hL : ¬L.NeBot), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
Tactic: by_cases hL : L.NeBot
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have neg : LE.le.{u_3} (α := α) (∏ᶠ (i : ι), f i) 1
Tactic: simp only [tprod_bot hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f L
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
have neg : LE.le.{u_3} (α := α) 1 1
Tactic: rw [tprod_eq_one_of_not_multipliable hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ HasProd f 1 L ↔ f = 1
have refine_1 : ∀ (hf' : HasProd f 1 L), f = 1
Tactic: refine ⟨fun hf' ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
refine_1 : ∀ (hf' : HasProd f 1 L), f = 1
⊢ HasProd f 1 L ↔ f = 1
have refine_2 : f = 1 → HasProd f 1 L
Tactic: refine ⟨fun hf' ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1 L
⊢ f = 1
have refine_1 : ∀ (i : ι), f i = 1 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (hypothesis)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ a₁ < a₂
have this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1
Tactic: have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (hypothesis)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1
⊢ a₁ < a₂
have this₁ : 1 / f i * a₁ ≤ 1 / g i * a₂
Tactic: have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ a₁ < a₂
have have : ∀ (this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1), a₁ < a₂
Tactic: classical
  have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
  have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
  simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
have have₁ have₂ : ∀ (this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1), a₁ < a₂
⊢ a₁ < a₂
have have₃ : ∀ (this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1)
  (this : 1 / f i * a₁ ≤ 1 / g i * a₂), a₁ < a₂
Tactic: classical
  have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
  have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
  simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
g : ι → α
inst_6 : L.LeAtTop
inst_7 : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ LT.lt.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
have rw : LT.lt.{u_3} (α := α) (∏'[L] (x : ι), 1) (∏'[L] (i : ι), g i)
Tactic: rw [← tprod_one (L := L)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∀ (x : ι), f x = 1
have rw : Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ HasProd f 1
Tactic: rw [← hasProd_one_iff, hf.hasProd_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
rw : Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ HasProd f 1
⊢ Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∀ (x : ι), f x = 1
have rw₁ : Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ Eq.{u_3 + 1} (α := α) (∏' (b : ι), f b) 1
Tactic: rw [← hasProd_one_iff, hf.hasProd_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ Ne.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
have rw : ¬Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
Tactic: rw [Ne, hf.tprod_eq_one_iff, not_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
rw : ¬Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
⊢ Ne.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
have rw₁ : (¬∀ (x : ι), f x = 1) ↔ ∃ (x : ι), f x ≠ 1
Tactic: rw [Ne, hf.tprod_eq_one_iff, not_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
rw : ¬Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
rw₁ : (¬∀ (x : ι), f x = 1) ↔ ∃ (x : ι), f x ≠ 1
⊢ Ne.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
have rw₂ : (∃ (x : ι), ¬f x = 1) ↔ ∃ (x : ι), f x ≠ 1
Tactic: rw [Ne, hf.tprod_eq_one_iff, not_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (hypothesis)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
⊢ Finite ι
have H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
Tactic: have H : ∀ s : Finset ι, #s • b ≤ ∑' _ : ι, b := fun s ↦ by
    simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
⊢ Finite ι
have obtain : ∀ (n : ℕ) (hn : ∑' (x : ι), b ≤ n • b), Finite ι
Tactic: obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (hypothesis)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
⊢ Finite ι
have this : ∀ (s : Finset ι), #s ≤ n
Tactic: have : ∀ s : Finset ι, #s ≤ n := fun s ↦ by
    simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this : ∀ (s : Finset ι), #s ≤ n
⊢ Finite ι
have have : ∀ (this : Fintype ι), Finite ι
Tactic: have : Fintype ι := fintypeOfFinsetCardLe n this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ CauchySeq f
have lift : ∀ (d : (i : ℕ) → ℝ≥0) (hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n)
  (hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)), CauchySeq f
Tactic: lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
Cleared hypotheses: d, hf, hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n
hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)
⊢ CauchySeq f
have hf₁ : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ENNReal)
Tactic: apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n
hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)
hf₁ : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ENNReal)
⊢ CauchySeq f
have hd₁ : Summable d
Tactic: apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
have refine : ∀ (m : ℕ) (hnm : m ≥ n), dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
Tactic: refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
have refine : LE.le (α := ℝ) (∑ i ∈ Ico n m, d i) (∑' (m : ℕ), d (n + m))
Tactic: refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ LE.le (α := ℝ) (∑ i ∈ Ico n m, d i) (∑' (m : ℕ), d (n + m))
have rw : LE.le (α := ℝ) (∑ k ∈ range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))
Tactic: rw [sum_Ico_eq_sum_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ LE.le (α := ℝ) (∑ k ∈ range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))
have refine : Summable (α := ℝ) fun (k : ℕ) ↦ d (n + k)
Tactic: refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ¬Summable f ↔ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
have lift : ∀ (f : (i : ℕ) → ℝ≥0),
  (¬Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)) ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop atTop
Tactic: lift f to ℕ → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable f ↔ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
have rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
Tactic: rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
⊢ Summable f ↔ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
have rw₁ : ¬Summable f ↔ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
Tactic: rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]