mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
⊢ ∀ (c : R), ∀ y ∈ span R (range (Subtype.val ∘ v)), c • x + y = 0 → c = 0

Tactic:
intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ↑s.ncard = ↑0 ↔ s = ∅

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.encard = ↑0 ↔ s = ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).encard = ↑s.ncard + 1

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).encard = s.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1

Tactic:
hs.cast_ncard_eq,

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ s.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ ↑(s \ {a}).ncard + 1 = ↑s.ncard

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ ↑(s \ {a}).ncard + 1 = s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < s.ncard

Tactic:
rw [← ncard_sdiff_singleton_add_one h hs]; apply lt_add_one

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ ↑s.ncard

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : ↑(f '' s).ncard = ↑s.ncard
hs : s.Finite
⊢ InjOn f s

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : ↑(f '' s).ncard = s.encard
hs : s.Finite
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = Fintype.card (Fin n)

Tactic:
← Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
himage : s = f' '' univ
⊢ s.ncard = Nat.card (Fin n)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
⊢ s.ncard ≤ t.ncard

Tactic:
have hle := encard_le_encard_of_injOn hf f_inj
  to_encard_tac; rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = s.encard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
by
  rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard = ↑s.ncard + ↑t.ncard

Tactic:
hs.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard = s.encard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + t.encard

Tactic:
hs.cast_ncard_eq,

Goal state after:
case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ ↑(s \ t).ncard + t.encard
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (comap ⇑f ⋯ (conGen rel)) a b
⊢ (conGen (rel on ⇑f)) a b

Tactic:
simp only [Con.comap_rel] at h

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
a b : M
h : (conGen rel) (f a) (f b)
⊢ (conGen (rel on ⇑f)) a b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
p' : Submodule R (M ⧸ p)
⊢ p ≤ comap p.mkQ p'

Tactic:
by
  simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a✝ : R
ha : a✝ ≠ 0
x✝¹ x✝ : R
hb : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
⊢ x✝¹ = x✝

Tactic:
by
    obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
    simpa [← mul_assoc, h.mul_comm, hx] using congr_arg (x * ·) hb

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
x : α
⊢ a < x ∧ x ≤ pred b ↔ a < x ∧ x < b

Tactic:
le_pred_iff_of_not_isMin hb

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
x : α
⊢ a < x ∧ x < b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ a ≤ x ∧ x ≤ pred b ↔ a ≤ x ∧ x < b

Tactic:
le_pred_iff_of_not_isMin hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ≤ pred b ↔ x < b

Tactic:
le_pred_iff_of_not_isMin hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x < b ↔ x < b
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
⊢ map (inl R M M₂) p = p.prod ⊥

Tactic:
ext ⟨x, y⟩
  simp only [and_left_comm, eq_comm, mem_map, Prod.mk_inj, inl_apply, mem_bot, exists_eq_left',
    mem_prod]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc_of_not_isMax hb a

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x < a, f x = ∏ x ≤ a, f x

Tactic:
mul_prod_Iio_eq_prod_Iic

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ ∏ x ≤ a, f x = ∏ x ≤ a, f x
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I = ⊥

Tactic:
rw [eq_bot_iff]

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I ≤ ⊥
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
⊢ J ∈ s → y✝ ∈ J

Tactic:
hJ

Goal state after:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
hJ : J ∈ s
⊢ y✝ ∈ J
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
x y : α
h : Associated x y
⊢ x ∈ I ↔ y ∈ I

Tactic:
obtain ⟨u, rfl⟩ := h.symm

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
y : α
u : αˣ
h : Associated (y * ↑u) y
⊢ y * ↑u ∈ I ↔ y ∈ I
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - y * z, y} = span {x, y}

Tactic:
rw [← span_pair_add_right_mul, sub_add_cancel]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
by
  have A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
      ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) := by
    rw [prod_range_succ, prod_range_succ']; simp
  rw [prod_range_succ']
  simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _

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.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
simp [comap_neBot_iff_frequently, hα]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal (⇑e '' s)
⊢ IsCofinal s

Tactic:
by simpa using e.symm.map_isCofinal hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
rw [← sub_pos, ← sub_smul]; exact smul_pos (sub_pos.2 ha) hb

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
  intro S₁ hS₁ S₂ hS₂
  exact finite_sup S₁ S₂

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}

Tactic:
intro β s _

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < univ.{u, v}
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

pp: case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c

Tactic:
· rwa [Ordinal.sub_eq_zero_iff_le.2 hab.le]

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ ∃ d < c, a < b + d

Tactic:
refine ⟨_, hc.succ_lt hd, ?_⟩

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + succ d
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
⊢ succ a < iSup f

Tactic:
by_contra! hoa

Goal state after:
ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
by
  rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]
  apply (lift_card_sInf_compl_le _).trans
  rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]
  exact mk_range_le_lift

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

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
| limit c l IH =>

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ type r

