awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
n : ℕ
⊢ (toNat : (a : Cardinal.{u_1}) → ℕ) (↑n : Cardinal.{u_1}) = n

Tactic:
toNat_ofENat n

Premises used: Cardinal.toNat_ofENat, Nat.cast, Cardinal.ofENat, ENat.toNat, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
rw₁ :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (0 : ℕ∞) ∨
      Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔
    c = 0 ∨ ℵ₀ ≤ c
rw₂ : c = 0 ∨ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) (⊤ : ℕ∞) ↔ c = 0 ∨ ℵ₀ ≤ c
rw₃ rw₄ : c = 0 ∨ ℵ₀ ≤ c ↔ c = 0 ∨ ℵ₀ ≤ c
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]

Premises used: Cardinal.toENat_eq_zero, Cardinal.toNat_toENat, Cardinal.toENat_eq_top, ENat.toNat_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
⊢ Ne (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (0 : ℕ) ↔ c ≠ 0 ∧ c < ℵ₀

Tactic:
simp [not_or]

Premises used: not_or
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
⊢ LT.lt (α := ℕ) (0 : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ↔ c ≠ 0 ∧ c < ℵ₀

Tactic:
pos_iff_ne_zero.trans toNat_ne_zero

Premises used: Iff.trans, Cardinal.toNat_ne_zero, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c < ℵ₀

Tactic:
h
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
lift :
  ∀ (c : ℕ),
    Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) (↑c : Cardinal.{u_1})) : Cardinal.{u_1})
      (↑c : Cardinal.{u_1})
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) = c

Tactic:
lift c to ℕ using h
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : ℕ
rw rw₁ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑c : Cardinal.{u_1})
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) (↑c : Cardinal.{u_1})) : Cardinal.{u_1})
    (↑c : Cardinal.{u_1})

Tactic:
rw [toNat_natCast]

Premises used: Cardinal.toNat_natCast
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
h : c < ℵ₀
rw : c = (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) ⋯) : Cardinal.{u})
rw₁ rw₂ : c = c
⊢ Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) c) : Cardinal.{u})
    (↑(Classical.choose (p := fun (x : ℕ) ↦ c = (↑x : Cardinal.{u})) ⋯) : Cardinal.{u})

Tactic:
rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]

Premises used: Classical.choose_spec, Iff.mp, Cardinal.cast_toNat_of_lt_aleph0, Cardinal.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) c : ℕ) (0 : ℕ)

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑0 : Cardinal.{u_2}) 0
rw₁ rw₂ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) 0 0
⊢ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_2}) 0

Tactic:
rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]

Premises used: Cardinal.toNat_apply_of_aleph0_le, Nat.cast_zero
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) = c
rw : (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) < ℵ₀
⊢ c < ℵ₀

Tactic:
rw [← h]
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u_1}
h : (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) = c
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) c) : Cardinal.{u_1}) < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
simp : ∀ (i i_1 : ℕ), i < i_1 → i < i_1
⊢ StrictMonoOn (β := ℕ) (⇑toNat : (a : Cardinal.{u_1}) → ℕ) (Iio ℵ₀)

Tactic:
simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]

Premises used: Set.forall_mem_range, Cardinal.range_natCast, Cardinal.toNat_natCast, StrictMonoOn, Nat.cast_lt
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1

Tactic:
fun _ _ ↦ id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ MonotoneOn (β := ℕ) (⇑toNat : (a : Cardinal.{u_1}) → ℕ) (Iio ℵ₀)

Tactic:
toNat_strictMonoOn.monotoneOn

Premises used: Cardinal.toNat_strictMonoOn, StrictMonoOn.monotoneOn
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ InjOn (β := ℕ) (⇑toNat : (a : Cardinal.{u_1}) → ℕ) (Iio ℵ₀)

Tactic:
toNat_strictMonoOn.injOn

Premises used: StrictMonoOn.injOn, Cardinal.toNat_strictMonoOn
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ) ↔ c = d

Tactic:
toNat_injOn.eq_iff hc hd

Premises used: Set.InjOn.eq_iff, Cardinal.toNat_injOn
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ LE.le (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ) ↔ c ≤ d

Tactic:
toNat_strictMonoOn.le_iff_le hc hd

Premises used: Cardinal.toNat_strictMonoOn, StrictMonoOn.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ LT.lt (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ) ↔ c < d

Tactic:
toNat_strictMonoOn.lt_iff_lt hc hd

Premises used: Cardinal.toNat_strictMonoOn, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hcd : c ≤ d
hd : d < ℵ₀
⊢ LE.le (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)

Tactic:
toNat_monotoneOn (hcd.trans_lt hd) hd hcd

Premises used: Cardinal.toNat_monotoneOn, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hcd : c < d
hd : d < ℵ₀
⊢ LT.lt (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)

Tactic:
toNat_strictMonoOn (hcd.trans hd) hd hcd

Premises used: Cardinal.toNat_strictMonoOn, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) (OfNat.ofNat n) : ℕ) (OfNat.ofNat n : ℕ)

Tactic:
toNat_natCast n

Premises used: Cardinal.toNat_natCast
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ RightInverse (α := Cardinal.{u_1}) Nat.cast (⇑toNat : (a : Cardinal.{u_1}) → ℕ)

Tactic:
toNat_natCast

Premises used: Function.LeftInverse, Function.RightInverse, Cardinal.toNat_natCast
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ Surjective (α := Cardinal.{u_1}) (β := ℕ) (⇑toNat : (a : Cardinal.{u_1}) → ℕ)

Tactic:
toNat_rightInverse.surjective

Premises used: Cardinal.toNat_rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
α : Type u
h : Infinite α
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) ℵ₀ : ℕ) (0 : ℕ)

Tactic:
toNat_apply_of_aleph0_le le_rfl

Premises used: le_rfl, Cardinal.toNat_apply_of_aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
α : Type u
inst : Fintype α
⊢ (toNat : (a : Cardinal.{u}) → ℕ) #α = Fintype.card α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) 1 : ℕ) (1 : ℕ)

Tactic:
map_one _

Premises used: map_one
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
rw : ENat.toNat ((toENat : (a : Cardinal.{u}) → ℕ∞) c) = n ↔ c = (↑n : Cardinal.{u})
rw₁ : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c = (↑n : Cardinal.{u})
rw₂ rw₃ : c = (↑n : Cardinal.{u}) ↔ c = (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) c = n ↔ c = (↑n : Cardinal.{u})

Tactic:
rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_natCast]

Premises used: ENat.toNat_eq_iff, Cardinal.toNat_toENat, Cardinal.toENat_eq_natCast
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (OfNat.ofNat n : ℕ) ↔ c = OfNat.ofNat n

Tactic:
toNat_eq_iff <| OfNat.ofNat_ne_zero n

Premises used: Cardinal.toNat_eq_iff, OfNat.ofNat_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{u}
rw : c = (↑1 : Cardinal.{u}) ↔ c = 1
rw₁ rw₂ : c = 1 ↔ c = 1
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) (1 : ℕ) ↔ c = 1

Tactic:
rw [toNat_eq_iff one_ne_zero, Nat.cast_one]

Premises used: Cardinal.toNat_eq_iff, one_ne_zero, Nat.cast_one
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
α : Type u
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) (1 : ℕ) ↔ Subsingleton α ∧ Nonempty α

Tactic:
toNat_eq_one.trans eq_one_iff_unique

Premises used: Cardinal.toNat_eq_one, Cardinal.eq_one_iff_unique, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c : Cardinal.{v}
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{u, v} c) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) c : ℕ)

Tactic:
simp only [← toNat_toENat, toENat_lift]

Premises used: Cardinal.toENat_lift, Cardinal.toNat_toENat
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
α : Type u
β : Type v
e : α ≃ β
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{v, u} #α) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max v u}) → ℕ) (lift.{max u v, v} #β) : ℕ)
    ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
rw₂ rw₃ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) #α : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) #β : ℕ)

Tactic:
rw [← toNat_lift, (lift_mk_eq.{_, _, v}).mpr ⟨e⟩, toNat_lift]

Premises used: Cardinal.toNat_lift
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
x y : Cardinal.{u_1}
⊢ (toNat : (a : Cardinal.{u_1}) → ℕ) (x * y) =
    HMul.hMul (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) x : ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) y : ℕ)

Tactic:
map_mul toNat x y

Premises used: Cardinal.toNat, map_mul
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ c < ℵ₀

Tactic:
hc
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
lift :
  ∀ (c : ℕ),
    (toNat : (a : Cardinal.{u}) → ℕ) ((↑c : Cardinal.{u}) + d) =
      HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
        ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)
⊢ (toNat : (a : Cardinal.{u}) → ℕ) (c + d) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) c : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)

Tactic:
lift c to ℕ using hc
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
⊢ d < ℵ₀

Tactic:
hd
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
d : Cardinal.{u}
hd : d < ℵ₀
c : ℕ
lift :
  ∀ (d : ℕ),
    (toNat : (a : Cardinal.{u}) → ℕ) (HAdd.hAdd (α := Cardinal.{u}) (↑c : Cardinal.{u}) (↑d : Cardinal.{u})) =
      HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
        ((toNat : (a : Cardinal.{u}) → ℕ) (↑d : Cardinal.{u}) : ℕ)
⊢ (toNat : (a : Cardinal.{u}) → ℕ) ((↑c : Cardinal.{u}) + d) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) d : ℕ)

Tactic:
lift d to ℕ using hd
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
c d : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : c + d = c + d
⊢ (toNat : (a : Cardinal.{u}) → ℕ) (HAdd.hAdd (α := Cardinal.{u}) (↑c : Cardinal.{u}) (↑d : Cardinal.{u})) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑c : Cardinal.{u}) : ℕ)
      ((toNat : (a : Cardinal.{u}) → ℕ) (↑d : Cardinal.{u}) : ℕ)

Tactic:
norm_cast
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ (toNat : (a : Cardinal.{max u v}) → ℕ) (lift.{v, u} a + lift.{u, v} b) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) a : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) b : ℕ)

Tactic:
simp [*]
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u_1}
inl : ∀ (h : a < ℵ₀), (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
inr : ∀ (h : ℵ₀ ≤ a), (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a

Tactic:
obtain h | h := lt_or_ge a ℵ₀

Premises used: Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a

Tactic:
simp [cast_toNat_of_lt_aleph0 h]

Premises used: Cardinal.cast_toNat_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ (↑((toNat : (a : Cardinal.{u_1}) → ℕ) a) : Cardinal.{u_1}) ≤ a

Tactic:
simp [Cardinal.toNat_apply_of_aleph0_le h]

Premises used: Cardinal.toNat_apply_of_aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
nth_rw :
  LE.le (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) a : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑n : Cardinal.{u}) : ℕ) ↔
    a ≤ (↑n : Cardinal.{u})
nth_rw₁ nth_rw₂ : a ≤ (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a ≤ n ↔ a ≤ (↑n : Cardinal.{u})

Tactic:
nth_rw 1 [← Cardinal.toNat_natCast.{u} n,
    Cardinal.toNat_le_iff_le_of_lt_aleph0 lt (Cardinal.natCast_lt_aleph0)]

Premises used: Cardinal.natCast_lt_aleph0, Cardinal.toNat_le_iff_le_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
nth_rw :
  (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔
    Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) a) : Cardinal.{u}) (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔ a = (↑n : Cardinal.{u})

Tactic:
nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt]

Premises used: Cardinal.cast_toNat_of_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔
    Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) a) : Cardinal.{u}) (↑n : Cardinal.{u})

Tactic:
Nat.cast_inj.symm

Premises used: Nat.cast_inj, Iff.symm
-- Module: Mathlib.SetTheory.Cardinal.ToNat
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔
    Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) a) : Cardinal.{u}) (↑n : Cardinal.{u})

Tactic:
exact Nat.cast_inj.symm

