awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : 1 < #α ↔ ∃ (x : α) (y : α), x ≠ y
rw₁ : Nontrivial α ↔ ∃ (x : α) (y : α), x ≠ y
⊢ 2 ≤ #α ↔ ∃ (x : α) (y : α), x ≠ y
have rw₂ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), x ≠ y
Tactic: rw [two_le_iff_one_lt, one_lt_iff_nontrivial, nontrivial_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ (y : α), y ≠ x
have rw : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (y : α), y ≠ x
Tactic: rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
rw : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (y : α), y ≠ x
⊢ 2 ≤ #α ↔ ∃ (y : α), y ≠ x
have rw₁ : Nontrivial α ↔ ∃ (y : α), y ≠ x
Tactic: rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
rw : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (y : α), y ≠ x
rw₁ : Nontrivial α ↔ ∃ (y : α), y ≠ x
⊢ 2 ≤ #α ↔ ∃ (y : α), y ≠ x
have rw₂ : (∃ (y : α), y ≠ x) ↔ ∃ (y : α), y ≠ x
Tactic: rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have simp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
  ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
Tactic: simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have mp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
  ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
mp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
⊢ (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have mpr : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) →
  ∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have simp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
  ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
Tactic: classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
simp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have mp : (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
  ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
Tactic: classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
simp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) ↔
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
mp :
  (∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}) →
    ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
⊢ #α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
have mpr : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) →
  ∃ (t : Finset α), (↑t : Set α) = univ ∧ ∃ (x : α) (y : α), x ≠ y ∧ t = {x, y}
Tactic: classical
  simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]
  constructor
  · rintro ⟨t, ht, x, y, hne, rfl⟩
    exact ⟨x, y, hne, by simpa using ht⟩
  · rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
