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

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

Tactic:
by
  rw [mul_comm, span_pair_sub_right_mul]

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

Goal state before:
pp: case zero
n : ℕ
⊢ ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
⊢ ∑ k ∈ range (0 + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ 0 * ↑(n.choose 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ ∑ m ∈ range (0 + 1), (-1) ^ m * ↑(Nat.choose 0 m) = if 0 = 0 then 1 else 0

Tactic:
| zero =>

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

Goal state before:
pp: case isUnit_or_isUnit.refine_1
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ span {a} = span {a * (c * d)}

Tactic:
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

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x

Tactic:
exact card_le_card hy

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
⊢ map f (f.iterateMapComap i 0 K) ≤ map i (f.iterateMapComap i 0 K)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero.zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
⊢ f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ f.iterateMapComap i 0 K = f.iterateMapComap i (0 + 1) K

Tactic:
| zero =>

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

Goal state before:
pp: case zero
d : ℕ
⊢ ∑ ij ∈ antidiagonal 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
⊢ 0 ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
by
  rw [mem_kernMap, compl_surjective.exists]
  refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)
  rw [kernImage_compl, compl_eq_comm, eq_comm]

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

Goal state before:
pp: α : Type u
S : Set (Set α)
f : Filter α
⊢ f ≤ generate S ↔ f ≤ ⨅ s ∈ S, 𝓟 s

Tactic:
by simp [le_generate_iff, le_principal_iff, subset_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter (α ⊕ β)
⊢ map inl (comap inl l) ⊔ map inr (comap inr l) = l

Tactic:
by
  rw [← comap_sumElim_eq, Sum.elim_inl_inr, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ⊥ = map m f ↔ f = ⊥

Tactic:
by rw [eq_comm, map_eq_bot_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
⊢ (map f F).NeBot ↔ F.NeBot

Tactic:
simp only [neBot_iff, Ne, map_eq_bot_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
← hs,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ (u.seq v).seq t ∈ h.seq (g.seq x)
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
this : Mul α := e.mul
⊢ IsRightCancelMul α

Tactic:
exact e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid O
e : N ≃ O
inst✝ : MulDistribMulAction M O
this : Monoid N := e.monoid
⊢ ∀ (r : M), r • 1 = 1

Tactic:
by simp [one_def, smul_def, smul_one]

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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
⊢ True → f '' Ici a ∈ atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k a : ℕ
h : k ≤ a
⊢ a ≤ a - k + k

Tactic:
by rw [Nat.sub_add_cancel h]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ x✝¹ • f x✝ = 0

Tactic:
← hs,

Goal state after:
R : Type u_4
M : Type u_5
N : Type u_6
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ f (x✝¹ • x✝) = 0
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
dsimp at hm
    rw [← sub_eq_zero, ← smul_sub] at hm
    simpa [hr.ne_zero, sub_eq_zero] using eq_zero_or_eq_zero_of_smul_eq_zero hm

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✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ a • b < 0 ↔ b < 0

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₂ := (0 : β))

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
⊢ IsCofinal t

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
⊢ ∃ y ∈ t, a ≤ y
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
⊢ IsCofinal (f '' s)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
⊢ ∃ y ∈ f '' s, a ≤ y
Module: Mathlib.Order.Cofinal

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

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ ℵ₀ ≤ cof α ↔ 1 < cof α

Tactic:
simp [← not_lt]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s

Tactic:
by
  simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter]
  grind

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ ⊤.FG

Tactic:
← Module.finite_def

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ Module.Finite S P
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∪ t)

Tactic:
by
  rw [← dirSupClosedOn_compl, compl_union]; exact hs.compl.inter ht.compl

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝ : Nonempty β
this : OrderBot β := WellFoundedLT.toOrderBot β
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
let := WellFoundedLT.conditionallyCompleteLinearOrderBot α

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝¹ : Nonempty β
this✝ : OrderBot β := WellFoundedLT.toOrderBot β
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this✝ : Nonempty α
this : OrderBot α := WellFoundedLT.toOrderBot α
⊢ a ∈ range f

Tactic:
let := WellFoundedLT.conditionallyCompleteLinearOrderBot α

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
lift_univ,

Goal state after:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u} c < univ.{u, max (u + 1) v}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α.ToType ≤i β.ToType

Tactic:
apply Classical.choice (type_le_iff.mp _)
  rwa [type_toType, type_toType]

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

Goal state before:
pp: case refine_4
α : Type u
β✝ : Type v
γ : Type w
r✝ : α → α → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a : Ordinal.{u}
β : Type u
s : β → β → Prop
wo : IsWellOrder β s
g : s ≺i r
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone (fun a ↦ type (Subrel r fun x ↦ r x a)) ⋯)