Tactic:
← ord_le_type,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ (#α).ord
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < type r

Tactic:
← ord_le_type,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < (#α).ord
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
j : Ordinal.{max u v}
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
exact (hf _ _ hj').trans (le_bsup _ _ _)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = o.bsup fun x x_1 ↦ f x

Tactic:
bsup_eq_blsub_of_lt_succ_limit h

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = o.blsub fun x x_1 ↦ f x

f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ a < o, f a < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : a * b ≠ 0
h : b = 0
⊢ False

Tactic:
by simp [h] at b0

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

Goal state before:
pp: case neg.limit
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ o' ≤ b ^ o'
⊢ a ^ c ≤ b ^ c

Tactic:
| limit c l IH =>

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

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c

Tactic:
by
  by_cases ha : a = 0
  · by_cases c = 0 <;> simp_all
  · induction c using limitRecOn with
    | zero => simp
    | add_one c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)

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

Goal state before:
pp: m n : ℕ
⊢ ↑(n * (m / n) + m % n) = ↑m

Tactic:
Nat.div_add_mod

Goal state after:
m n : ℕ
⊢ ↑m = ↑m
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
| limit c l IH =>

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

Goal state before:
pp: case inr.inr.inr.limit
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
| limit c l IH =>

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

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

Tactic:
opow_eq_zero

Goal state after:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
h : b = 0 ∧ c ≠ 0
⊢ c ≤ log b 0
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:
simp_rw [log_zero_right, zero_le]

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

Goal state before:
pp: case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ (u + log b v + 1)

Tactic:
hw,

Goal state after:
case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + b ^ u ≤ b ^ (u + log b v + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove (fixedPoints f)

Tactic:
convert! not_bddAbove_fp_family fun _ : Unit => H

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
exact nfp_monotone (isNormal_add_right a).monotone zero_le

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

Goal state before:
pp: a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
refine
    ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩

Goal state after:
a b : Ordinal.{u}
hb : b < a
c : Ordinal.{u}
hc : c < a
H : a ≤ b + c
hab : a - b = a
⊢ False
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preAleph o).ord = preOmega o

Tactic:
by
  rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

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

Goal state before:
pp: case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * (x + y)

Tactic:
rw [mul_add]

Goal state after:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * x + a * y
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

Tactic:
rcases le_or_gt o 2 with ho | ho

Goal state after:
case refine_1.inl
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a * o = o

case refine_1.inr
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : 2 < o
⊢ a * o = o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b

Tactic:
exact h.trans (le_max_left a b)

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

Goal state before:
pp: case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
⊢ IsCofinal (range fun i ↦ ⟨f i, ⋯⟩)

Tactic:
intro ⟨b, hb⟩

Goal state after:
case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb : b ∈ Iio (⨆ i, f i + 1)
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb⟩ ≤ y
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case e'_4.e'_6
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, (f i.toOrd).card = ⨆ a, (f a).card

Tactic:
· exact ToType.mk.symm.iSup_comp (g := fun x ↦ (f x).card)

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Tactic:
by
  apply (card_iSup_Iio_le_sum_card f).trans
  convert! ← sum_le_lift_mk_mul_iSup _
  · exact mk_toType o
  · exact ToType.mk.symm.iSup_comp (g := fun x ↦ (f x).card)

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

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬a ^ b = 0

Tactic:
opow_eq_zero

Goal state after:
case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ¬(a = 0 ∧ b ≠ 0)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = 2 ^ lift.{v, u} #ι

Tactic:
← lift_two_power

Goal state after:
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ False

Tactic:
apply mk_univ.not_lt

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑Set.univ < #?m.36

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.37
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #ι < c.ord.cof

Tactic:
· rwa [hc.cof_ord]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
⊢ f = g

Tactic:
ext a; rw [← (f a).xor_false, ← (g a).xor_false]; exact congr(($h ⟨a, false⟩).2)

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

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
rw [mk_list_eq_mk]
    apply le_max_right

Goal state after: