awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
ht : ∀ (b : ℝ≥0∞), b ≠ 0 → Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞)
top :
  ∀ (ha : Ne (α := ℝ≥0∞) ∞ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ Ne (α := ℝ≥0∞) ∞ ∞),
    Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (∞, b)) (𝓝 (∞ * b))
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))
have coe : ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) ≠ 0 ∨ b ≠ ∞) (hb : b ≠ 0 ∨ (↑a : ℝ≥0∞) ≠ ∞),
  Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 * p.2) (𝓝 ((↑a : ℝ≥0∞), b)) (𝓝 ((↑a : ℝ≥0∞) * b))
Tactic: induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ insert a_1 s, f c b) x (𝓝 (∏ c ∈ insert a_1 s, a c))
have insert : Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))
Tactic: simp only [Finset.prod_insert has]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))
have insert : a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
Tactic: apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞
insert : a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
⊢ Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))
have insert₁ : Tendsto (β := ℝ≥0∞) (fun (a : α) ↦ ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a c))
Tactic: apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ Insert.insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ Insert.insert a_1 s, a i ≠ ∞
insert : a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
insert₁ : Tendsto (β := ℝ≥0∞) (fun (a : α) ↦ ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a c))
⊢ Tendsto (fun (b : α) ↦ f a_1 b * ∏ c ∈ s, f c b) x (𝓝 (a a_1 * ∏ c ∈ s, a c))
have insert₂ : Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) 0 ∨ a a_1 ≠ ∞
Tactic: apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a_1 : ι
s : Finset ι
has : a_1 ∉ s
IH :
  ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a_1 s, a i ≠ ∞
⊢ a a_1 ≠ 0 ∨ Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
have insert : Ne (α := ℝ≥0∞) (∏ c ∈ s, a c) ∞
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
  (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
Tactic: induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
    (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
have insert : ∀ (a_1 : ι) (s : Finset ι) (has : a_1 ∉ s)
  (IH :
    ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
      Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)))
  (h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ insert a_1 s, a i ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ insert a_1 s, f c b) x (𝓝 (∏ c ∈ insert a_1 s, a c))
Tactic: induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
  (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
s : Finset ι
h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ s, a i ≠ ∞
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Tendsto (f i) x (𝓝 (a i)))
    (h' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → a i ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
have insert : ∀ (a_1 : ι) (s : Finset ι) (has : a_1 ∉ s)
  (IH :
    ∀ (h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ s, a i ≠ ∞),
      Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)))
  (h : ∀ i ∈ insert a_1 s, Tendsto (f i) x (𝓝 (a i))) (h' : ∀ i ∈ insert a_1 s, a i ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (b : α) ↦ ∏ c ∈ insert a_1 s, f c b) x (𝓝 (∏ c ∈ insert a_1 s, a c))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp [tendsto_const_nhds]
  | insert _ _ has IH =>
    simp only [Finset.prod_insert has]
    apply Tendsto.mul (h _ (Finset.mem_insert_self _ _))
    · right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)
    · exact IH (fun i hi => h _ (Finset.mem_insert_of_mem hi)) fun i hi =>
        h' _ (Finset.mem_insert_of_mem hi)
    · exact Or.inr (h' _ (Finset.mem_insert_self _ _))
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ (n + 1)
have succ : ∀ (x : ℝ≥0∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x
Tactic: simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x
have succ : x ^ n ≠ 0 ∨ x ≠ ∞
Tactic: refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
succ : x ^ n ≠ 0 ∨ x ≠ ∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ n * a) x
have succ₁ : x ≠ 0 ∨ x ^ n ≠ ∞
Tactic: refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞
have pos : ∀ (H : x = 0), x ^ n ≠ 0 ∨ x ≠ ∞
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
pos : ∀ (H : x = 0), x ^ n ≠ 0 ∨ x ≠ ∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞
have neg : ∀ (H : ¬x = 0), x ^ n ≠ 0 ∨ x ≠ ∞
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞
have pos : ∀ (H : x = 0), x ≠ 0 ∨ x ^ n ≠ ∞
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
x : ℝ≥0∞
pos : ∀ (H : x = 0), x ≠ 0 ∨ x ^ n ≠ ∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞
have neg : ∀ (H : ¬x = 0), x ≠ 0 ∨ x ^ n ≠ ∞
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
have zero : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 0
Tactic: induction n with
  | zero => simp [continuous_const]
  | succ n IH =>
    simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
n : ℕ
zero : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 0
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n
have succ : ∀ (n : ℕ) (IH : Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n), Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ (n + 1)
Tactic: induction n with
  | zero => simp [continuous_const]
  | succ n IH =>
    simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
    intro x
    refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
    · simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
    · exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
    · simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]
    · simp only [H, true_or, Ne, not_false_iff]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
x y : ℝ≥0∞
hp : Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, y)
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, y)
have hp₁ : ¬(x = ∞ ∧ y = ∞)
Tactic: simp only [Ne, Set.mem_setOf_eq, Prod.mk_inj] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ a - x
have change : Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) (uncurry Sub.sub ∘ fun (x : ℝ≥0∞) ↦ (a, x))
Tactic: change Continuous (Function.uncurry Sub.sub ∘ (a, ·))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
a_ne_top : a ≠ ∞
⊢ Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) (uncurry Sub.sub ∘ fun (x : ℝ≥0∞) ↦ (a, x))
have refine : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (a, x)
Tactic: refine continuousOn_sub.comp_continuous (.prodMk_right a) fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ a - x) {x : ℝ≥0∞ | x ≠ ∞}
have rw : ContinuousOn (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (a, x)) {x : ℝ≥0∞ | x ≠ ∞}
Tactic: rw [show (fun x => a - x) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨a, x⟩ by rfl]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
⊢ ContinuousOn (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (a, x))
    {x : ℝ≥0∞ | x ≠ ∞}
have apply : MapsTo (β := ℝ≥0∞ × ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ (a, x)) {x : ℝ≥0∞ | x ≠ ∞} {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)}
Tactic: apply continuousOn_sub.comp (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
have pos : ∀ (a_infty : a = ∞), Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
Tactic: by_cases a_infty : a = ∞
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
pos : ∀ (a_infty : a = ∞), Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
have neg : ∀ (a_infty : ¬a = ∞), Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
Tactic: by_cases a_infty : a = ∞
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x - a
have neg : Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (x, a))
Tactic: rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous (X := ℝ≥0∞) (Y := ℝ≥0∞) ((fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) ∘ fun (x : ℝ≥0∞) ↦ (x, a))
have neg : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set (ℝ≥0∞ × ℝ≥0∞)) {p : ℝ≥0∞ × ℝ≥0∞ | p ≠ (∞, ∞)} (x, a)
Tactic: apply continuousOn_sub.comp_continuous (by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
⊢ x ≤ y
have this : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
Tactic: have : Tendsto (· * x) (𝓝[<] 1) (𝓝 (1 * x)) :=
    (ENNReal.continuousAt_mul_const (Or.inr one_ne_zero)).mono_left inf_le_left
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
⊢ x ≤ y
have this₁ : Tendsto (fun (x_1 : ℝ≥0∞) ↦ x_1 * x) (𝓝[<] 1) (𝓝 x)
Tactic: rw [one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun (a : α) ↦ ma a / mb a) f (𝓝 (a / b))
have apply : a ≠ 0 ∨ b⁻¹ ≠ ∞
Tactic: apply Tendsto.mul hma _ (tendsto_inv_iff.2 hmb) _
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : Filter α
ma mb : α → ℝ≥0∞
a b : ℝ≥0∞
hma : Tendsto ma f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
hmb : Tendsto mb f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
apply : a ≠ 0 ∨ b⁻¹ ≠ ∞
⊢ Tendsto (fun (a : α) ↦ ma a / mb a) f (𝓝 (a / b))
have apply₁ : b⁻¹ ≠ 0 ∨ a ≠ ∞
Tactic: apply Tendsto.mul hma _ (tendsto_inv_iff.2 hmb) _
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ ∞ ∨ a ≠ ∞
⊢ Tendsto (fun (b : α) ↦ a / m b) f (𝓝 (a / b))
have apply : b⁻¹ ≠ 0 ∨ a ≠ ∞
Tactic: apply Tendsto.const_mul (tendsto_inv_iff.2 hm)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun (x : α) ↦ m x / b) f (𝓝 (a / b))
have apply : a ≠ 0 ∨ b⁻¹ ≠ ∞
Tactic: apply Tendsto.mul_const hm
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
⊢ ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s
have obtain : ∀ (s : Set ℝ≥0∞) (s_count : s.Countable) (s_dense : Dense s)
  (hs : (∀ (x : ℝ≥0∞), IsBot x → x ∉ s) ∧ ∀ (x : ℝ≥0∞), IsTop x → x ∉ s),
  ∃ (s : Set ℝ≥0∞), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s
Tactic: obtain ⟨s, s_count, s_dense, hs⟩ :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s :=
    exists_countable_dense_no_bot_top ℝ≥0∞
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
⊢ ∃ (R : ℝ), ∃ᶠ (n : ι) in l, x n < R
have by_contra! : ∀ (h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
⊢ False
have refine : ∀ (r : ℝ≥0), ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
Tactic: refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
have simp : ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
Tactic: simp only [eventually_map, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
have h₁ : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ (↑r : ℝ) ≤ x x_3) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
    a
Tactic: filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ (↑r : ℝ) ≤ x x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
      a
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
have h₂ : ∀ (a : ι), (↑r : ℝ) ≤ x a → r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
Tactic: filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
⊢ ∃ (R : ℝ), ∃ᶠ (n : ι) in l, R < x n
have by_contra! : ∀ (h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
⊢ False
have refine : ∀ (r : ℝ≥0), ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
Tactic: refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l, (↑r : ℝ≥0∞) ≤ n
have simp : ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
Tactic: simp only [eventually_map, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
have h₁ : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ x x_3 ≤ -(↑r : ℝ)) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
    a
Tactic: filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : Ne (α := ℝ≥0∞) (liminf (fun (n : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x n)) : ℝ≥0∞)) l) ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, x x_1 ≤ R
r : ℝ≥0
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ x x_3 ≤ -(↑r : ℝ)) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)) x_2} x_1}
      a
⊢ ∀ᶠ (a : ι) in l, r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
have h₂ : ∀ (a : ι), x a ≤ -(↑r : ℝ) → r ≤ (Real.nnabs : (a : ℝ) → ℝ≥0) (x a)
Tactic: filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)