Tactic:
exact ⟨_, g.subrelIso.ordinalType_congr⟩

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ ¬r ((enum r) o₁) ((enum r) o₂) ↔ o₂ ≤ o₁

Tactic:
enum_lt_enum (r := r),

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ ¬o₁ < o₂ ↔ o₂ ≤ o₁
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝ : Nonempty α
this : OrderBot α := WellFoundedLT.toOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b

Tactic:
let := WellFoundedLT.conditionallyCompleteLinearOrderBot α

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ (sSup (range fun i ↦ f i)).ord = sSup (range fun i ↦ (f i).ord)

Tactic:
sSup_ord,

Goal state after:
ι : Sort u_3
f : ι → Cardinal.{u_4}
⊢ sSup (ord '' range fun i ↦ f i) = sSup (range fun i ↦ (f i).ord)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : 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 : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
intro a

Goal state after:
α β : 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 : β), Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
⊢ enumOrd t ≤ enumOrd s

Tactic:
intro a

Goal state after:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ enumOrd t a ≤ enumOrd s a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
n : ℕ
hn : n ≠ 0
b : ℕ
hb : 1 < b
hfuel : n < b ^ 0
⊢ (go n b 0).fst = n / b ^ (go n b 0).snd ∧ b ^ (go n b 0).snd ≤ n ∧ n < b ^ ((go n b 0).snd + 1)

Tactic:
| zero =>

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
⊢ ⨅ r, type ↑r = ⨅ r, type ↑r

Tactic:
refine congr_arg sInf <| ext fun o ↦ ⟨?_, ?_⟩ <;>
    rintro ⟨⟨r, hr⟩, rfl⟩ <;>
    refine ⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩

Goal state after:
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ β ≃ α

case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ α ≃ β
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case zero
⊢ ↑0 ≤ (↑0).ord

Tactic:
| zero =>

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

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

Tactic:
intro a

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

Goal state before:
pp: case zero
a b : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (0 + 1) = a * (0 + 1) + b

Tactic:
| zero =>

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o * 2 = o + o

Tactic:
← one_add_one_eq_two,

Goal state after:
o : Ordinal.{u_4}
⊢ o * (1 + 1) = o + o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
⊢ log b y < x

Tactic:
rcases eq_or_ne y 0 with rfl | hy
  · grind [log_zero_right]
  · exact log_lt_of_lt_pow hy hlt

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

Goal state before:
pp: case zero
⊢ 1 ^ 0 = 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
a : Ordinal.{u_1}
⊢ a ^ ↑0 = a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
b n : ℕ
⊢ log b (n / b ^ 0) = log b n - 0

Tactic:
| zero =>

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

Goal state before:
pp: case neg.zero
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑(n + (m - n)) = ↑n + (↑m - ↑n)

Tactic:
add_tsub_cancel_of_le h,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑m = ↑n + (↑m - ↑n)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
n : ℕ
hn : 1 < n
b : ℕ
hb : 1 < b
hfuel : n < b ^ 0
⊢ (go n b 0).fst = b ^ ((go n b 0).snd + 1) / n ∧ b ^ (go n b 0).snd < n ∧ n ≤ b ^ ((go n b 0).snd + 1)

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case inr.inr.inr.zero
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case inr.zero
b : ℕ
hb : 1 < b
⊢ log b 0 ≤ clog b 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
⊢ f i (derivFamily f 0) = derivFamily f 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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
⊢ a ≤ derivFamily f 0 → ∃ o, derivFamily f o = a

Tactic:
| zero =>

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

Goal state before:
pp: case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ (op a)^[0] a < o

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsPrincipal op (nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o)

Tactic:
intro a

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄,
    a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o →
      b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o → op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ (n + 1)

Tactic:
by simp [pow_succ, natCast_pow m n]

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

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

Tactic:
by
  rw [IsInitial, card_nat, ord_natCast]

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

Goal state before:
pp: case zero
⊢ preOmega ↑0 = ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
⊢ a * ↑0 < o

Tactic:
| zero =>

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ ∀ b < ω ^ o, b + b < ω ^ o

Tactic:
intro a

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
⊢ a < ω ^ o → a + a < ω ^ o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

Tactic:
constructor
  · rw [or_iff_not_imp_left]
    refine fun H ho ↦ ⟨log ω o, (opow_log_le_self ω ho).eq_of_not_lt ?_⟩
    obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)
    exact fun h ↦ hn.not_gt <| H.mul_natCast_lt h n
  · rintro (rfl | ⟨a, rfl⟩)
    exacts [isPrincipal_zero, isPrincipal_add_omega0_opow a]

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

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

Tactic:
card_nat

Goal state after:
n : ℕ
⊢ ↑n = ↑n