mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
[

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u}
h : o < ω
⊢ o < ℵ₀.ord

Tactic:
rcases Ordinal.lt_lift_iff.1 h with ⟨o, ho, rfl⟩

Goal state after:
o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ Ordinal.lift.{u, 0} o < ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}
⊢ blsub 0 f = 0

Tactic:
by rw [blsub_eq_zero_iff]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
simp [hb, log_of_left_le_one]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : succ (f b hb) = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
[

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : succ (f b hb) = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ x, a ^ ↑x

Tactic:
[

Goal state after:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ x, a ^ ↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
      apply Nat.lt_succ_self

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ n, o = ↑n

Tactic:
[

Goal state after:
o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ n, o = ↑n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0

Tactic:
[

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < clog b n

Tactic:
rw [clog, if_pos]

Goal state after:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

case hc
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
[

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y

Tactic:
[

Goal state after:
case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x

Tactic:
[

Goal state after:
case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y

Tactic:
rintro ⟨hx₁, hx₂⟩
    apply le_antisymm
    · rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]
    · rwa [← opow_le_iff_le_log hb hx]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, a ≤ derivFamily f o' → ∃ o, derivFamily f o = a
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = a

Tactic:
intro h₁
      rcases eq_or_lt_of_le h₁ with h | h
      · exact ⟨_, h.symm⟩
      rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h
      obtain ⟨o', h⟩ := h
      exact IH o' o'.2 (le_of_not_ge h)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝

Tactic:
[

Goal state after:
x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a

Tactic:
exact iterate_le_nfp ..

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

Tactic:
[

Goal state after:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preOmega ω = ω

Tactic:
[

Goal state after:
⊢ preOmega ω = ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c ^ b)

Tactic:
· rw [← opow_mul]
    exact isPrincipal_add_omega0_opow _

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
[

Goal state after:
case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x

Tactic:
[

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)) → x ∈ range fun a ↦ preBeth ↑a

Tactic:
rintro ⟨⟨i, hi⟩, rfl⟩

Goal state after:
case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ (fun i ↦ lift.{v, u_1} (preBeth ↑i)) ⟨i, hi⟩ ∈ range fun a ↦ preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun a ↦ preBeth ↑a) → x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
rintro ⟨⟨i, hi⟩, rfl⟩

Goal state after:
case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) = Cardinal.lift.{u + 1, v} (Order.cof β)

Tactic:
this

Goal state after:
case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

pp: case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i ∈ Iio (⨆ i, f i + 1)

Tactic:
· have := lift_cof_congr_of_strictMono this ?_
    · rw [← Cardinal.lift_inj.{_, max (u + 1) v}, Cardinal.lift_lift.{_, _, v},
        Cardinal.lift_umax.{_, u + 1}, Cardinal.lift_umax.{_, u + 1}, this]
      simp
    · intro ⟨b, hb⟩
      rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb
      obtain ⟨i, hi⟩ := hb
      exact ⟨_, Set.mem_range_self i, hi⟩

Goal state after:
case refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
i : β
⊢ f i ∈ Iio (⨆ i, f i + 1)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Tactic:
[

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
[

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 ≤ o

Tactic:
[

Goal state after:
case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 ≤ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i

Tactic:
[

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j

Tactic:
[

Goal state after:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
| Cardinal.lift.{u + 1, v} c

Tactic:
rw [← Cardinal.lift_lift.{u, u + 1}]

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
| Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

pp: case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
· have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
    simp [iSup, csSup_of_not_bddAbove, hf, hfc]

Goal state after:
case pos
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i

Tactic:
[

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
[

Goal state after:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
⊢ Cardinal.lift.{?u.36, u} #ι < c.cof

Tactic:
(#ι).lift_id

Goal state after:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
⊢ #ι < c.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #↑{x | Bounded r x} ≤ #α

Tactic:
this

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
⊢ #↑(⋃ i, 𝒫 {j | r j i}) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ a, #α < #↑(f ⁻¹' {a})

Tactic:
[

Goal state after:
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
⊢ ∃ a, #α < #↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
by
  rcases le_or_gt ℵ₀ c with h | h
  · rw [powerlt_aleph0 h]
    apply le_max_left
  rw [powerlt_le]
  exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Tactic:
[

Goal state after:
α : Type u
β' : Type v
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})

Tactic:
[

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
⊢ ∃ a, Infinite ↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)

Tactic:
[

Goal state after:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, Uncountable ↑(f ⁻¹' {a})

Tactic:
[

Goal state after:
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, Uncountable ↑(f ⁻¹' {a})
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ IsCofinal s

Tactic:
[

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ IsCofinal s
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (x.1, f x.1 ^^ (f x.1 ^^ x.2)) = x

Tactic:
[

Goal state after:
case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (x.1, f x.1 ^^ (f x.1 ^^ x.2)) = x
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
[

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #↑(Iio b) < (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof

Tactic:
rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
⊢ b < c.ord → derivFamily f b < c.ord

Tactic:
| limit b hb H =>

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : (linearCombination R v') l = (linearCombination R v') l'
⊢ l = l'

Tactic:
[

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : (linearCombination R v') l = (linearCombination R v') l'
⊢ l = l'
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : (linearCombination R v') l = (linearCombination R v') l'
⊢ l = l'

Tactic:
simp_rw [linearCombination_option, v', Option.elim] at z

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z :
  l none • b i +
      (linearCombination R
          ((fun o ↦
              match o, b i, v with
              | Option.some x, x_1, f => f x
              | none, y, x => y) ∘
            Option.some))
        l.some =
    l' none • b i +
      (linearCombination R
          ((fun o ↦
              match o, b i, v with
              | Option.some x, x_1, f => f x
              | none, y, x => y) ∘
            Option.some))
        l'.some
⊢ l = l'
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
⊢ (b.repr ((linearCombination R v) l.some)) i = (b.repr ((linearCombination R v) l'.some)) i

Tactic:
[

Goal state after:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
⊢ (b.repr ((linearCombination R v) l.some)) i = (b.repr ((linearCombination R v) l'.some)) i
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
[

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
obtain hj | (hj : f j = 0) := s.prop j
          · exact Or.inl (Multiset.mem_cons_of_mem hj)
          · exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j

Tactic:
simp [hi.symm]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | f i ≠ 0}
left✝ : i ∈ sx.toFinset
h : f i ≠ 0
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
exact Finset.mem_filter.2 ⟨Multiset.mem_toFinset.2 <| (hy i).resolve_right h, h⟩

Goal state after: