awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq l
inst_3 : T2Space R
f : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
⊢ Eq (α := Matrix ((i : l) × m' i) ((i : l) × n' i) R) (blockDiagonal' (m' := m') (n' := n') (∑'[L] (x : X), f x))
    (∑'[L] (x : X), blockDiagonal' (m' := m') (n' := n') (f x))

Tactic:
Function.LeftInverse.map_tsum (g := blockDiagonal'AddMonoidHom m' n' R) f
    continuous_id.matrix_blockDiagonal' continuous_id.matrix_blockDiag' blockDiag'_blockDiagonal'

Premises used: Function.LeftInverse.map_tsum, Matrix.blockDiag'_blockDiagonal', continuous_id, Continuous.matrix_blockDiag', Matrix.blockDiagonal', Continuous.matrix_blockDiagonal'
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R
a : Matrix ((i : l) × m' i) ((i : l) × n' i) R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ (f x).blockDiag' (m' := m') (n' := n')) (a.blockDiag' (m' := m') (n' := n')) L

Tactic:
hf.map (blockDiag'AddMonoidHom m' n' R) continuous_id.matrix_blockDiag'

Premises used: HasSum.map, Matrix.blockDiag'AddMonoidHom, Matrix.blockDiag', continuous_id, Continuous.matrix_blockDiag'
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R
hf : Summable f L
⊢ Summable (α := (k : l) → Matrix.{u_9, u_10, u_8} (m' k) (n' k) R)
    (fun (x : X) ↦ (f x).blockDiag' (m' := m') (n' := n')) L

Tactic:
hf.hasSum.matrix_blockDiag'.summable

Premises used: HasSum.matrix_blockDiag', HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
x : ℝ≥0
⊢ IsOpen (Ico 0 x)

Tactic:
Ico_bot (a := x) ▸ isOpen_Iio

Premises used: Eq.rec, isOpen_Iio, Set.Ico_bot, Eq.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ Continuous Real.toNNReal

Tactic:
(continuous_id.max continuous_const).subtype_mk _

Premises used: continuous_const, NNReal.mk, NNReal, Continuous.subtype_mk, continuous_id, Continuous.max, Real.toNNReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
x : ℝ≥0
rw : 𝓝[toReal '' Set.Ioi x] (↑x : ℝ) = 𝓝[>] (↑x : ℝ)
rw₁ rw₂ : 𝓝[>] (↑x : ℝ) = 𝓝[>] (↑x : ℝ)
⊢ Filter.map toReal (𝓝[>] x) = 𝓝[>] (↑x : ℝ)

Tactic:
rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ioi]

Premises used: NNReal.isEmbedding_coe, NNReal.image_coe_Ioi, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
x : ℝ≥0
rw : 𝓝[toReal '' Set.Ici x] (↑x : ℝ) = 𝓝[≥] (↑x : ℝ)
rw₁ rw₂ : 𝓝[≥] (↑x : ℝ) = 𝓝[≥] (↑x : ℝ)
⊢ Filter.map toReal (𝓝[≥] x) = 𝓝[≥] (↑x : ℝ)

Tactic:
rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ici]

Premises used: NNReal.isEmbedding_coe, NNReal.image_coe_Ici, Topology.IsEmbedding.map_nhdsWithin_eq
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℝ≥0 → ℝ≥0
s : Set ℝ
t : Set ℝ≥0
hf : ContinuousOn f t
h : MapsTo Real.toNNReal s t
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) s

Tactic:
continuous_subtype_val.comp_continuousOn <| hf.comp continuous_real_toNNReal.continuousOn h

Premises used: Continuous.continuousOn, continuous_subtype_val, Continuous.comp_continuousOn, ContinuousOn.comp, continuous_real_toNNReal, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun (a : α) ↦ (↑(m a) : ℝ)) f (𝓝 (↑x : ℝ)) ↔ Tendsto m f (𝓝 x)

Tactic:
tendsto_subtype_rng.symm

Premises used: NNReal, tendsto_subtype_rng, NNReal.toReal, Iff.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
f : Filter α
inst : f.NeBot
m : α → ℝ≥0
x : ℝ
⊢ Tendsto (fun (a : α) ↦ (↑(m a) : ℝ)) f (𝓝 x) ↔
    ∃ (hx : 0 ≤ x), Tendsto m f (𝓝 (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) x hx))

Tactic:
⟨fun h => ⟨ge_of_tendsto' h fun c => (m c).2, tendsto_coe.1 h⟩, fun ⟨_, hm⟩ => tendsto_coe.2 hm⟩

Premises used: Iff.mpr, _private.0.NNReal.tendsto_coe'.match_1, nhds, ge_of_tendsto', Filter.Tendsto, Iff.intro, Exists.intro, Iff.mp, NNReal.tendsto_coe, NNReal.toReal, Subtype.property
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ Filter.map toReal atTop = atTop

Tactic:
map_val_Ici_atTop 0

Premises used: Set.Ici, Set.Mem, Filter.map_val_Ici_atTop, NNReal, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ comap toReal atTop = atTop

Tactic:
(atTop_Ici_eq 0).symm

Premises used: Filter.atTop_Ici_eq, Set.Ici, Set.Mem, NNReal, OfNat.ofNat, Eq.symm, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → ℝ≥0
⊢ Tendsto (β := ℝ) (fun (a : α) ↦ (↑(m a) : ℝ)) f atTop ↔ Tendsto m f atTop

Tactic:
tendsto_Ici_atTop.symm

Premises used: Set.Ici, Set.Mem, NNReal, NNReal.toReal, Filter.tendsto_Ici_atTop, Iff.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
f : Filter α
m : α → ℝ
x : ℝ
h : Tendsto m f (𝓝 x)
⊢ Tendsto (fun (a : α) ↦ (m a).toNNReal) f (𝓝 x.toNNReal)

Tactic:
(continuous_real_toNNReal.tendsto _).comp h

Premises used: NNReal.mk, Continuous.tendsto, continuous_real_toNNReal, Filter.Tendsto.comp, Real.toNNReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
rw : Filter.map Real.toNNReal (Filter.map toReal atTop) = atTop
rw₁ rw₂ : Eq (α := Filter ℝ≥0) atTop atTop
⊢ Filter.map Real.toNNReal atTop = atTop

Tactic:
rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]

Premises used: NNReal.map_coe_atTop, Real.toNNReal_coe, Function.LeftInverse.filter_map
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ Tendsto Real.toNNReal atTop atTop

Tactic:
Real.map_toNNReal_atTop.le

Premises used: Eq.le, Filter.Tendsto, Real.map_toNNReal_atTop
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ comap Real.toNNReal atTop = atTop

Tactic:
le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap

Premises used: Filter.Tendsto.le_comap, tendsto_real_toNNReal_atTop, le_antisymm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
refine : comap Real.toNNReal atTop ≤ atTop
⊢ comap Real.toNNReal atTop = atTop

Tactic:
refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap

Premises used: Filter.Tendsto.le_comap, tendsto_real_toNNReal_atTop, le_antisymm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ comap Real.toNNReal atTop ≤ atTop

Tactic:
(atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.ge_iff, Filter.atTop_basis_Ioi', OfNat.ofNat
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
refine : ∀ (a : ℝ) (ha : 0 < a), Set.Ioi a ∈ comap Real.toNNReal atTop
⊢ comap Real.toNNReal atTop ≤ atTop

Tactic:
refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.ge_iff, Filter.atTop_basis_Ioi', OfNat.ofNat
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
a : ℝ
ha : 0 < a
h : ∀ (x : ℝ) (hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal), x ∈ Set.Ioi a
⊢ Set.Ioi a ∈ comap Real.toNNReal atTop

Tactic:
filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx

Premises used: Filter.Ioi_mem_atTop, Filter.preimage_mem_comap, Real.toNNReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal
⊢ x ∈ Set.Ioi a

Tactic:
(Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx

Premises used: Set.Ioi, Set.Mem, Real.toNNReal_lt_toNNReal_iff_of_nonneg, setOf, LT.lt.le, Iff.mp
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
a : ℝ
ha : 0 < a
x : ℝ
hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal
⊢ x ∈ Set.Ioi a

Tactic:
exact (Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx

Premises used: Real.toNNReal_lt_toNNReal_iff_of_nonneg, LT.lt.le, Iff.mp
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
rw : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l (comap Real.toNNReal atTop)
rw₁ : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto (Real.toNNReal ∘ f) l atTop
rw₂ rw₃ :
  Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop
⊢ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.tendsto_comap_iff, Real.comap_toNNReal_atTop, Function.comp_def
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ Tendsto Real.toNNReal atTop atTop

Tactic:
Real.tendsto_toNNReal_atTop_iff.2 tendsto_id

Premises used: Iff.mpr, Real.tendsto_toNNReal_atTop_iff, Filter.tendsto_id
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
simp : Eq (α := Filter ℝ≥0) (⨅ (l : ℝ≥0), ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l)) (⨅ (a : ℝ≥0), ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a))
⊢ Eq (α := Filter ℝ≥0) (⨅ (l : ℝ≥0), ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l)) (⨅ (a : ℝ≥0), ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a))

