awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose contrapose₁ : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
contrapose₂ contrapose₃ contrapose₄ : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
contrapose₅ contrapose₆ : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n), ¬cantorFunction c f = cantorFunction c g
contrapose₇ :
  ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
    let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
    ∀ (hn : ∀ k < n, f k = g k), ¬cantorFunction c f = cantorFunction c g
false :
  ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
    let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
    ∀ (hn : ∀ k < n, f k = g k) (fn : f n = Bool.false), ¬cantorFunction c f = cantorFunction c g
⊢ f = g
have true : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
  let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
  ∀ (hn : ∀ k < n, f k = g k) (fn : f n = true), ¬cantorFunction c f = cantorFunction c g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp h
    let n := Nat.find this
    have hn : ∀ k : ℕ, k < n → f k = g k := by
      intro k hk
      apply of_not_not
      exact Nat.find_min this hk
    cases fn : f n
    · apply _root_.ne_of_lt
      refine increasing_cantorFunction h1 h2 hn fn ?_
      apply Bool.eq_true_of_not_eq_false
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this
    · apply _root_.ne_of_gt
      refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn
      apply Bool.eq_false_of_not_eq_true
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #ℝ = 𝔠
have a : #ℝ ≤ 𝔠
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : #ℝ ≤ 𝔠
⊢ #ℝ = 𝔠
have a₁ : 𝔠 ≤ #ℝ
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #ℝ ≤ 𝔠
have a : #(CauSeq.Completion.Cauchy (α := ℚ) abs) ≤ 𝔠
Tactic: rw [Real.equivCauchy.cardinal_eq]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #(CauSeq.Completion.Cauchy (α := ℚ) abs) ≤ 𝔠
have a : #(CauSeq ℚ abs) ≤ 𝔠
Tactic: apply mk_quotient_le.trans
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #(CauSeq ℚ abs) ≤ 𝔠
have a : #(ℕ → ℚ) = 𝔠
Tactic: apply (mk_subtype_le _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #(ℕ → ℚ) = 𝔠
have a : #ℚ ^ #ℕ = 𝔠
Tactic: rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : #ℚ ^ #ℕ = 𝔠
⊢ #(ℕ → ℚ) = 𝔠
have a₁ : #ℚ ^ ℵ₀ = 𝔠
Tactic: rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : #ℚ ^ #ℕ = 𝔠
a₁ : #ℚ ^ ℵ₀ = 𝔠
⊢ #(ℕ → ℚ) = 𝔠
have a₂ : ℵ₀ ^ ℵ₀ = 𝔠
Tactic: rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : #ℚ ^ #ℕ = 𝔠
a₁ : #ℚ ^ ℵ₀ = 𝔠
a₂ : ℵ₀ ^ ℵ₀ = 𝔠
⊢ #(ℕ → ℚ) = 𝔠
have a₃ : 𝔠 = 𝔠
Tactic: rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ 𝔠 ≤ #ℝ
have h : 𝔠 = #(ℕ → Bool)
Tactic: convert! mk_le_of_injective (cantorFunction_injective _ _)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #(ℕ → Bool)
⊢ 𝔠 ≤ #ℝ
have a : ℝ
Tactic: convert! mk_le_of_injective (cantorFunction_injective _ _)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #(ℕ → Bool)
a : ℝ
⊢ 𝔠 ≤ #ℝ
have a₁ : 0 < 1 / 3
Tactic: convert! mk_le_of_injective (cantorFunction_injective _ _)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #(ℕ → Bool)
a : ℝ
a₁ : 0 < 1 / 3
⊢ 𝔠 ≤ #ℝ
have a₂ : 1 / 3 < 1 / 2
Tactic: convert! mk_le_of_injective (cantorFunction_injective _ _)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ 𝔠 = #(ℕ → Bool)
have h : 𝔠 = #Bool ^ #ℕ
Tactic: rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #Bool ^ #ℕ
⊢ 𝔠 = #(ℕ → Bool)
have h₁ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 #ℕ
Tactic: rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #Bool ^ #ℕ
h₁ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 #ℕ
⊢ 𝔠 = #(ℕ → Bool)
have h₂ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 ℵ₀
Tactic: rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
h : 𝔠 = #Bool ^ #ℕ
h₁ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 #ℕ
h₂ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 ℵ₀
⊢ 𝔠 = #(ℕ → Bool)
have h₃ : 𝔠 = 𝔠
Tactic: rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
⊢ #(↑Set.univ : Type) = 𝔠
have rw : #ℝ = 𝔠
Tactic: rw [mk_univ, mk_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
rw : #ℝ = 𝔠
⊢ #(↑Set.univ : Type) = 𝔠
have rw₁ : 𝔠 = 𝔠
Tactic: rw [mk_univ, mk_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ Uncountable ℝ
have rw : ℵ₀ < 𝔠
Tactic: rw [← aleph0_lt_mk_iff, mk_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
⊢ #(↑(Ioi a) : Type) = 𝔠
have refine : 𝔠 ≤ #(↑(Ioi a) : Type)
Tactic: refine le_antisymm (mk_real ▸ mk_set_le _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
⊢ 𝔠 ≤ #(↑(Ioi a) : Type)
have rw : ¬#(↑(Ioi a) : Type) < 𝔠
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ False
have refine : #(↑Set.univ : Type) < 𝔠
Tactic: refine _root_.ne_of_lt ?_ mk_univ_real
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ
have h₁ : Iio a ∪ {a} = Iic a
Tactic: convert! @Iic_union_Ioi ℝ _ _
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ #(↑Set.univ : Type) < 𝔠
have hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
Tactic: have hu : Iio a ∪ {a} ∪ Ioi a = Set.univ := by
    convert! @Iic_union_Ioi ℝ _ _
    exact Iio_union_right
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #(↑Set.univ : Type) < 𝔠
have rw : #(↑(Iio a ∪ {a} ∪ Ioi a) : Type) < 𝔠
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #(↑(Iio a ∪ {a} ∪ Ioi a) : Type) < 𝔠
have grw : #(↑(Iio a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
Tactic: grw [mk_union_le, mk_union_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
have a₁ : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a ↔ ∀ (a b : ℝ), (fun (x : ℝ) ↦ a - x) '' Ioi b = Iio (a - b)
Tactic: convert! @image_const_sub_Ioi ℝ _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #(↑(Iio a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
have h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
Tactic: have h2 : (fun x => a + a - x) '' Ioi a = Iio a := by
    convert! @image_const_sub_Ioi ℝ _ _ _
    simp
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ #(↑(Iio a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
have rw : #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
Tactic: rw [← h2]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
have refine : #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) < 𝔠
Tactic: refine add_lt_of_lt (cantor _).le ?_ h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) < 𝔠
have refine : #(↑{a} : Type) < 𝔠
Tactic: refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ #(↑{a} : Type) < 𝔠
have rw : 1 < 𝔠
Tactic: rw [mk_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a : ℝ
⊢ #(↑(Iio a) : Type) = 𝔠
have refine : 𝔠 ≤ #(↑(Iio a) : Type)
Tactic: refine le_antisymm (mk_real ▸ mk_set_le _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a : ℝ
⊢ 𝔠 ≤ #(↑(Iio a) : Type)
have h2 : (fun (x : ℝ) ↦ a + a - x) '' Iio a = Ioi a
Tactic: have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by
    simp only [image_const_sub_Iio, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h : a < b
⊢ #(↑(Ioo a b) : Type) = 𝔠
have refine : 𝔠 ≤ #(↑(Ioo a b) : Type)
Tactic: refine le_antisymm (mk_real ▸ mk_set_le _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a b : ℝ
h : a < b
⊢ 𝔠 ≤ #(↑(Ioo a b) : Type)
have h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
Tactic: have h1 : #((fun x => x - a) '' Ioo a b) ≤ #(Ioo a b) := mk_image_le
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
⊢ 𝔠 ≤ #(↑(Ioo a b) : Type)
have refine : 𝔠 ≤ #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type)
Tactic: refine le_trans ?_ h1
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
⊢ 𝔠 ≤ #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type)
have rw : 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)
Tactic: rw [image_sub_const_Ioo, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
⊢ 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)
have h₁ : 0 < b - a
Tactic: replace h := sub_pos_of_lt h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
⊢ 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)
have h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
Tactic: have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
⊢ 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)
have refine : 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)
Tactic: refine le_trans ?_ h2
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
⊢ 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)
have rw : 𝔠 ≤ #(↑(Ioo 0 (b - a))⁻¹ : Type)
Tactic: rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
rw : 𝔠 ≤ #(↑(Ioo 0 (b - a))⁻¹ : Type)
⊢ 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)
have rw₁ : 𝔠 ≤ #(↑(Ioi (b - a)⁻¹) : Type)
Tactic: rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
rw : 𝔠 ≤ #(↑(Ioo 0 (b - a))⁻¹ : Type)
rw₁ : 𝔠 ≤ #(↑(Ioi (b - a)⁻¹) : Type)
⊢ 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)
have rw₂ : 𝔠 ≤ 𝔠
Tactic: rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
⊢ (Ioo x y).Countable ↔ y ≤ x
have refine : ∀ (h : (Ioo x y).Countable), y ≤ x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : (Ioo x y).Countable
⊢ y ≤ x
have contrapose! : ∀ (h : x < y), ¬(Ioo x y).Countable
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : x < y
⊢ ¬(Ioo x y).Countable
have rw : ℵ₀ < 𝔠
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
⊢ (Ico x y).Countable ↔ y ≤ x
have refine : ∀ (h : (Ico x y).Countable), y ≤ x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : (Ico x y).Countable
⊢ y ≤ x
have contrapose! : ∀ (h : x < y), ¬(Ico x y).Countable
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : x < y
⊢ ¬(Ico x y).Countable
have rw : ℵ₀ < 𝔠
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real h, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
⊢ (Ioc x y).Countable ↔ y ≤ x
have refine : ∀ (h : (Ioc x y).Countable), y ≤ x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : (Ioc x y).Countable
⊢ y ≤ x
have contrapose! : ∀ (h : x < y), ¬(Ioc x y).Countable
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : x < y
⊢ ¬(Ioc x y).Countable
have rw : ℵ₀ < 𝔠
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : y ≤ x
⊢ (Icc x y).Countable
have inl : ∀ (heq : y = x), (Icc x y).Countable
Tactic: rcases le_iff_eq_or_lt.mp h with heq | hlt
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : y ≤ x
inl : ∀ (heq : y = x), (Icc x y).Countable
⊢ (Icc x y).Countable
have inr : ∀ (hlt : y < x), (Icc x y).Countable
Tactic: rcases le_iff_eq_or_lt.mp h with heq | hlt
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
⊢ (Icc x y).Countable ↔ y ≤ x
have refine : ∀ (h : (Icc x y).Countable), y ≤ x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by
    rcases le_iff_eq_or_lt.mp h with heq | hlt
    · simp [heq]
    · simp [hlt]⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : (Icc x y).Countable
⊢ y ≤ x
have contrapose! : ∀ (h : x < y), ¬(Icc x y).Countable
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
x y : ℝ
h : x < y
⊢ ¬(Icc x y).Countable
have rw : ℵ₀ < 𝔠
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
⊢ (↑r : ℝ*) < ω
have apply : ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
Tactic: apply ofSeq_lt_ofSeq.2 <| Filter.Eventually.filter_mono Nat.hyperfilter_le_atTop _
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
⊢ ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
have obtain : ∀ (n : ℕ) (hn : r < (↑n : ℝ)), ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
Tactic: obtain ⟨n, hn⟩ := exists_nat_gt r
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
n : ℕ
hn : r < (↑n : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
have rw : ∃ (a : ℕ), ∀ b ≥ a, r < (↑b : ℝ)
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
⊢ stdPart ω = 0
have rw : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk ω) 0
Tactic: rw [stdPart_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
hxr : Germ.Tendsto x (𝓝 r)
⊢ (Germ.map f x).Tendsto (𝓝 (f r))
have rcases : ∀ (g : ℕ → ℝ) (hxr : Germ.Tendsto (ofSeq g) (𝓝 r)), (Germ.map f (ofSeq g)).Tendsto (𝓝 (f r))
Tactic: rcases ofSeq_surjective x with ⟨g, rfl⟩
Cleared hypotheses: x, hxr
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
r s : ℝ
f : ℝ → ℝ → ℝ
hxr : Germ.Tendsto x (𝓝 r)
hys : Germ.Tendsto y (𝓝 s)
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ (Germ.map₂ f x y).Tendsto (𝓝 (f r s))
have rcases : ∀ (x : ℕ → ℝ) (hxr : Germ.Tendsto (ofSeq x) (𝓝 r)), (Germ.map₂ f (ofSeq x) y).Tendsto (𝓝 (f r s))
Tactic: rcases ofSeq_surjective x with ⟨x, rfl⟩
Cleared hypotheses: x, hxr
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
y : ℝ*
r s : ℝ
f : ℝ → ℝ → ℝ
hys : Germ.Tendsto y (𝓝 s)
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Germ.Tendsto (ofSeq x) (𝓝 r)
⊢ (Germ.map₂ f (ofSeq x) y).Tendsto (𝓝 (f r s))
have rcases : ∀ (y : ℕ → ℝ) (hys : Germ.Tendsto (ofSeq y) (𝓝 s)), (Germ.map₂ f (ofSeq x) (ofSeq y)).Tendsto (𝓝 (f r s))
Tactic: rcases ofSeq_surjective y with ⟨y, rfl⟩
Cleared hypotheses: y, hys
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
⊢ Germ.Tendsto x (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
have rcases : ∀ (f : ℕ → ℝ), Germ.Tendsto (ofSeq f) (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
⊢ Germ.Tendsto (ofSeq f) (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have rw : (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → ∀ᶠ (x : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f x ∈ Set.Ioo i.1 i.2) ↔
  (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
Tactic: rw [tendsto_ofSeq, (nhds_basis_Ioo _).tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → ∀ᶠ (x : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f x ∈ Set.Ioo i.1 i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have simp_rw : (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
  (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
Tactic: simp_rw [Set.mem_Ioo, eventually_and, ← ofSeq_lt_ofSeq]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have refine_1 : ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
  (s : ℝ) (hs : s < r), (↑s : ℝ*) ≤ ofSeq f
Tactic: refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
refine_1 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s < r), (↑s : ℝ*) ≤ ofSeq f
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have refine_2 : ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
  (s : ℝ) (hs : s > r), ofSeq f ≤ (↑s : ℝ*)
Tactic: refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
refine_1 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s < r), (↑s : ℝ*) ≤ ofSeq f
refine_2 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s > r), ofSeq f ≤ (↑s : ℝ*)
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have refine_3 : ∀ (H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)) (x : ℝ × ℝ) (s t : ℝ),
  (s, t).1 < r ∧ r < (s, t).2 → ∀ (hs : (s, t).1 < r) (ht : r < (s, t).2), (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
Tactic: refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
refine_1 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s < r), (↑s : ℝ*) ≤ ofSeq f
refine_2 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s > r), ofSeq f ≤ (↑s : ℝ*)
refine_3 :
  ∀ (H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)) (x : ℝ × ℝ) (s t : ℝ),
    (s, t).1 < r ∧ r < (s, t).2 → ∀ (hs : (s, t).1 < r) (ht : r < (s, t).2), (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
have refine_4 : ∀ (H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)) (x : ℝ × ℝ) (s t : ℝ),
  (s, t).1 < r ∧ r < (s, t).2 → ∀ (hs : (s, t).1 < r) (ht : r < (s, t).2), ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2
Tactic: refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s < r
⊢ (↑s : ℝ*) ≤ ofSeq f
have refine_1 : ∀ (t : ℝ) (ht : r < t), (↑s : ℝ*) ≤ ofSeq f
Tactic: obtain ⟨t, ht⟩ := exists_gt r
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s > r
⊢ ofSeq f ≤ (↑s : ℝ*)
have refine_2 : ∀ (t : ℝ) (ht : t < r), ofSeq f ≤ (↑s : ℝ*)
Tactic: obtain ⟨t, ht⟩ := exists_lt r
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
have refine_3 : ∀ (u : ℝ) (hu : (s, t).1 < u) (hu' : u < r), (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
Tactic: obtain ⟨u, hu, hu'⟩ := exists_between hs
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
⊢ ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2
have refine_4 : ∀ (u : ℝ) (hu : r < u) (hu' : u < (s, t).2), ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2
Tactic: obtain ⟨u, hu, hu'⟩ := exists_between ht