⊢ #α = 2 ↔ ∃! y : α, y ≠ x
have rw : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) ↔ ∃! y : α, y ≠ x
Tactic: rw [mk_eq_two_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
⊢ (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) ↔ ∃! y : α, y ≠ x
have mp : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) → ∃! y : α, y ≠ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x : α
mp : (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) → ∃! y : α, y ≠ x
⊢ (∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ) ↔ ∃! y : α, y ≠ x
have mpr : (∃! y : α, y ≠ x) → ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
x a b : α
hne : a ≠ b
h : Eq (α := Set α) {a, b} univ
⊢ ∃! y : α, y ≠ x
have h₁ : ∀ (x : α), x = a ∨ x = b
Tactic: simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y : α, y ≠ x
have mp : ∀ (hne : x ≠ b) (h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b), ∃! y : α, y ≠ x
Tactic: rcases h x with (rfl | rfl)
Cleared hypotheses: a, hne, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
mp : ∀ (hne : x ≠ b) (h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b), ∃! y : α, y ≠ x
⊢ ∃! y : α, y ≠ x
have mp₁ : ∀ (hne : a ≠ x) (h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x), ∃! y : α, y ≠ x
Tactic: rcases h x with (rfl | rfl)
Cleared hypotheses: b, hne, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
l : List α
h : (↑l.length : Cardinal.{u_1}) < #α
⊢ ∃ (z : α), z ∉ l
have contrapose! : ∀ (h : ∀ (z : α), z ∈ l), #α ≤ (↑l.length : Cardinal.{u_1})
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
l : List α
h : (↑l.length : Cardinal.{u_1}) < #α
⊢ ∃ (z : α), z ∉ l
have contrapose! : ∀ (h : (↑l.length : Cardinal.{u_1}) < #α), ∃ (z : α), z ∉ l
Tactic: classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
l : List α
h : (↑l.length : Cardinal.{u_1}) < #α
contrapose! contrapose!₁ : ∀ (h : (↑l.length : Cardinal.{u_1}) < #α), ∃ (z : α), z ∉ l
⊢ ∃ (z : α), z ∉ l
have contrapose!₂ : (∀ (z : α), z ∈ l) → #α ≤ (↑l.length : Cardinal.{u_1})
Tactic: classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ (z : α), z ≠ x ∧ z ≠ y
have this : (↑3 : Cardinal.{u_1}) ≤ #α
Tactic: have : ↑(3 : ℕ) ≤ #α := by simpa using h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this : (↑3 : Cardinal.{u_1}) ≤ #α
⊢ (↑2 : Cardinal.{u_1}) < #α
have rwa : HAdd.hAdd (α := Cardinal.{u_1}) (↑2 : Cardinal.{u_1}) 1 ≤ #α
Tactic: rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this : (↑3 : Cardinal.{u_1}) ≤ #α
⊢ ∃ (z : α), z ≠ x ∧ z ≠ y
have this₁ : (↑2 : Cardinal.{u_1}) < #α
Tactic: have : ↑(2 : ℕ) < #α := by rwa [← natCast_add_one_le_iff, ← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u_1
h : 3 ≤ #α
x y : α
this_1 : (↑3 : Cardinal.{u_1}) ≤ #α
this : (↑2 : Cardinal.{u_1}) < #α
⊢ ∃ (z : α), z ≠ x ∧ z ≠ y
have this₁ : ∃ (z : α), z ∉ [x, y]
Tactic: have := exists_notMem_of_length_lt [x, y] this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b
have refine : BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (y : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑y : Cardinal.{u}))
Tactic: refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (y : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑y : Cardinal.{u}))
have rw : BddAbove (HPow.hPow a '' Iio b)
Tactic: rw [← image_eq_range]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c
have rw : (∀ (i : (↑(Iio b) : Type (u + 1))), a ^ (↑i : Cardinal.{u}) ≤ c) ↔ ∀ x < b, a ^ x ≤ c
Tactic: rw [powerlt, ciSup_le_iff']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b c : Cardinal.{u}
rw : (∀ (i : (↑(Iio b) : Type (u + 1))), a ^ (↑i : Cardinal.{u}) ≤ c) ↔ ∀ x < b, a ^ x ≤ c
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c
have h : BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (c : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑c : Cardinal.{u}))
Tactic: rw [powerlt, ciSup_le_iff']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b c : Cardinal.{u}
⊢ BddAbove.{u + 1} (α := Cardinal.{u}) (range fun (c : (↑(Iio b) : Type (u + 1))) ↦ a ^ (↑c : Cardinal.{u}))
have h : BddAbove (HPow.hPow a '' Iio b)
Tactic: rw [← image_eq_range]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1
have apply : 1 ≤ 0 ^< a
Tactic: apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 1 ≤ 0 ^< a
have rw : HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 0 0 ≤ 0 ^< a
Tactic: rw [← power_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
⊢ a ^< 0 = 0
have convert_3 : IsEmpty.{u_1 + 2} (↑(Iio 0) : Type (u_1 + 1))
Tactic: convert! Cardinal.iSup_of_empty _
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #(↑s : Type u)
have rw : (∀ (i : { s : Set α // IsCofinal s }), c ≤ lift.{v, u} #(↑(↑i : Set α) : Type u)) ↔
  ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #(↑s : Type u)
Tactic: rw [cof, lift_iInf, le_ciInf_iff']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
⊢ ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α
have obtain : ∀ (s : { s : Set α // IsCofinal s })
  (hs :
    Eq.{u + 2} (α := Cardinal.{u}) ((fun (s : { s : Set α // IsCofinal s }) ↦ mk.{u} (↑(↑s : Set α) : Type u)) s)
      (⨅ (s : { s : Set α // IsCofinal s }), #(↑(↑s : Set α) : Type u))),
  ∃ (s : Set α), IsCofinal s ∧ #(↑s : Type u) = cof α
Tactic: obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
⊢ cof α = 0 ↔ IsEmpty α
have refine : cof α = 0 → IsEmpty α
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ by simp [cof]⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : cof α = 0
⊢ IsEmpty α
have obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), IsEmpty α
Tactic: obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
⊢ cof α = 1 ↔ ∃ (x : α), IsTop x
have refine_1 : ∀ (h : cof α = 1), ∃ (x : α), IsTop x
Tactic: refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
refine_1 : ∀ (h : cof α = 1), ∃ (x : α), IsTop x
⊢ cof α = 1 ↔ ∃ (x : α), IsTop x
have refine_2 : (∃ (x : α), IsTop x) → ∀ (t : α) (ht : IsTop t), cof α = 1
Tactic: refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
⊢ ∃ (x : α), IsTop x
have refine_1 : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), ∃ (x : α), IsTop x
Tactic: obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (hypothesis)
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ ∃ (x : α), IsTop x
have hs'₁ : ∃ (x : α), s = {x}
Tactic: rw [h, mk_set_eq_one_iff] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ (x : α), s = {x}
⊢ ∃ (x : α), IsTop x
have refine_1 : ∀ (t : α) (hs : IsCofinal (α := α) {t}), ∃ (x : α), IsTop x
Tactic: obtain ⟨t, rfl⟩ := hs'
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
t : α
hs : IsCofinal (α := α) {t}
⊢ ∃ (x : α), IsTop x
have h₁ : IsTop t
Tactic: use t
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : cof α = 1
t : α
hs : IsCofinal (α := α) {t}
⊢ IsTop t
have h₁ : ∀ (hs : IsTop t), IsTop t
Tactic: rwa [isCofinal_singleton_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
⊢ cof α = 1
have refine_2 : cof α ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
refine_2 : cof α ≤ 1
⊢ cof α = 1
have refine_2₁ : 1 ≤ cof α
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
⊢ cof α ≤ 1
have apply : IsCofinal (α := α) {t}
Tactic: apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
h : ∃ (x : α), IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α
have refine_2 : Nonempty α
Tactic: rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α
have rw : (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Tactic: rw [← not_iff_not, not_not, noTopOrder_iff, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ (x : α), IsTop x
have rw : (cof α = 0 ∨ ∃ (x : α), IsTop x) ↔ ∃ (x : α), IsTop x
Tactic: rw [le_iff_lt_or_eq, Cardinal.lt_one_iff, cof_eq_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Nonempty α
⊢ 1 < cof α ↔ NoTopOrder α
have rw : (∃ (x : α), IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Tactic: rw [← not_iff_not, not_lt, noTopOrder_iff, cof_le_one_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) = lift.{u, v} (cof β)
have a : lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
a : lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)
⊢ lift.{v, u} (cof α) = lift.{u, v} (cof β)
have a₁ : lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)
have a : ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
Tactic: rw [le_lift_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)
have a : ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)
Tactic: rw [le_lift_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
have H : ∀ (x : (↑s : Type v)), ∃ (y : α), (↑x : β) ≤ f y
Tactic: have H (x : s) : ∃ y : α, x ≤ f y := by simpa using hf' x
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
H : ∀ (x : (↑s : Type v)), ∃ (y : α), (↑x : β) ≤ f y
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
have a : ∀ (g : (x : (↑s : Type v)) → α) (hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)),
  lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
Tactic: choose g hg using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #(↑s : Type v)
have a : ∀ (a : α), ∃ y ∈ range g, a ≤ y
Tactic: refine (lift_le.2 <| cof_le (s := range g) fun a ↦ ?_).trans mk_range_le_lift
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a : α
⊢ ∃ y ∈ range g, a ≤ y
have a₁ : ∀ (b : α) (hb : f a ≤ f b), ∃ y ∈ range g, a ≤ y
Tactic: obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' (f a)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
⊢ ∃ y ∈ range g, a ≤ y
have a₁ : ∀ (c : β) (hc : c ∈ s) (hc' : f b ≤ c), ∃ y ∈ range g, a ≤ y
Tactic: obtain ⟨c, hc, hc'⟩ := hs (f b)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ ∃ y ∈ range g, a ≤ y
have a₁ : a ≤ g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc)
Tactic: refine ⟨_, Set.mem_range_self ⟨c, hc⟩, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : (x : (↑s : Type v)) → α
hg : ∀ (x : (↑s : Type v)), (↑x : β) ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ a ≤ g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc)
have a₁ : f a ≤ f (g (Subtype.mk (p := fun (x : β) ↦ x ∈ s) c hc))
Tactic: rw [← hf.le_iff_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
⊢ cof α < ℵ₀ ↔ cof α ≤ 1
have refine : ∀ (h : cof α < ℵ₀), cof α ≤ 1
Tactic: refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
⊢ cof α ≤ 1
have obtain : ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = cof α), cof α ≤ 1
Tactic: obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ s.Finite
have rw : #(↑s : Type u) < ℵ₀
Tactic: rw [Set.Finite, ← mk_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (hypothesis)
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
⊢ cof α ≤ 1
have hf : s.Finite
Tactic: have hf : s.Finite := by
    rw [Set.Finite, ← mk_lt_aleph0_iff]
    exact hs'.trans_lt h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
hf : s.Finite
⊢ cof α ≤ 1
have obtain : ∀ (t : Set α) (ht : t.Subsingleton) (ht' : IsCofinal t), cof α ≤ 1
Tactic: obtain ⟨t, ht, ht'⟩ := hf.exists_subsingleton_isCofinal hs
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
inst : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = cof α
hf : s.Finite
t : Set α
ht : t.Subsingleton
ht' : IsCofinal t
⊢ cof α ≤ 1
have apply : #(↑t : Type u) ≤ 1
Tactic: apply (cof_le ht').trans
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)
have rw : ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #(↑s : Type u)
Tactic: rw [le_lift_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : #(↑s : Type u_1) < cof α
⊢ ∃ x ∈ s, IsCofinal x
have contrapose! : ∀ (h₂ : ∀ (x : Set α) (_ : x ∈ s), ¬IsCofinal x), cof α ≤ #(↑s : Type u_1)
Tactic: contrapose! h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ (x : Set α) (_ : x ∈ s), ¬IsCofinal x
⊢ cof α ≤ #(↑s : Type u_1)
have h₃ : ∀ (x : Set α) (_ : x ∈ s), ∃ (x_1 : α), ∀ y ∈ x, y < x_1
Tactic: simp_rw [not_isCofinal_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ (x : Set α) (_ : x ∈ s), ∃ (x_1 : α), ∀ y ∈ x, y < x_1
⊢ cof α ≤ #(↑s : Type u_1)
have choose : ∀ (f : (x : Set α) → (_ : x ∈ s) → α) (hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _), cof α ≤ #(↑s : Type u_1)
Tactic: choose f hf using h₂
Cleared hypotheses: h₂