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

Goal state before:
pp: case neg
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
c : ℕ
a✝ : c ∈ Finset.range (k + 1)
h : ¬m ≤ c
⊢ a ^ c * b ^ (k - c) ∈ I

Tactic:
refine I.mul_mem_left _ (I.pow_mem_of_pow_mem hb ?_)
    lia

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

Goal state before:
pp: case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ 1 ∈ J

Tactic:
rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]

Goal state after:
case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ x * y - (x * y - 1) ∈ J
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 0 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = 0

Tactic:
exact congr_arg _ (zero_smul _ _)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (x y : (ι → R) ⧸ pi fun x ↦ I),
    Quotient.liftOn' (x + y) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
      Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯ + Quotient.liftOn' y (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
rintro ⟨_⟩ ⟨_⟩; rfl

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (m : R ⧸ I) (x : (ι → R) ⧸ pi fun x ↦ I),
    Quotient.liftOn' (m • x) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
      (RingHom.id (R ⧸ I)) m • Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
rintro ⟨_⟩ ⟨_⟩; rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, (∃ i_1, p i_1 ∧ s i_1 = i) ∧ id i ⊆ x✝

Tactic:
simp [h.mem_iff]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ pure a ≤ 𝓟 s ↔ a ∈ s

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ atTop = generate (range Ici)

Tactic:
simp only [generate_eq_biInf, atTop, iInf_range]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha

Goal state after:
case inl
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ ∀ {x y : Set β}, x ∈ kernImage m '' f.sets → x ⊆ y → y ∈ kernImage m '' f.sets

Tactic:
rintro _ t ⟨s, hs, rfl⟩ hst
    refine ⟨s ∪ m ⁻¹' t, mem_of_superset hs subset_union_left, ?_⟩
    rw [kernImage_union_preimage, union_eq_right.mpr hst]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝ : Nonempty α
s : Set α
hs : s ∈ ⊤
⊢ univ.Nonempty

Tactic:
← nonempty_iff_univ_nonempty

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝ : Nonempty α
s : Set α
hs : s ∈ ⊤
⊢ Nonempty α
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
⊢ comap m (g ⊓ 𝓟 (range m)) = comap m g

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Tactic:
disjoint_comm,

Goal state after:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f
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:
← comap_sumElim_eq,

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

Goal state before:
pp: α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
s : Set α
⊢ sᶜ ∈ comk p he hmono hunion ↔ p s

Tactic:
by
  simp

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
e : α ≃ β
inst✝ : MulAction M β
⊢ ∀ (b : α), 1 • b = b

Tactic:
simp [smul_def]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
by
  rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]

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

Goal state before:
pp: k : ℕ
hk : 0 < k
a b : ℕ
x✝ : 1 ≤ b
⊢ a / k ≤ b ↔ a ≤ k * b + (k - 1)

Tactic:
Nat.div_le_iff_le_mul_add_pred hk

Goal state after:
k : ℕ
hk : 0 < k
a b : ℕ
x✝ : 1 ≤ b
⊢ a ≤ k * b + (k - 1) ↔ a ≤ k * b + (k - 1)
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
refine ⟨s', hs's, ?_⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ span R s = span R ↑s'
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : m ≤ l
⊢ (f ^ l).ker ≤ (f ^ m).ker

pp: case inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : l < m
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
· rw [← hn _ (hm.trans h), hn _ hm]

Goal state after:
case inr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : l < m
⊢ (f ^ l).ker ≤ (f ^ m).ker
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : OrderTop α
⊢ IsCofinal {⊤}

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ⋃ i ∈ s, Iio i = univ

Tactic:
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (x : α), ∃ i ∈ s, x ∈ Iio i
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✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ 0 < a • b ↔ 0 < a

Tactic:
simpa only [zero_smul] using smul_lt_smul_iff_of_pos_right hb (a₁ := 0) (a₂ := a)

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

Goal state before:
pp: R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
inst✝³ : CommSemiring R
inst✝² : Algebra R A
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
hS : S.FG
h : Surjective ⇑(algebraMap R A)
⊢ (restrictScalars R S).FG

Tactic:
by
  obtain ⟨s, rfl⟩ := hS
  exact ⟨s, .symm <| restrictScalars_span R A h _⟩

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

Goal state before:
pp: α : Type u
inst✝² : LinearOrder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ ℵ₀ ≤ cof α

Tactic:
by
  simp

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
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
⊢ ∃ S_1, S_1.Finite ∧ span S S_1 = ⊤

Tactic:
refine ⟨f '' s, hsfin.image f, eq_top_iff.mpr fun p _ ↦ ?_⟩

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
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ p ∈ span S (⇑f '' s)
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
hf' : (f ⁻¹' s).Nonempty
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' ha : IsLUB s (f (sSup (f ⁻¹' s)))
⊢ f (sSup (f ⁻¹' s)) ∈ range f

Tactic:
exact mem_range_self _

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

Goal state before:
pp: ⊢ liftPrincipalSeg.top = typeLT Ordinal.{u}

Tactic:
by
  simp

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

Goal state before:
pp: a : Ordinal.{v}
⊢ lift.{u, v} (a + 1) = lift.{u, v} a + 1

Tactic:
by
  simp

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
by
  simp

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

Goal state before:
pp: ⊢ cof Ordinal.{u} = Cardinal.univ.{u, u + 1}

Tactic:
by
  simp

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ ⨆ i, f i + 1 ≤ a ↔ ∀ (i : ι), f i < a

Tactic:
by
  simp

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ a < ⨆ i, f i + 1 ↔ ∃ i, a ≤ f i

Tactic:
by
  simp

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≺i s)
f : r ≺i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
      (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (o + 1).card = o.card + 1

Tactic:
by
  simp

Goal state after:
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 : β
this : type r * succ ((typein s).toRelEmbedding b) ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
mul_succ

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 : β
this : type r * (typein s).toRelEmbedding b + type r ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (succ o).card = o.card + 1

Tactic:
by
  simp

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

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)

Tactic:
refine isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩

Goal state after:
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ enumOrd s o ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a ∈ Iio (typeLT α)

Tactic:
rw [mem_Iio, ← ha, lt_succ_iff]

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

Goal state before:
pp: o : Ordinal.{u_1}
x y : o.ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding y ↔ x ≤ y

Tactic:
by
  simp

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

Goal state before:
pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)

Tactic:
mul_succ

Goal state after:
case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: 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
⊢ β ≃ α

pp: 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
⊢ α ≃ β

Tactic:
exacts [f.symm, f]

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

Goal state before:
pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)

Tactic:
exact isSuccLimit_add _ l

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

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * succ c' ≤ a * c

Tactic:
IH _ h,

Goal state after:
a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ a * succ c' + b ≤ a * c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
by
  rcases le_total m n with h | h
  · rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]
  · rw [← add_left_cancel_iff (a := ↑n), ← Nat.cast_add, add_tsub_cancel_of_le h,
      Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)]

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

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

Tactic:
simpa using hb.pos

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b

Tactic:
rw [← lt_mul_iff_div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
⊢ b ∈ s → y < b → ∃ b ∈ s, op x y < b

Tactic:
hbs

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
⊢ y < b → ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m : ℕ
⊢ ∀ (n : ℕ), ↑(m ^ n) = ↑m ^ ↑n

Tactic:
by
  simp

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b

Tactic:
obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h

Goal state after:
case refine_1
a b : Ordinal.{u_1}
h : a + b = b
c : Ordinal.{u_1}
hc : deriv (fun x ↦ a + x) c = b
⊢ deriv (fun x ↦ a + x) 0 ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
refine ⟨fun hab => ?_, fun h => ?_⟩

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

case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * succ b

Tactic:
mul_succ

Goal state after:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
ho : 0 ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 0

pp: case inr.inl
ho : 1 ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 1

pp: case inr.inr
ho : 2 ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 2

Tactic:
exacts [isPrincipal_zero, isPrincipal_mul_one, isPrincipal_mul_two]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ * ℵ_ o = ℵ_ o

Tactic:
by
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ o * ℵ₀ = ℵ_ o

Tactic:
by
  simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ (o + 1) = succ (ℵ_ o)

Tactic:
by
  simp

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

Goal state before:
pp: x o : Ordinal.{u_1}
⊢ x < ω_ o ↔ x.card < ℵ_ o

Tactic:
rw [← (isInitial_omega o).card_lt_card, card_omega]

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

Goal state before:
pp: α : Type u_1
inst✝ : Uncountable α
⊢ ℵ_ 1 ≤ #α

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ #α + #α = #α

Tactic:
by
  simp

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

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

Tactic:
by
  simp

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

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

Tactic:
by
  simp

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

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

pp: case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
· left
      use ha
      rw [← not_lt]
      apply fun hb => ne_of_gt _ h
      intro hb
      exact hb.trans_le (self_le_add_left b a)

Goal state after:
case refine_1.inr
a b : Cardinal.{u_1}
h : a + b = a
ha : a < ℵ₀
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + b = a

Tactic:
h3,

Goal state after:
case refine_2.inr
a b : Cardinal.{u_1}
h3 : b = 0
⊢ a + 0 = a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
⊢ b = c

Tactic:
have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb
    rw [lt_aleph0] at *
    rcases ha with ⟨n, rfl⟩
    rcases hb with ⟨m, rfl⟩
    rcases hc with ⟨k, rfl⟩
    norm_cast at h ⊢
    apply add_left_cancel h

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

Goal state before:
pp: case a
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 := ⋯
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
⊢ ⨆ i, ↑(f i) + 1 ≤ a

Tactic:
simp [hs]

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

Goal state before:
pp: a o : Ordinal.{u_1}
ha : o.cof.ord = a
⊢ ∃ f, IsFundamentalSeq f

Tactic:
subst ha
  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq o.ToType
  rw [cof_toType] at hs'
  let g := (OrderIso.setCongr _ _ (congrArg _ hs'.symm)).trans <|
    .ofRelIsoLT (enum (α := s) (· < ·))
  refine ⟨fun i ↦ g i, le_rfl, fun _ ↦ by simp, ?_⟩
  rw [range_comp', OrderIso.map_isCofinal_iff, range_comp', g.range_eq]
  simpa

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

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]

Goal state after:
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 c = 2 ^ lift.{v, u} #ι

Tactic:
← lift_id'.{u, v} (prod.{u, v} c),

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} #ι
⊢ lift.{u, max u v} (prod c) = 2 ^ lift.{v, u} #ι
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ω_ o).cof = ℵ_ o

Tactic:
by
  rw [← ord_aleph, H.cof_ord]

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

Goal state before:
pp: κ : Cardinal.{v}
h : κ.IsRegular
⊢ (Cardinal.lift.{u, v} κ).IsRegular

Tactic:
by
  obtain ⟨h₁, h₂⟩ := h
  constructor
  · simpa
  · rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]

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

Goal state before:
pp: κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ κ ≤ κ.ord.cof

Tactic:
simpa [← lift_le.{u, v}]

Goal state after: