mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = max (toZ i0 (succ^[n] i0)) 0

Tactic:
toZ_of_ge (le_succ_iterate _ _),

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ ↑(Nat.find ⋯) = max (↑(Nat.find ⋯)) 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n

Tactic:
if_pos hn

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some (succ^[n.toNat] hι.some) = n
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b + 0 = 0
⊢ a * b = 0

Tactic:
add_zero,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
this : a * a * b = 0
⊢ a * b = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + 0 + y ^ (n + 1)

Tactic:
add_zero,

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y ^ (n + 1)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), n.choose m = 2 ^ n

Tactic:
by
  have := (add_pow 1 1 n).symm
  simpa [one_add_one_eq_two] using this

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (x✝ ∈ pi fun x ↦ span {r x}) ↔ x✝ ∈ span {r}

Tactic:
simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ ∀ (x y : R ⧸ I),
    (↑(Submodule.quotEquivOfEq I J h)).toFun (x * y) =
      (↑(Submodule.quotEquivOfEq I J h)).toFun x * (↑(Submodule.quotEquivOfEq I J h)).toFun y

Tactic:
rintro ⟨x⟩ ⟨y⟩

Goal state after:
case mk.mk
R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ I
x : R
y✝ : R ⧸ I
y : R
⊢ (↑(Submodule.quotEquivOfEq I J h)).toFun
      (Quot.mk (⇑(Submodule.quotientRel I)) x * Quot.mk (⇑(Submodule.quotientRel I)) y) =
    (↑(Submodule.quotEquivOfEq I J h)).toFun (Quot.mk (⇑(Submodule.quotientRel I)) x) *
      (↑(Submodule.quotEquivOfEq I J h)).toFun (Quot.mk (⇑(Submodule.quotientRel I)) y)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1 + (c - (n + 1))) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0

Tactic:
add_zero,

Goal state after:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1 + (c - (n + 1))) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)

Tactic:
choose_symm (this _ hi)

Goal state after:
case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose i
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x ↦ x ^ t.attach.sup fun x ↦ n ⟨↑x, ⋯⟩) x ∈ ↑(span (range fun x ↦ ↑x ^ n x))

Tactic:
← Nat.sub_add_cancel (Finset.le_sup <| t.mem_attach ⟨x, hxt⟩)

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x_1 ↦ x_1 ^ ((t.attach.sup fun x ↦ n ⟨↑x, ⋯⟩) - n ⟨↑⟨x, hxt⟩, ⋯⟩ + n ⟨↑⟨x, hxt⟩, ⋯⟩)) x ∈
    ↑(span (range fun x ↦ ↑x ^ n x))
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
h_bot : I ≠ ⊥
h_top : I ≠ ⊤
⊢ ¬IsField R

Tactic:
contrapose h_bot

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
h_top : I ≠ ⊤
h_bot : IsField R
⊢ I = ⊥
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
induction n using Nat.strong_induction_on with | h n ih =>
  intro x y s _ hn eq
  rw [← x.single_add_erase 0, ← y.single_add_erase 0]
  simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq]
  congr 2
  by_contra ne
  apply ne (ih _ _ _ rfl (inj _))
  · contrapose! ne; simp_all [-comapDomain_support]
  · simp +contextual [hn, s, ← Nat.succ_le_iff, Finset.le_max']
  simp_rw [← snd_prodOfFinsuppNat, eq]

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

Goal state before:
pp: case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V

Tactic:
exact subset_inter_iff.mp W_sub

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ t ∈ l'

Tactic:
hl'.mem_iff

Goal state after:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ s i ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map ψ (map φ F) = map ρ (map θ F)

Tactic:
by
  rw [Filter.map_map, H, ← Filter.map_map]

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
⊢ ⋃ x ∈ s, Ici x = Ici a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
  · exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ m '' S ∈ map m (comap m f) ↔ m '' S ∈ f

Tactic:
map_comap_of_mem large

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ m '' S ∈ f ↔ m '' S ∈ f
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
t u : Set α
⊢ u ∈ l ⊔ 𝓟 t ↔ ∃ i, p i ∧ s i ∪ t ⊆ u

Tactic:
by
    simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, and_true,
      Unique.exists_iff]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
simp [comap_neBot_iff_frequently, *]

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

Goal state before:
pp: case inr
ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
H : Nonempty ((j : ι) → α j)
this : ∀ (j : ι), Nonempty (α j)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, *]

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

Goal state before:
pp: α : Type u
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ f.NeBot

Tactic:
simp [frequently_iff_neBot]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
⊢ f ⁻¹' U ⊆ V → x ∈ V

Tactic:
f_U_V

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
V : Set α
U : Set β
U_in : U ∈ F
f_U_V : f ⁻¹' U ⊆ V
⊢ x ∈ V
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
by
  refine map_inf_le.antisymm ?_
  rintro t ⟨s₁, hs₁, s₂, hs₂, ht : m ⁻¹' t = s₁ ∩ s₂⟩
  refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_
  rw [← image_inter h, image_subset_iff, ht]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LE β
l : Filter α
f f' g g' : α → β
H✝ : f ≤ᶠ[l] g
hf✝ : f =ᶠ[l] f'
hg✝ : g =ᶠ[l] g'
x : α
hf : f x = f' x
hg : g x = g' x
H : f x ≤ g x
⊢ f' x ≤ g' x

Tactic:
by rwa [hf, hg] at H

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False

Tactic:
· obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
    rw [f.apply_covBy_apply_iff] at hb
    exact h _ hb

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ x, IsTop x