Premises used: Nat.cast_inj, Iff.symm
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
simp_rw : (∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
⊢ UnivLE.{u, v} ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
simp_rw [univLE_iff, small_iff_lift_mk_lt_univ]

Premises used: univLE_iff, Cardinal.small_iff_lift_mk_lt_univ
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
contrapose! : (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}
⊢ (∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
⊢ (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: _private.0.univLE_iff_cardinal_le.match_2, Cardinal.univ, LT.lt, Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
refine_1 :
  (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) →
    ∀ (α : Type u) (le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α), univ.{v, u + 1} < univ.{u, v + 1}
refine_2 : ∀ (h : univ.{v, u + 1} < univ.{u, v + 1}), ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h : ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α

Tactic:
rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift] at le

Premises used: Cardinal.lift_univ, Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h : ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
le.trans_lt (lift_lt_univ'.{u, v + 1} #α)

Premises used: Cardinal.mk, Cardinal.lift_lt_univ', LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h : ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
exact le.trans_lt (lift_lt_univ'.{u, v + 1} #α)
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h : univ.{v, u + 1} < univ.{u, v + 1}
refine_2 :
  ∀ (w : Cardinal.{u}) (α : Type u)
    (h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)),
    ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
obtain ⟨⟨α⟩, h⟩ := lt_univ'.mp h

Premises used: Iff.mp, Cardinal.lt_univ'
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
h₁ : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
use α
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
h₁ : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift]

Premises used: Cardinal.lift_univ, Cardinal.lift_lift
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α

Tactic:
h.le

Premises used: Eq.le
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α

Tactic:
exact h.le

Premises used: Eq.le
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
rw : univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
rw [univLE_iff_cardinal_le]

Premises used: univLE_iff_cardinal_le
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
lift_mk_le'

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
exact lift_mk_le'

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
f : Ordinal.{u} → Ordinal.{v}
h : Function.Injective f
⊢ UnivLE.{u, v}

Tactic:
univLE_iff_exists_embedding.2 ⟨f, h⟩

Premises used: univLE_iff_exists_embedding, Iff.mpr, Function.Embedding.mk, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
simp_rw : univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
simp_rw [univLE_iff_cardinal_le]

Premises used: univLE_iff_cardinal_le
-- Module: Mathlib.SetTheory.Cardinal.UnivLE
Goal:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}

Tactic:
apply le_total

Premises used: le_total
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T : Set (List A) | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
w : Set (List A)
left : t ∈ S
right : x ∈ t
⊢ x ∈ sSup S

Tactic:
use t, ht, hS ht hx
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T : Set (List A) | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
h : x ++ [a] ∈ sInf S
T : Set (List A)
hT : T ∈ S
⊢ x ∈ T

Tactic:
hS hT <| h T hT
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T : Set (List A) | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
h : x ++ [a] ∈ sInf S
T : Set (List A)
hT : T ∈ S
⊢ x ∈ T

Tactic:
exact hS hT <| h T hT
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x : List A
h : x ++ [] ∈ T
⊢ x ∈ T

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A} (h : x ++ ys ∈ T), x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ++ [y] ++ ys ∈ T

Tactic:
simpa
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A} (h : x ++ ys ∈ T), x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ∈ T

Tactic:
exact T.prop (ih (by simpa))

Premises used: Subtype.prop
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : x ++ y ∈ T
nil : ∀ {x : List A} (h : x ++ [] ∈ T), x ∈ T
cons : ∀ (y : A) (ys : List A) (ih : ∀ {x : List A} (h : x ++ ys ∈ T), x ∈ T) {x : List A} (h : x ++ y :: ys ∈ T), x ∈ T
⊢ x ∈ T

Tactic:
induction y generalizing x with
  | nil => simpa using h
  | cons y ys ih => exact T.prop (ih (by simpa))
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h' : x <+: y
h : y ∈ T
obtain : ∀ (w : List A) (h : x ++ w ∈ T), x ∈ T
⊢ x ∈ T

Tactic:
obtain ⟨_, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x w : List A
h : x ++ w ∈ T
⊢ x ∈ T

Tactic:
mem_of_append h

Premises used: Descriptive.Tree.mem_of_append
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
x w : List A
h : x ++ w ∈ T
⊢ x ∈ T

Tactic:
exact mem_of_append h

Premises used: Descriptive.Tree.mem_of_append
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
a : A
x : List A
h : a :: x ∈ T
⊢ [a] ∈ T

Tactic:
mem_of_prefix ⟨x, rfl⟩ h

Premises used: Descriptive.Tree.mem_of_prefix, Exists.intro, rfl
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
⊢ [] ∉ ⊥

Tactic:
simp
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
h₁ : ∀ (x : List A), x ∈ T ↔ Membership.mem (γ := ↥(tree A)) ⊥ x
⊢ T = ⊥

Tactic:
ext x
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∈ T ↔ Membership.mem (γ := ↥(tree A)) ⊥ x

Tactic:
simpa using fun h' ↦ h <| mem_of_prefix x.nil_prefix h'

Premises used: Descriptive.Tree.mem_of_prefix, List.nil_prefix
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
n : ℕ
x : ↥T
⊢ List.take n (↑x : List A) ∈ T

Tactic:
mem_of_prefix (x.val.take_prefix n) x.prop

Premises used: Descriptive.Tree.mem_of_prefix, List.take_prefix, Subtype.prop, Subtype.val
-- Module: Mathlib.SetTheory.Descriptive.Tree
Goal:
A : Type u_1
T : ↥(tree A)
m n : ℕ
x : ↥T
⊢ take m (take n x) = take (min m n) x

Tactic:
simp [Subtype.ext_iff, List.take_take]

Premises used: Subtype.ext_iff, List.take_take