mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
by
  rw [← encard_eq_three, ncard_def]
  simp

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a

Tactic:
mem_Ici,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ succ a ≤ x ↔ x ∈ Ioi a
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ x ∈ Ici a

Tactic:
mem_Ici,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ pred a < x ↔ a ≤ x
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ (update f i b i) c = update (fun i ↦ (f i) c) i (b c) i

Tactic:
update_self,

Goal state after:
case pos
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ b c = update (fun i ↦ (f i) c) i (b c) i
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a

Tactic:
mem_Ici,

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d ≤ a + d + c
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))

Tactic:
exact (Ici_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => le_of_add_le_add_right hx.2

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ i ∈ Ioc a b, f i) * ∏ i ∈ {b + 1}, f i = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Tactic:
prod_singleton

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ i ∈ Ioc a b, f i) * f (b + 1) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ (∏ k ∈ range m, f k) / ∏ k ∈ range n, f k = ∏ k ∈ range m with n ≤ k, f k

Tactic:
rw [← prod_Ico_eq_div f hnm]

Goal state after:
G : Type u_4
inst✝ : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ ∏ k ∈ Ico n m, f k = ∏ k ∈ range m with n ≤ k, f k
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))

Goal state after:
case pos
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

case neg
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
hn_max : ¬IsMax (succ^[↑n] ⊥)
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} < span {y} ↔ DvdNotUnit y x

Tactic:
by
  rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Finset α
⊢ ∑ m ∈ range (#x + 1), (#x).choose m • (-1) ^ m = if x = ∅ then 1 else 0

Tactic:
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (Ici '' s) ≤ generate (range Ici)

Tactic:
rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (Ici '' s)) A B

Goal state after:
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f

Tactic:
← @map_id _ g,

Goal state after:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map id g ≤ map mab f
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Tactic:
by
  rw [Tendsto, Tendsto, map_map]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
⊢ ∀ᶠ (x : α) in f, x ∈ x✝ → p x

Tactic:
filter_upwards [h] with _ pa _ using pa

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q

Tactic:
simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
exact Nat.exists_strictMono_subsequence h

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
intro n
    cases n <;> simp [hu']

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ Bounded r {x}

Tactic:
refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ ∀ b ∈ {x}, r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (cof α).ord ≤ typeLT α

Tactic:
rw [ord_le, card_type]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α ≤ #α
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔ o₁ ≤ o₂

Tactic:
by
  rw [← enum_le_enum, not_lt]

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

Goal state before:
pp: o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩ ≤ a

Tactic:
rw [← not_lt]
  apply enum_zero_le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < o

Tactic:
by
      rw [← ho]
      exact typein_lt_type r i

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ b + c ≤ b + (a - b)

Tactic:
exact h.trans (le_add_sub a b)

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

Goal state before:
pp: case inl
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
⊢ a - b < c

Tactic:
Ordinal.sub_eq_zero_iff_le.2 hab.le

Goal state after:
case inl
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
⊢ 0 < c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (hr : o < type r) (hs : o < type s), f ((enum r) ⟨o, hr⟩) = (enum s) ⟨o, hs⟩

Tactic:
refine inductionOn o ?_; rintro γ t wo ⟨g⟩ ⟨h⟩
  rw [enum_type g, enum_type (g.transRelIso f)]; rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
this✝ : Bot ↑s := { bot := ⟨sInf s, ⋯⟩ }
this : OrderBot ↑s := { toBot := this✝, bot_le := ⋯ }
⊢ ↑((enum s hs) ⊥) = sInf s

Tactic:
OrderIso.map_bot

Goal state after:
α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
this✝ : Bot ↑s := { bot := ⟨sInf s, ⋯⟩ }
this : OrderBot ↑s := { toBot := this✝, bot_le := ⋯ }
⊢ ↑⊥ = sInf s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : lift.{max u v, max u v} (type s) < lift.{u, v} (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)

Tactic:
← lift_umax.{v, u},

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : lift.{max u v, max u v} (type s) < lift.{max v u, v} (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup ∅ ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
csSup_of_not_bddAbove (s := _ '' _)

Goal state after:
case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup ∅ ≤ sSup ∅

case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]
    intro i
    obtain ⟨j, hj⟩ := exists_gt i
    apply (le_ciSup hf' j).trans'
    rw [add_one_le_iff]
    exact hf hj

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

Goal state before:
pp: case h₁
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < a, enumOrd s c < b}).Nonempty

pp: case h₁
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a b c : Ordinal.{u}
a✝ : c < a
⊢ enumOrd t c ≤ enumOrd s c

Tactic:
exacts [enumOrd_nonempty hs a, enumOrd_le_of_subset hs hst c]

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
have := type_ne_zero_iff_nonempty.1 h
    rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r] <;>
      rfl

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

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

Tactic:
← iSup_eq_bsup,

Goal state after:
f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ iSup (familyOfBFamily 1 f) = f 0 ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_1
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a✝ < c
a : { x // Prod.Lex s r x (b, a✝) }
⊢ { x // s x b } × α ⊕ { x // r x a✝ }

pp: case refine_2
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a✝ < c
a b : { x // Prod.Lex s r x (b✝, a✝) }
⊢ Subrel (Prod.Lex s r) (fun x ↦ Prod.Lex s r x (b✝, a✝)) a b →
    Sum.Lex (Prod.Lex (Subrel s fun x ↦ s x b✝) r) (Subrel r fun x ↦ r x a✝) ?refine_1 ?refine_1

Tactic:
· rcases a with ⟨⟨b', a'⟩, h⟩
    by_cases e : b = b'
    · exact .inr ⟨a', by grind [asymm_of s]⟩
    · exact .inl (⟨b', by grind⟩, a')

Goal state after:
case refine_2
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a✝ < c
a b : { x // Prod.Lex s r x (b✝, a✝) }
⊢ Subrel (Prod.Lex s r) (fun x ↦ Prod.Lex s r x (b✝, a✝)) a b →
    Sum.Lex (Prod.Lex (Subrel s fun x ↦ s x b✝) r) (Subrel r fun x ↦ r x a✝)
      (Subtype.casesOn a fun val h ↦
        Prod.casesOn (motive := fun x ↦ Prod.Lex s r x (b✝, a✝) → { x // s x b✝ } × α ⊕ { x // r x a✝ }) val
          (fun b' a' h ↦ if e : b✝ = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      (Subtype.casesOn b fun val h ↦
        Prod.casesOn (motive := fun x ↦ Prod.Lex s r x (b✝, a✝) → { x // s x b✝ } × α ⊕ { x // r x a✝ }) val
          (fun b' a' h ↦ if e : b✝ = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f

Tactic:
← iSup_eq_bsup,

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = o.blsub f ∨ succ (iSup (o.familyOfBFamily f)) = o.blsub f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ a < c.ord

Tactic:
← Ordinal.lift_lt

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{?u.37, v} a < Ordinal.lift.{?u.37, v} c.ord
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f

Tactic:
← iSup_eq_bsup,

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = o.blsub f ↔ ∀ a < o.blsub f, succ a < o.blsub f
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b : Ordinal.{u_1}
h✝ : a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases b = 0

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case neg
a b : Ordinal.{u_1}
h✝ : ¬a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
by_cases b = 0

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
· rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]
    · simp
    exact fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt

Goal state after:
case inr.inl
b c : Ordinal.{u_1}
ha : 0 < 1
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

case inr.inr
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

Tactic:
simpa [hc] using hb.ne_bot

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

Goal state before:
pp: case limit.inr
ι : 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
h₁ : a ≤ derivFamily f o
h : a < derivFamily f o
⊢ ∃ o, derivFamily f o = a

Tactic:
rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h

Goal state after:
case limit.inr
ι : 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
h₁ : a ≤ derivFamily f o
h : ∃ x, ¬derivFamily f ↑x ≤ a
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m n : ℕ
hm : m ≤ 1
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
Nat.log_of_left_le_one hm

Goal state after:
m n : ℕ
hm : m ≤ 1
⊢ ↑0 = log ↑m ↑n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x ↦ a✝ + x) (a✝ * ω + a + 1) = a✝ * ω + a + 1

Tactic:
exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

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

Goal state before:
pp: ⊢ ¬BddAbove {x | x.IsInitial}

Tactic:
by
  rintro ⟨a, ha⟩
  have := ha (isInitial_ord (succ a.card))
  rw [ord_le] at this
  exact (lt_succ _).not_ge this

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

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
g : α × α → α := uncurry max
⊢ #α * #α ≤ #α

Tactic:
let f : α × α ↪ α ×ₗ (α ×ₗ α) := ⟨fun p ↦ toLex (g p, toLex p), fun p q ↦ congrArg Prod.snd⟩

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 * b < o

Tactic:
rwa [zero_mul]

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

Goal state before:
pp: case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
← h a ha hao

Goal state after:
case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < a * o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
rw [max_le_iff]

Goal state after:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ_ 1 ↔ c = ℵ_ 1

Tactic:
by
  simp [eqComm]

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Tactic:
rw [max_le_iff]

Goal state after:
a b : Cardinal.{u_1}
⊢ a + b = a ↔ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = ℵ_ ↑n ↔ c = ℵ_ ↑n

Tactic:
by
  simp [eqComm]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c = ℶ_ ↑n ↔ c = ℶ_ ↑n

Tactic:
by
  simp [eqComm]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o = ω_ 1 ↔ o = ω_ 1

Tactic:
by
  simp [eqComm]

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o = ω_ ↑n ↔ o = ω_ ↑n

Tactic:
by
  simp [eqComm]

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _)

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a.card ≤ (a ^ b).card

a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b.card ≤ (a ^ b).card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c

Tactic:
← power_mul,

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 2 ^ (c * c) ≤ 2 ^ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^ c = 2 ^ c

Tactic:
apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
  · exact power_le_power_right (natCast_le_aleph0.trans h)
  · rw [← power_mul, mul_eq_self h]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ (b ^ a) ^ a < (b ^ a) ^ (b ^ a).ord.cof

Tactic:
← power_mul,

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ b ^ (a * a) < (b ^ a) ^ (b ^ a).ord.cof