Tactic:
by
  rw [le_iff_lt_or_eq, Cardinal.lt_one_iff, cof_eq_one_iff]
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
exact (smul_le_smul_of_nonneg_right ha h₁.le).trans_lt (smul_lt_smul_of_pos_left hb h₂)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
this : ∀ (s : ↥S), ∃ n, ↑s ∈ N n
⊢ ∃ n, M' = N n

Tactic:
choose f hf using this

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ ∃ n, M' = N n
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₂ • -_b < a₁ • -_b
⊢ a₁ < a₂

Tactic:
exact lt_of_smul_lt_smul_right (β := β) h <| neg_nonneg.2 hb

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ DirSupInacc (⋃ i, f i)

Tactic:
rw [← sUnion_range f]
  exact DirSupInacc.sUnion (by simpa)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : y < sSup (f ⁻¹' Iic x)
⊢ y ∈ f ⁻¹' Iic x

Tactic:
rw [lt_csSup_iff h₂ h₁] at hy

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : ∃ b ∈ f ⁻¹' Iic x, y < b
⊢ y ∈ f ⁻¹' Iic x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ typeLT α ≤ type fun x1 x2 ↦ x1 < x2

Tactic:
← ord_cardinalMk,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ (#α).ord ≤ type fun x1 x2 ↦ x1 < x2
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ r ≺i fun x1 x2 ↦ x1 < x2

Tactic:
refine ⟨RelEmbedding.ofMonotone _ fun a b ha ↦
    ((PrincipalSeg.ofElement r a).codRestrict _ ?_ ?_).ordinal_type_lt, type r, fun a ↦ ⟨?_, ?_⟩⟩
  · rintro ⟨c, hc⟩
    exact trans hc ha
  · exact ha
  · rintro ⟨b, rfl⟩
    exact (PrincipalSeg.ofElement _ _).ordinal_type_lt
  · refine inductionOn a ?_
    rintro β s wo ⟨g⟩
    exact ⟨_, g.subrelIso.ordinalType_congr⟩

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

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s

Tactic:
apply (RelEmbedding.ofMonotone (Sum.recOn · f fun _ ↦ f.top) ?_).ordinal_type_le

Goal state after:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r emptyRelation a b →
      s (Sum.recOn a ⇑f.toRelEmbedding fun x ↦ f.top) (Sum.recOn b ⇑f.toRelEmbedding fun x ↦ f.top)
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
ciSup_unique,

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

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + c

Tactic:
e,

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + a * d
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

Tactic:
simpa only [mul_one, opow_succ] using fun b ↦ mul_lt_mul_of_pos_left h (opow_pos b ha)

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

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n

Tactic:
intro m

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ m ≤ n.log2 ↔ m ≤ log 2 n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ a < o

Tactic:
e,

Goal state after:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ ↑n < o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

Tactic:
rw [derivFamily_succ, ← succ_le_iff]

Goal state after:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ nfp f a

pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ n, f^[n] a

Tactic:
· rw [Ordinal.iSup_le_iff]
    intro n
    rw [← List.length_replicate (n := n) (a := Unit.unit), ← List.foldr_const f a]
    exact Ordinal.le_iSup _ _

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 ≤ nfp (fun x ↦ a * x) b

Tactic:
exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord.IsInitial

Tactic:
IsInitial,

Goal state after:
c : Cardinal.{u_1}
⊢ c.ord.card.ord = c.ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ (↑n).IsInitial

Tactic:
IsInitial,

Goal state after:
n : ℕ
⊢ (↑n).card.ord = ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ω.IsInitial

Tactic:
IsInitial,

Goal state after:
⊢ ω.card.ord = ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preOmega (ω + 0) = ω

Tactic:
add_zero,

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

Goal state before:
pp: case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0

Tactic:
rwa [← pos_iff_ne_zero]

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

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b + 0 < a ^ ω * d
⊢ succ b ≤ d

Tactic:
add_zero,

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b < a ^ ω * d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preAleph (ω + 0) = ℵ₀

Tactic:
add_zero,

Goal state after:
⊢ preAleph ω = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ preBeth ω ≤ ℵ₀

Tactic:
rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]

Goal state after:
case a
⊢ ∀ (i : ↑(Iio ω)), preBeth ↑i ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
⊢ Small.{u, u + 2} ↑(Iio (typeLT ↑s))

Tactic:
refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_

Goal state after:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
x✝ : ↑(Iio (typeLT ↑s))
⊢ ∀ ⦃a₂ : ↑(Iio (typeLT ↑s))⦄, (fun x ↦ ⟨↑(f x), ⋯⟩) x✝ = (fun x ↦ ⟨↑(f x), ⋯⟩) a₂ → x✝ = a₂
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

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

Tactic:
apply hc.trans_lt

Goal state after:
case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
b : Ordinal.{u_1}
hb : b < o
c : ↑(Iio a)
hc : b ≤ ↑(f c)
⊢ ↑(f c) < ⨆ i, ↑(f i) + 1
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb⟩ ≤ y

Tactic:
rw [mem_Iio, hg.lt_iff_exists_lt ho] at hb

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb✝ : b ∈ Iio (g o)
hb : ∃ a' < o, b < g a'
⊢ ∃ y ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩, ⟨b, hb✝⟩ ≤ y
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof

Tactic:
rwa [Cardinal.lift_umax, c.lift_id']

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (Cardinal.lift.{u, max u v} c).ord.cof

Tactic:
rwa [Cardinal.lift_umax, c.lift_id']

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

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (type r)

Tactic:
← hr

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (#α).ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(range f) ≤ #β

Tactic:
apply mk_range_le

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

Goal state before:
pp: ⊢ preAleph Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.preAleph_ord

Goal state after: