awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
zero :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < 0, f k = g k) (fn : f 0 = false) (gn : g 0 = true),
    cantorFunction c f < cantorFunction c g
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
        cantorFunction c f < cantorFunction c g)
    {f g : ℕ → Bool} (hn : ∀ k < n + 1, f k = g k) (fn : f (n + 1) = false) (gn : g (n + 1) = true),
    cantorFunction c f < cantorFunction c g
⊢ cantorFunction c f < cantorFunction c g

Tactic:
induction n generalizing f g with
  | zero =>
    let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
    have hf_max : ∀ n, f n → f_max n := by
      intro n hn
      cases n
      · rw [fn] at hn
        contradiction
      simp [f_max]
    let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
    have hg_min : ∀ n, g_min n → g n := by
      intro n hn
      cases n
      · rw [gn]
      simp at hn
    apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
    refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)
    have : c / (1 - c) < 1 := by
      rw [div_lt_one, lt_sub_iff_add_lt]
      · convert! _root_.add_lt_add h2 h2
        norm_num
      rwa [sub_pos]
    convert! this
    · rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]
      apply zero_add
    · refine (tsum_eq_single 0 ?_).trans ?_
      · intro n hn
        cases n
        · contradiction
        simp [g_min]
      · exact cantorFunctionAux_zero _
  | succ n ih =>
  rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]
  rw [hn 0 <| zero_lt_succ n]
  gcongr
  exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn

Premises used: Nat.zero_lt_succ, le_of_lt, tsum_geometric_of_lt_one, LT.lt.le, zero_add, div_eq_mul_inv, Cardinal.cantorFunction_succ, tsum_eq_single, Nat.zero, Cardinal.cantorFunctionAux_zero, OfNat.ofNat, Nat.succ, Eq.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
⊢ f = g

Tactic:
contrapose hfg with h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ∃ (n : ℕ), f n ≠ g n

Tactic:
have : ∃ n, f n ≠ g n := Function.ne_iff.mp h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
k : ℕ
hk : k < n
a : ¬¬f k = g k
⊢ f k = g k

Tactic:
apply of_not_not

Premises used: of_not_not
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
k : ℕ
hk : k < n
⊢ ¬¬f k = g k

Tactic:
Nat.find_min this hk

Premises used: Nat.find_min
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
k : ℕ
hk : k < n
⊢ ¬¬f k = g k

Tactic:
exact Nat.find_min this hk

Premises used: Nat.find_min
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
⊢ ∀ k < n, f k = g k

Tactic:
have hn : ∀ k : ℕ, k < n → f k = g k := by
      intro k hk
      apply of_not_not
      exact Nat.find_min this hk
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
false : ∀ (fn : f n = Bool.false), ¬cantorFunction c f = cantorFunction c g
true : ∀ (fn : f n = Bool.true), ¬cantorFunction c f = cantorFunction c g
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
cases fn : f n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.false
false : cantorFunction c f < cantorFunction c g
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
apply _root_.ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ cantorFunction c f < cantorFunction c g

Tactic:
increasing_cantorFunction h1 h2 hn fn ?_

Premises used: Cardinal.increasing_cantorFunction
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.false
false : g n = true
⊢ cantorFunction c f < cantorFunction c g

Tactic:
refine increasing_cantorFunction h1 h2 hn fn ?_

Premises used: Cardinal.increasing_cantorFunction
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.false
false : ¬g n = Bool.false
⊢ g n = true

Tactic:
apply Bool.eq_true_of_not_eq_false

Premises used: Bool.eq_true_of_not_eq_false
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.false
false : ¬g n = f n
⊢ ¬g n = Bool.false

Tactic:
rw [← fn]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.false
false : f n ≠ g n
⊢ ¬g n = f n

Tactic:
apply Ne.symm

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ f n ≠ g n

Tactic:
Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ f n ≠ g n

Tactic:
exact Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.true
true : cantorFunction c g < cantorFunction c f
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
apply _root_.ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ cantorFunction c g < cantorFunction c f

Tactic:
increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn

Premises used: Cardinal.increasing_cantorFunction, Eq.symm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.true
true : g n = false
⊢ cantorFunction c g < cantorFunction c f

Tactic:
refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn

Premises used: Cardinal.increasing_cantorFunction, Eq.symm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.true
true : ¬g n = Bool.true
⊢ g n = false

Tactic:
apply Bool.eq_false_of_not_eq_true

Premises used: Bool.eq_false_of_not_eq_true
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.true
true : ¬g n = f n
⊢ ¬g n = Bool.true

Tactic:
rw [← fn]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = Bool.true
true : f n ≠ g n
⊢ ¬g n = f n

Tactic:
apply Ne.symm

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ f n ≠ g n

Tactic:
Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ f n ≠ g n

Tactic:
exact Nat.find_spec this

Premises used: Nat.find_spec
-- Module: Mathlib.Analysis.Real.Cardinality
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
true 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 = Bool.true), ¬cantorFunction c f = cantorFunction c g
⊢ f = 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

Premises used: ne_of_gt, Ne.symm, Bool.eq_false_of_not_eq_true, Bool.eq_true_of_not_eq_false, ne_of_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : #ℝ ≤ 𝔠
a₁ : 𝔠 ≤ #ℝ
⊢ #ℝ = 𝔠

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : #(CauSeq.Completion.Cauchy (α := ℚ) abs) ≤ 𝔠
⊢ #ℝ ≤ 𝔠

Tactic:
rw [Real.equivCauchy.cardinal_eq]

Premises used: Equiv.cardinal_eq, Real.equivCauchy
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : #(CauSeq ℚ abs) ≤ 𝔠
⊢ #(CauSeq.Completion.Cauchy (α := ℚ) abs) ≤ 𝔠

Tactic:
apply mk_quotient_le.trans

Premises used: Cardinal.mk_quotient_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : #(ℕ → ℚ) = 𝔠
⊢ #(CauSeq ℚ abs) ≤ 𝔠

Tactic:
apply (mk_subtype_le _).trans_eq

Premises used: LE.le.trans_eq, Cardinal.mk_subtype_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : #ℚ ^ #ℕ = 𝔠
a₁ : #ℚ ^ ℵ₀ = 𝔠
a₂ : ℵ₀ ^ ℵ₀ = 𝔠
a₃ a₄ : 𝔠 = 𝔠
⊢ #(ℕ → ℚ) = 𝔠

Tactic:
rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]

Premises used: Cardinal.mkRat, Cardinal.aleph0_power_aleph0, Cardinal.mk_nat, Cardinal.power_def
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
⊢ #(ℕ → Bool) ≤ #ℝ

Tactic:
mk_le_of_injective (cantorFunction_injective _ _)

Premises used: Cardinal.cantorFunction_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
h : 𝔠 = #(ℕ → Bool)
a : ℝ
a₁ : 0 < 1 / 3
a₂ : 1 / 3 < 1 / 2
⊢ 𝔠 ≤ #ℝ

Tactic:
convert! mk_le_of_injective (cantorFunction_injective _ _)

Premises used: Cardinal.cantorFunction_injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
h : 𝔠 = #Bool ^ #ℕ
h₁ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 #ℕ
h₂ : 𝔠 = HPow.hPow (α := Cardinal.{0}) 2 ℵ₀
h₃ h₄ : 𝔠 = 𝔠
⊢ 𝔠 = #(ℕ → Bool)

Tactic:
rw [← power_def, mk_bool, mk_nat, two_power_aleph0]

Premises used: Cardinal.mk_nat, Cardinal.mk_bool, Cardinal.two_power_aleph0, Cardinal.power_def
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
⊢ ℝ

Tactic:
exact 1 / 3
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
⊢ 0 < 1 / 3

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
⊢ 1 / 3 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
rw : #ℝ = 𝔠
rw₁ rw₂ : 𝔠 = 𝔠
⊢ #(↑Set.univ : Type) = 𝔠

Tactic:
rw [mk_univ, mk_real]

Premises used: Cardinal.mk_univ, Cardinal.mk_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
n : ℕ
rw : ℵ₀ < 𝔠
⊢ Uncountable ℝ

Tactic:
rw [← aleph0_lt_mk_iff, mk_real]

Premises used: Cardinal.mk_real, Cardinal.aleph0_lt_mk_iff
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠

Tactic:
aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠

Tactic:
exact aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
⊢ ¬Set.Countable (α := ℝ) Set.univ

Tactic:
not_countable_univ

Premises used: Set.not_countable_univ
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ #(↑(Ioi a) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
refine : 𝔠 ≤ #(↑(Ioi a) : Type)
⊢ #(↑(Ioi a) : Type) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
rw : ¬#(↑(Ioi a) : Type) < 𝔠
⊢ 𝔠 ≤ #(↑(Ioi a) : Type)

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ False

Tactic:
_root_.ne_of_lt ?_ mk_univ_real

Premises used: Cardinal.mk_univ_real, ne_of_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
refine : #(↑Set.univ : Type) < 𝔠
⊢ False

Tactic:
refine _root_.ne_of_lt ?_ mk_univ_real

Premises used: Cardinal.mk_univ_real, ne_of_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ Iic a ∪ Ioi a = Set.univ

Tactic:
@Iic_union_Ioi ℝ _ _

Premises used: Set.Iic_union_Ioi
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
h₁ : Iio a ∪ {a} = Iic a
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ

Tactic:
convert! @Iic_union_Ioi ℝ _ _

Premises used: Set.Iic_union_Ioi
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ Iio a ∪ {a} = Iic a

Tactic:
Iio_union_right

Premises used: Set.Iio_union_right
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ Iio a ∪ {a} = Iic a

Tactic:
exact Iio_union_right

Premises used: Set.Iio_union_right
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
⊢ 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
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
rw : #(↑(Iio a ∪ {a} ∪ Ioi a) : Type) < 𝔠
⊢ #(↑Set.univ : Type) < 𝔠

Tactic:
rw [← hu]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
grw : #(↑(Iio a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
⊢ #(↑(Iio a ∪ {a} ∪ Ioi a) : Type) < 𝔠

Tactic:
grw [mk_union_le, mk_union_le]

Premises used: Cardinal.mk_union_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ ∀ (a b : ℝ), (fun (x : ℝ) ↦ a - x) '' Ioi b = Iio (a - b)

Tactic:
@image_const_sub_Ioi ℝ _ _ _

Premises used: Set.image_const_sub_Ioi
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
a₁ : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a ↔ ∀ (a b : ℝ), (fun (x : ℝ) ↦ a - x) '' Ioi b = Iio (a - b)
⊢ (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a

Tactic:
convert! @image_const_sub_Ioi ℝ _ _ _

Premises used: Set.image_const_sub_Ioi
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a ↔ ∀ (a b : ℝ), (fun (x : ℝ) ↦ a - x) '' Ioi b = Iio (a - b)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (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
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
rw : #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠
⊢ #(↑(Iio a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠

Tactic:
rw [← h2]
-- Module: Mathlib.Analysis.Real.Cardinality
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) < 𝔠

Tactic:
add_lt_of_lt (cantor _).le ?_ h

Premises used: Cardinal.add_lt_of_lt, LT.lt.le, Cardinal.cantor
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
refine : #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) < 𝔠
⊢ #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) + #(↑(Ioi a) : Type) < 𝔠

Tactic:
refine add_lt_of_lt (cantor _).le ?_ h

Premises used: Cardinal.add_lt_of_lt, LT.lt.le, Cardinal.cantor
-- Module: Mathlib.Analysis.Real.Cardinality
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) < 𝔠

Tactic:
add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_

Premises used: Cardinal.mk_image_le, Cardinal.add_lt_of_lt, LT.lt.le, Cardinal.cantor, LE.le.trans_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
refine : #(↑{a} : Type) < 𝔠
⊢ #(↑((fun (x : ℝ) ↦ a + a - x) '' Ioi a) : Type) + #(↑{a} : Type) < 𝔠

Tactic:
refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_

Premises used: Cardinal.mk_image_le, Cardinal.add_lt_of_lt, LT.lt.le, Cardinal.cantor, LE.le.trans_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
rw : 1 < 𝔠
⊢ #(↑{a} : Type) < 𝔠

Tactic:
rw [mk_singleton]

Premises used: Cardinal.mk_singleton
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠

Tactic:
one_lt_aleph0.trans (cantor _)

Premises used: Cardinal.one_lt_aleph0, Cardinal.cantor, LT.lt.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h : #(↑(Ioi a) : Type) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠

Tactic:
exact one_lt_aleph0.trans (cantor _)

Premises used: Cardinal.one_lt_aleph0, Cardinal.cantor, LT.lt.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ #(↑(Ici a) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioi_real a ▸ mk_le_mk_of_subset Ioi_subset_Ici_self)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ #(↑(Iio a) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
refine : 𝔠 ≤ #(↑(Iio a) : Type)
⊢ #(↑(Iio a) : Type) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ (fun (x : ℝ) ↦ a + a - x) '' Iio a = Ioi a

Tactic:
simp only [image_const_sub_Iio, add_sub_cancel_right]

Premises used: Set.image_const_sub_Iio, add_sub_cancel_right
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ (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]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #(↑(Iio a) : Type)

Tactic:
mk_Ioi_real a ▸ h2 ▸ mk_image_le

Premises used: Eq.rec, Cardinal.mk_image_le, Cardinal.mk_Ioi_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
h2 : (fun (x : ℝ) ↦ a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #(↑(Iio a) : Type)

Tactic:
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a : ℝ
⊢ #(↑(Iic a) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) (mk_Iio_real a ▸ mk_le_mk_of_subset Iio_subset_Iic_self)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
⊢ #(↑(Ioo a b) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
refine : 𝔠 ≤ #(↑(Ioo a b) : Type)
⊢ #(↑(Ioo a b) : Type) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
⊢ #(↑((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
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
⊢ 𝔠 ≤ #(↑(Ioo a b) : Type)

Tactic:
le_trans ?_ h1

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
refine : 𝔠 ≤ #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type)
⊢ 𝔠 ≤ #(↑(Ioo a b) : Type)

Tactic:
refine le_trans ?_ h1

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
rw : 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)
⊢ 𝔠 ≤ #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type)

Tactic:
rw [image_sub_const_Ioo, sub_self]

Premises used: sub_self, Set.image_sub_const_Ioo
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
⊢ 0 < b - a

Tactic:
replace h := sub_pos_of_lt h