mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case refine_1
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

Tactic:
have : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
    exact zero_ne_one

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ Irreducible a

Tactic:
constructor
  · intro ha
    apply max.ne_top
    rw [span_singleton_eq_top.2 ha]
  · intro u v ha
    by_contra! huv
    have hu : span {u} ≤ span {a} :=
      (max.eq_of_le (span_singleton_ne_top huv.1)
        (span_singleton_le_span_singleton.2 ((dvd_mul_right u v).trans ha.symm.dvd))).ge
    have hv : span {v} ≤ span {a} :=
      (max.eq_of_le (span_singleton_ne_top huv.2)
        (span_singleton_le_span_singleton.2 ((dvd_mul_left v u).trans ha.symm.dvd))).ge
    rw [span_singleton_le_span_singleton] at hu hv
    obtain ⟨c, rfl⟩ := hu
    obtain ⟨d, rfl⟩ := hv
    refine idem (a * (c * d)) ?_ ?_
    · apply le_antisymm <;> rw [span_singleton_le_span_singleton]
      · exact (dvd_mul_right (a * (c * d)) a).trans (ha.trans (by ring)).symm.dvd
      · apply dvd_mul_right
    · rw [isIdempotentElem_iff]
      refine Eq.trans ?_ (congrArg (· * (c * d)) ha.symm)
      ring

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: 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
x : ℕ →₀ P
⊢ ∑ c ∈ x.support, ((((inr R P M ∘ₗ f) ^ c) ∘ₗ inl R P M) (x c)).2 =
    f
      (∑ x_1 ∈ ((comapDomain.addMonoidHom ⋯) x).support,
        (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (((comapDomain.addMonoidHom ⋯) x) x_1))

Tactic:
← Finset.sum_preimage (· + 1) _ (add_left_injective 1).injOn _ (by simp_all)

Goal state after:
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
x : ℕ →₀ P
⊢ ∑ x_1 ∈ x.support.preimage (fun x ↦ x + 1) ⋯, ((((inr R P M ∘ₗ f) ^ (x_1 + 1)) ∘ₗ inl R P M) (x (x_1 + 1))).2 =
    f
      (∑ x_1 ∈ ((comapDomain.addMonoidHom ⋯) x).support,
        (((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (((comapDomain.addMonoidHom ⋯) x) x_1))
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f (∑ a, Finsupp.single a (s a))) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
Finsupp.mapDomain_finsetSum

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (∑ i, mapDomain f (Finsupp.single i (s i))) y = ∑ x with f x = y, equivFunOnFinite s x
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x y : α
hy : y ∈ s
hy' : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨y, hy, hy'.le⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap id F = F

Tactic:
comap_id

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ F = F
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ioi i

Tactic:
exact mem_biUnion hys hyx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ range m

Tactic:
simp only [comap_neBot_iff, frequently_iff, mem_range, @and_comm (_ ∈ _), exists_exists_eq_and]

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

Goal state before:
pp: case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Tactic:
· refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)
    exact Iic_disjoint_Ici.2 hle

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap id f ≤ f

Tactic:
comap_id

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ f ≤ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ comap id l = l

Tactic:
comap_id

Goal state after:
α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ l = l
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x) x
⊢ False

Tactic:
by
    simpa only [and_not_self_iff, exists_false] using H hp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
sa : Set α
h : lb.HasBasis pb sb
⊢ (𝓟 sa ×ˢ lb).HasBasis pb fun x ↦ sa ×ˢ sb x

Tactic:
by
  simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.snd).principal_inf _

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (F ⊓ map u atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U

Tactic:
inf_neBot_iff_frequently_left,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∃ᶠ (x : β) in map u atTop, p x) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG

Tactic:
refine ⟨fun ⟨hn⟩ => fun s hs =>
    have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
    Submodule.map_comap_eq_self this ▸ (hn _).map _,
    fun h => ⟨fun s => ?_⟩⟩
  specialize h (s.map N.subtype) (Submodule.map_subtype_le N s)
  exact Submodule.fg_of_fg_map_injective N.subtype Subtype.val_injective h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 • b < a • b

Tactic:
rwa [zero_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0 • b

Tactic:
rwa [zero_smul]

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
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite
span_t : span R t = N
⊢ span S (⇑f '' t) = Submodule.map f N

Tactic:
span_image,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite
span_t : span R t = N
⊢ Submodule.map f (span R t) = Submodule.map f N
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ Module.Finite R ↥(s.sup S)

Tactic:
refine s.sup_induction (f := S) (p := fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_
    inferInstance

Goal state after:
R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ ∀ (a₁ : Submodule R V), Module.Finite R ↥a₁ → ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(a₁ ⊔ a₂)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
by
  unfold iSup
  convert! map_sSup hf (range_nonempty g) hg
  ext
  simp

Goal state after:
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:
by
  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.Arithmetic

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

Tactic:
· simpa [sub_eq_zero_of_lt h] using h.le

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
⊢ ↑((enum s hs) ⊥) = sInf s

Tactic:
let : Bot s := ⟨⟨sInf s, csInf_mem hs.nonempty⟩⟩

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

Goal state before:
pp: α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ (o.brange fun x x_1 ↦ c) = {c}

Tactic:
by
  rw [← range_familyOfBFamily]
  exact @Set.range_const _ o.ToType (nonempty_toType_iff.2 ho) c

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

Goal state before:
pp: ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)

Tactic:
by convert! Set.image_mono h <;> apply Set.range_comp

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

Goal state before:
pp: case succ
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
cases Nat.lt_or_ge n b with
    | inl hnb =>
      simp [go, hnb, one_le_iff_ne_zero, hn]
    | inr hnb =>
      rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
      simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
      split <;> simp_all

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c

Tactic:
rw [← card_ord c]; exact Ordinal.card_le_card ho

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

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
rw [card_le_iff, ← lift_succ, ← lift_ord] at h
  exact mem_range_lift_of_le h.le

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

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y

Tactic:
refine (le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h

Goal state after:
b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
hb : b ≤ 1
⊢ b ^ x ≤ y
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m < (m / n).succ * n

Tactic:
← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < (m / n).succ
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case cons
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
H : ∀ (i : ι), Monotone (f i)
b : Ordinal.{u}
h : ∀ (i : ι), f i b ≤ b
i : ι
l : List ι
IH : ∀ {a : Ordinal.{u}}, a ≤ b → List.foldr f a l ≤ b
a : Ordinal.{u}
ab : a ≤ b
⊢ List.foldr f a (i :: l) ≤ b

Tactic:
| cons i l IH =>

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
rwa [← ord_aleph0, ord_le_ord]

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ ∀ (i : List ι), List.foldr f a i ≤ a

Tactic:
intro l

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o

Tactic:
obtain hab | hba := le_or_gt a b

Goal state after:
case mpr.inl
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right.refine_1
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (a : Ordinal.{u}), derivFamily f a ∈ ⋂ i, fixedPoints (f i)

pp: case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
· rintro a S ⟨i, hi⟩
    rw [← hi]
    exact derivFamily_fp (H i) a

Goal state after:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : List Unit), List.foldr (fun x ↦ f) a i ≤ ⨆ n, f^[n] a

Tactic:
intro l

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x ↦ f) a l ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * (↑1 + ↑n) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
Nat.cast_one,

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * (1 + ↑n) + a % ω ^ log ω a - ω ^ log ω a < a
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] a < nfp f a

Tactic:
apply (hf.iterate n h).trans_le

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n] (f a) ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
· intro ⟨a, ha, ⟨n, hn⟩⟩
    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
    · simp [mul_lt_mul_iff_right₀, opow_pos]
    · simpa

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a * x) 0 ≤ 0

Tactic:
nfp_le_iff

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x ↦ a * x)^[n] 0 ≤ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

Tactic:
rw [dvd_iff_mod_eq_zero]

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) a
⊢ False

Tactic:
rcases exists_lt_add_of_not_isPrincipal_add ha with ⟨b, hb, c, hc, rfl⟩

Goal state after:
b c : Ordinal.{u}
H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False
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]

Goal state after:
case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ (c * b))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof

Tactic:
cases o using inductionOnWellOrder with

Goal state after:
case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (typeLT α).cof = (lift.{v, u} (typeLT α)).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 1 ↔ o ∈ range succ

Tactic:
cases o using inductionOnWellOrder with

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c

Tactic:
refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_

Goal state after:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ x * ω < ω ^ c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c

Tactic:
rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
  · exact (lt_irrefl _).elim c0
  · rw [opow_succ] at ha
    obtain ⟨n, hn, an⟩ :=
      ((isNormal_mul_right <| opow_pos _ omega0_pos).lt_iff_exists_lt isSuccLimit_omega0).1 ha
    grw [an, opow_succ, mul_assoc]
    gcongr
    exacts [opow_pos _ omega0_pos, isPrincipal_mul_omega0 hn hb]
  · rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩
    refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
    rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
    exact l.succ_lt hx

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

Goal state before:
pp: case refine_1.inr.inl
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) 0
ho₂ : 2 < 0
⊢ 0 ≤ 2 ∨ 0 ∈ Set.range fun x ↦ ω ^ ω ^ x

pp: case refine_1.inr.inr
a : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) a)
ho₂ : 2 < (fun x ↦ ω ^ x) a
⊢ (fun x ↦ ω ^ x) a ≤ 2 ∨ (fun x ↦ ω ^ x) a ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
· exact (not_lt_zero ho₂).elim

Goal state after:
case refine_1.inr.inr
a : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) a)
ho₂ : 2 < (fun x ↦ ω ^ x) a
⊢ (fun x ↦ ω ^ x) a ≤ 2 ∨ (fun x ↦ ω ^ x) a ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ (f a).cof = a.cof

Tactic:
rw [hf.apply_of_isSuccLimit ha, cof_iSup_Iio _ ha.isSuccPrelimit]
  exact hf.strictMono.comp <| Subtype.strictMono_coe _

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o.cof.ord ≤ a

Tactic:
rw [← hf.iSup_add_one_eq, cof_iSup_Iio_add_one hf.strictMono]

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ a.cof.ord ≤ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
exact csInf_mem (cof_lsub_def_nonempty o)

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

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
⊢ a < μ → (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) μ

Tactic:
hlt

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) μ
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

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

pp: case inr
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : ℵ₀ ≤ #α
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Tactic:
· exact infinite_pigeonhole_card f ℵ₀ (aleph0_le_mk β) le_rfl
      (by rwa [isRegular_aleph0.cof_ord])

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

Goal state before:
pp: case mk
α : Type u
inst✝ : Infinite α
β : Type u
⊢ #{ t // #↑t ≤ #β } ≤ (#α + 1) ^ #β

Tactic:
fapply mk_le_of_surjective

Goal state after:
case mk.f
α : Type u
inst✝ : Infinite α
β : Type u
⊢ (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t // #↑t ≤ #β }

case mk.hf
α : Type u
inst✝ : Infinite α
β : Type u
⊢ Surjective ?mk.f