Tactic:
simp only [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ Eq (α := Filter ℝ≥0) (⨅ (l : ℝ≥0), ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l)) (⨅ (a : ℝ≥0), ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a))

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
⊢ HasBasis (α := ℝ≥0) (𝓝 0) (fun (a : ℝ≥0) ↦ 0 < a) fun (a : ℝ≥0) ↦ Set.Iio a

Tactic:
nhds_bot_basis

Premises used: nhds_bot_basis
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun (a : α) ↦ (↑(f a) : ℝ)) (↑r : ℝ) L ↔ HasSum f r L

Tactic:
simp only [HasSum, ← coe_sum, tendsto_coe]

Premises used: NNReal.coe_sum, HasSum, NNReal.tendsto_coe, SummationFilter.unconditional
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
inl : L.NeBot → HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
inr : ∀ (hL : L.filter = ⊥), HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L

Tactic:
rcases L.neBot_or_eq_bot with _ | hL

Premises used: SummationFilter.neBot_or_eq_bot
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h : L.NeBot
⊢ 0 ≤ y

Tactic:
hy.nonneg hf₀

Premises used: HasSum.nonneg
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h : L.NeBot
inl : ∀ (y : ℝ≥0) (hy : HasSum f (↑y : ℝ) L), HasSum (fun (x : α) ↦ (f x).toNNReal) (↑y : ℝ).toNNReal L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L

Tactic:
lift y to ℝ≥0 using hy.nonneg hf₀

Premises used: HasSum.nonneg
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
h : L.NeBot
y : ℝ≥0
hy : HasSum f (↑y : ℝ) L
⊢ ∀ (i : α), 0 ≤ f i

Tactic:
hf₀
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
h : L.NeBot
y : ℝ≥0
hy : HasSum f (↑y : ℝ) L
inl :
  ∀ (f : (i : α) → ℝ≥0) (hy : HasSum (fun (i : α) ↦ (↑(f i) : ℝ)) (↑y : ℝ) L),
    HasSum (fun (x : α) ↦ Real.toNNReal ((fun (i : α) ↦ (↑(f i) : ℝ)) x)) (↑y : ℝ).toNNReal L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) (↑y : ℝ).toNNReal L

Tactic:
lift f to α → ℝ≥0 using hf₀
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
h : L.NeBot
y : ℝ≥0
f : (i : α) → ℝ≥0
hy : HasSum (fun (i : α) ↦ (↑(f i) : ℝ)) (↑y : ℝ) L
⊢ HasSum (fun (x : α) ↦ Real.toNNReal ((fun (i : α) ↦ (↑(f i) : ℝ)) x)) (↑y : ℝ).toNNReal L

Tactic:
simpa [hasSum_coe] using hy

Premises used: NNReal.hasSum_coe
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L

Tactic:
simp [HasSum, hL]

Premises used: HasSum, SummationFilter.unconditional
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f L
⊢ HasSum (fun (n : α) ↦ (f n).toNNReal) (Real.toNNReal (∑'[L] (n : α), f n)) L

Tactic:
hf.hasSum.toNNReal hf_nonneg

Premises used: HasSum.toNNReal, Summable.hasSum
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
inl : L.NeBot → (Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L)
inr : ∀ (hL : L.filter = ⊥), Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L

Tactic:
rcases L.neBot_or_eq_bot with _ | hL

Premises used: SummationFilter.neBot_or_eq_bot
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
inl : Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L → Summable f L
inl₁ : Summable f L → Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L → Summable f L

Tactic:
fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩

Premises used: _private.0.NNReal.summable_coe.match_1, Subtype.mk, Exists.intro, Iff.mp, HasSum.nonneg, Summable, NNReal.hasSum_coe, Subtype.property
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L → Summable f L

Tactic:
exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
⊢ Summable f L → Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L

Tactic:
fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩

Premises used: Iff.mpr, Exists.intro, _private.0.NNReal.summable_coe.match_2, Summable, NNReal.hasSum_coe, Subtype.val, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
⊢ Summable f L → Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L

Tactic:
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
hL : L.filter = ⊥
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L

Tactic:
simp [Summable, HasSum, hL]

Premises used: HasSum, Summable, SummationFilter.unconditional
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf : ∀ (n : α), 0 ≤ f n
⊢ Summable (α := { r : ℝ // 0 ≤ r }) (fun (n : α) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (f n) ⋯) L ↔ Summable f L

Tactic:
Iff.symm <| summable_coe (f := fun x => ⟨f x, hf x⟩)

Premises used: NNReal.summable_coe, Iff.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
x : ℝ≥0
⊢ Real.toNNReal ((toRealHom : (a : ℝ≥0) → ℝ) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf₁ : ∀ (n : α), 0 ≤ f n
⊢ NNReal.mk (∑'[L] (n : α), f n) ⋯ = ∑'[L] (n : α), NNReal.mk (f n) ⋯

Tactic:
NNReal.eq <| Eq.symm <| coe_tsum (f := fun x => ⟨f x, hf₁ x⟩)

Premises used: NNReal.eq, NNReal.coe_tsum, Eq.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
a : ℝ≥0
f : α → ℝ≥0
⊢ (↑(∑'[L] (x : α), a * f x) : ℝ) = (↑(a * ∑'[L] (x : α), f x) : ℝ)

Tactic:
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]

Premises used: NNReal.coe_mul, NNReal.tsum_mul_left, NNReal.coe_tsum
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
a : ℝ≥0
⊢ (↑(∑'[L] (x : α), f x * a) : ℝ) = (↑((∑'[L] (x : α), f x) * a) : ℝ)

Tactic:
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]

Premises used: NNReal.tsum_mul_right, NNReal.coe_mul, NNReal.coe_tsum
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
rw :
  ∀ (hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)) {i : β → α} (hi : Function.Injective i),
    Summable (α := ℝ) fun (a : β) ↦ (↑((f ∘ i) a) : ℝ)
⊢ Summable (f ∘ i)

Tactic:
rw [← summable_coe] at hf ⊢

Premises used: NNReal.summable_coe
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
i : β → α
hi : Function.Injective i
⊢ Summable (α := ℝ) fun (a : β) ↦ (↑((f ∘ i) a) : ℝ)

Tactic:
hf.comp_injective hi

Premises used: Summable.comp_injective, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
i : β → α
hi : Function.Injective i
⊢ Summable (α := ℝ) fun (a : β) ↦ (↑((f ∘ i) a) : ℝ)

Tactic:
exact hf.comp_injective hi

Premises used: Summable.comp_injective
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
hf : Summable f
k : ℕ
⊢ Summable (α := ℝ≥0) fun (i : ℕ) ↦ f (i + k)

Tactic:
summable_comp_injective hf <| add_left_injective k

Premises used: NNReal.summable_comp_injective, add_left_injective
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
rw : (Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f (a + k)) : ℝ)) ↔ Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f a) : ℝ)
⊢ (Summable (α := ℝ≥0) fun (i : ℕ) ↦ f (i + k)) ↔ Summable f

Tactic:
rw [← summable_coe, ← summable_coe]

Premises used: NNReal.summable_coe
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f (a + k)) : ℝ)) ↔ Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f a) : ℝ)

Tactic:
@summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k

Premises used: summable_nat_add_iff
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f (a + k)) : ℝ)) ↔ Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f a) : ℝ)

Tactic:
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
rw :
  HasSum (fun (n : ℕ) ↦ (↑(f n) : ℝ)) ((↑a : ℝ) + ∑ i ∈ Finset.range k, (↑(f i) : ℝ)) ↔
    HasSum f (a + ∑ i ∈ Finset.range k, f i)
⊢ HasSum (fun (n : ℕ) ↦ f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]

Premises used: NNReal.hasSum_coe
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HasSum f (a + ∑ i ∈ Finset.range k, f i) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
⊢ HasSum (fun (n : ℕ) ↦ (↑(f n) : ℝ)) ((↑a : ℝ) + ∑ i ∈ Finset.range k, (↑(f i) : ℝ)) ↔
    HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
norm_cast
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
k : ℕ
hf : Summable f
⊢ ∑' (i : ℕ), f i = HAdd.hAdd (α := ℝ≥0) (∑ i ∈ Finset.range k, f i) (∑' (i : ℕ), f (i + k))

Tactic:
(((summable_nat_add_iff k).2 hf).sum_add_tsum_nat_add').symm

Premises used: Iff.mpr, NNReal.summable_nat_add_iff, Summable.sum_add_tsum_nat_add', Eq.symm
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_2
inst : CompleteLattice α
f : ℝ → α
⊢ Eq.{u_2 + 1} (α := α) (⨅ (n : ℝ), ⨅ (_ : 0 < n), f n) (⨅ (n : ℝ≥0), ⨅ (_ : 0 < n), f (↑n : ℝ))

Tactic:
le_antisymm (iInf_mono' fun r => ⟨r, le_rfl⟩) (iInf₂_mono' fun r hr => ⟨⟨r, hr.le⟩, hr, le_rfl⟩)

Premises used: le_rfl, LT.lt.le, Subtype.mk, le_antisymm, iInf₂_mono', Exists.intro, NNReal.toReal, iInf_mono'
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
hf : Summable f
simp : ∀ (hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)), Tendsto (fun (a : α) ↦ (↑(f a) : ℝ)) cofinite (𝓝 (↑0 : ℝ))
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
simp only [← summable_coe, ← tendsto_coe] at hf ⊢

Premises used: NNReal.summable_coe, NNReal.tendsto_coe
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
⊢ Tendsto (fun (a : α) ↦ (↑(f a) : ℝ)) cofinite (𝓝 (↑0 : ℝ))

Tactic:
hf.tendsto_cofinite_zero

Premises used: Summable.tendsto_cofinite_zero, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)
⊢ Tendsto (fun (a : α) ↦ (↑(f a) : ℝ)) cofinite (𝓝 (↑0 : ℝ))

Tactic:
exact hf.tendsto_cofinite_zero

Premises used: Summable.tendsto_cofinite_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
hf : Summable f
rw : Tendsto f cofinite (𝓝 0)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
tendsto_cofinite_zero_of_summable hf

Premises used: NNReal.tendsto_cofinite_zero_of_summable
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)

Tactic:
exact tendsto_cofinite_zero_of_summable hf

Premises used: NNReal.tendsto_cofinite_zero_of_summable
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
simp_rw : Tendsto (β := ℝ) (fun (a : Finset α) ↦ ∑' (a_1 : { x : α // x ∉ a }), (↑(f (↑a_1 : α)) : ℝ)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), f (↑b : α)) atTop (𝓝 0)

Tactic:
simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]

Premises used: NNReal.coe_zero, NNReal.tendsto_coe, NNReal.coe_tsum
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (β := ℝ) (fun (a : Finset α) ↦ ∑' (a_1 : { x : α // x ∉ a }), (↑(f (↑a_1 : α)) : ℝ)) atTop (𝓝 0)

Tactic:
tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)

Premises used: tendsto_tsum_compl_atTop_zero, NNReal.toReal
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (β := ℝ) (fun (a : Finset α) ↦ ∑' (a_1 : { x : α // x ∉ a }), (↑(f (↑a_1 : α)) : ℝ)) atTop (𝓝 0)

Tactic:
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n_1 : ℕ
α : Type u_2
L : SummationFilter α
n : ℕ
hn : n ≠ 0
⊢ Tendsto (β := ℝ≥0) (fun (b : ℝ≥0) ↦ id b ^ n) atBot atBot

Tactic:
simpa [OrderBot.atBot_eq, pos_iff_ne_zero]

Premises used: Filter.OrderBot.atBot_eq, pos_iff_ne_zero
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ
h_bdd : BddAbove (range f)
h_mon : Monotone f
⊢ ∃ (r : ℝ), Tendsto f atTop (𝓝 r)

Tactic:
⟨iSup f, tendsto_atTop_ciSup h_mon h_bdd⟩

Premises used: iSup, tendsto_atTop_ciSup, Exists.intro
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ
h_bdd : BddBelow (range f)
h_ant : Antitone f
⊢ ∃ (r : ℝ), Tendsto f atTop (𝓝 r)

Tactic:
⟨iInf f, tendsto_atTop_ciInf h_ant h_bdd⟩

Premises used: iInf, tendsto_atTop_ciInf, Exists.intro
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
f : ℕ → ℝ≥0
h_ant : Antitone f
⊢ BddBelow (range f)

Tactic:
simp
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
n : ℕ
hn : n ≠ 0
f : ι → ℝ≥0
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
(NNReal.powOrderIso n hn).map_ciSup' _

Premises used: OrderIso.map_ciSup', NNReal.powOrderIso
-- Module: Mathlib.Topology.Instances.NNReal.Lemmas
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
neg : ∀ (hn : ¬n = 0), HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n

Tactic:
by_cases hn : n = 0