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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ ↑(insert (pred b) (Ico a (pred b))) = ↑(Ico a b)

Tactic:
simpa using Set.insert_Ico_pred_right_eq_Ico h

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (partialSups t) n

Tactic:
by
  rw [← partialSups_disjointed, partialSups_apply, Finset.sup'_eq_sup, Finset.sup_eq_biUnion,
    disjiUnion_eq_biUnion]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ disjointed f (succ i) = f (succ i) \ (partialSups f) i

Tactic:
rw [disjointed_apply, partialSups_apply, sup'_eq_sup]
  congr 2 with m
  simpa only [mem_Iio, mem_Iic] using lt_succ_iff_of_not_isMax hi

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

pp: case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Tactic:
· exact hi.le.trans hj

Goal state after:
case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr.inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : j < i0
⊢ i ≤ j

Tactic:
rw [← iterate_pred_toZ i hi, ← iterate_pred_toZ j hj]
    refine Monotone.antitone_iterate_of_map_le pred_mono (pred_le _) (Int.toNat_le_toNat ?_)
    exact Int.neg_le_neg h_le

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid A
inst✝³ : PartialOrder A
inst✝² : CanonicallyOrderedMul A
inst✝¹ : LocallyFiniteOrderBot A
inst✝ : DecidableEq A
n : A
a : A × A
⊢ a ∈ {uv ∈ Iic n ×ˢ Iic n | uv.1 * uv.2 = n} ↔ a.1 * a.2 = n

Tactic:
simp only [mem_filter, and_iff_right_iff_imp]

Goal state after:
A✝ : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid A
inst✝³ : PartialOrder A
inst✝² : CanonicallyOrderedMul A
inst✝¹ : LocallyFiniteOrderBot A
inst✝ : DecidableEq A
n : A
a : A × A
⊢ a.1 * a.2 = n → a ∈ Iic n ×ˢ Iic n
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
I : Ideal α
inst✝ : I.IsTwoSided
hI : I.IsPrime
x y : α
⊢ x ∈ I ∨ y ∈ I → x * y ∈ I

Tactic:
rintro (h | h)

Goal state after:
case inl
α : Type u
inst✝¹ : Semiring α
I : Ideal α
inst✝ : I.IsTwoSided
hI : I.IsPrime
x y : α
h : x ∈ I
⊢ x * y ∈ I

case inr
α : Type u
inst✝¹ : Semiring α
I : Ideal α
inst✝ : I.IsTwoSided
hI : I.IsPrime
x y : α
h : y ∈ I
⊢ x * y ∈ I
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| (a + b) * b

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * b + b * b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ (a + b) * a + (a + b) * b = a + b

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a * a + b * a + (a * b + b * b) = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + b * a = 0

Tactic:
← add_right_cancel_iff (a := b),

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsCancelAdd R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
h : IsIdempotentElem (a + b)
⊢ a * b + b * a + b = 0 + b
Module: Mathlib.Algebra.Ring.Idempotent

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

Tactic:
add_mul,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * (a * b) * a + a * (b * a) * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : (p * q + q * p) * q - p * q = p * q
⊢ Commute p q

Tactic:
add_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : p * q * q + q * p * q - p * q = p * q
⊢ Commute p q
Module: Mathlib.Data.Nat.Choose.Sum

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

Tactic:
add_mul,

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * (x + y) + b * y = x✝¹
a b : α
h : a * (x + y) + b * y = x✝¹
⊢ a * x + (a + b) * y = x✝¹

Tactic:
add_mul,

Goal state after:
α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * (x + y) + b * y = x✝¹
a b : α
h : a * (x + y) + b * y = x✝¹
⊢ a * x + (a * y + b * y) = x✝¹
Module: Mathlib.RingTheory.Ideal.Basic

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

Tactic:
add_mul,

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

Goal state before:
pp: 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
n : ℕ
⊢ f.iterateMapComap i n K ≤ comap f (map i ((fun K ↦ comap f (map i K))^[n] K))

Tactic:
← iterateMapComap,

Goal state after:
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
n : ℕ
⊢ f.iterateMapComap i n K ≤ comap f (map i (f.iterateMapComap i n K))
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
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
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i ((fun K ↦ comap f (map i K))^[n] K)) = comap f (map i ((fun K ↦ comap f (map i K))^[n + 1] K))

Tactic:
← iterateMapComap,

Goal state after:
case succ
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
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun K ↦ comap f (map i K))^[n + 1] K))
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
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
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i (f.iterateMapComap i n K)) = comap f (map i ((fun K ↦ comap f (map i K))^[n + 1] K))

Tactic:
← iterateMapComap,

Goal state after:
case succ
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
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ comap f (map i (f.iterateMapComap i n K)) = comap f (map i (f.iterateMapComap i (n + 1) K))
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | ∀ ⦃x_1 : β⦄, x = y.1 → x_1 = y.2 → x_1 ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
@forall_comm β (_ = _),

Goal state after:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | x = y.1 → ∀ (a : β), a = y.2 → a ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
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 ∈ ⊤
⊢ s.Nonempty

Tactic:
rwa [mem_top.1 hs, ← nonempty_iff_univ_nonempty]

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

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

Tactic:
by rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; lia

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := ⋯
module : Module R α := ⋯
r : R
x : α
⊢ e.symm (e.addEquiv.toFun (r • x)) = e.symm ((RingHom.id R) r • e.addEquiv.toFun x)

Tactic:
simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ e.addEquiv.toEquiv (r • x) = r • e.addEquiv.toEquiv x
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
inst✝ : Finite α
C : Set α → Prop
S0 : Set α
H0 : C S0
H1 : ∀ (S : Set α), S ≠ univ → C S → ∃ a ∉ S, C (insert a S)
⊢ ∀ s ⊂ univ, C s → ∃ a ∈ univ \ s, C (insert a s)

Tactic:
by simpa [ssubset_univ_iff]

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
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f (span R ↑(t.preimage ⇑f ⋯)) = map f N

Tactic:
rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]

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
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ ↑t ⊆ range ⇑f
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ ∀ x ∈ Compl.compl '' s, DirSupClosedOn D x

Tactic:
rintro x ⟨x, hx, rfl⟩

Goal state after:
α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
x : Set α
hx : x ∈ s
⊢ DirSupClosedOn D xᶜ
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
obtain ⟨-, i, hi⟩ := lt_def.1 hb; exact le_of_smul_le_smul_right (h _) hi

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

Goal state before:
pp: case inl
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : 0 ≤ x
⊢ x ∈ Submodule.span R≥0 {1, -1}

pp: case inr
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ x ∈ Submodule.span R≥0 {1, -1}

Tactic:
· simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨x, hx⟩ (x := 1)
      (Submodule.subset_span <| by simp)

Goal state after:
case inr
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ x ∈ Submodule.span R≥0 {1, -1}
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp only [← hf, zero, smul] at *; exact smul_le_smul_of_nonneg_right ha hb

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

Goal state before:
pp: case mpr.type.refine_3
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
b : β
e : f b = (typein r).toRelEmbedding a'
⊢ (enum r) ⟨f b, ⋯⟩ = a'

Tactic:
simp [e]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} ↑(Iic o)

Tactic:
rw [← Iio_union_right]

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u}
⊢ Small.{u, u + 1} ↑(Iio o ∪ {o})
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : lift.{max u v, max u v} (type s) < lift.{max v u, v} (type r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)

Tactic:
lift_type_lt

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : Nonempty (s ≺i r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inr
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)
hnb : n ≥ b
⊢ (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:
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₃⟩

Goal state after:
case succ.inr
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)
hnb : n ≥ b
ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
ih₂ : (b * b) ^ (go n (b * b) fuel).snd ≤ n
ih₃ : n < (b * b) ^ ((go n (b * b) fuel).snd + 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)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ lsub f = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
blsub_eq_lsub'

Goal state after:
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ lsub f = lsub f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ ?a + a % b < ?a + b

pp: case a
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ Ordinal.{u_4}

Tactic:
div_add_mod

Goal state after:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
n : ℕ
⊢ a ^ ↑n = a ^ n

Tactic:
induction n with
  | zero => rw [Nat.cast_zero, opow_zero, pow_zero]
  | succ n IH => rw [Nat.cast_succ, ← succ_eq_add_one, opow_succ, pow_succ, IH]

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

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * (z * (y / z) + y % z) + w = x * y + w

Tactic:
div_add_mod

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w = x * y + w
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b n - 1 + 1 = log b n

Tactic:
Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)

Goal state after:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b n = log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
rcases clog.go_spec h.2 hb (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Goal state after:
case case1
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x

Tactic:
· simp_rw [log_of_left_le_one hb, zero_le]

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} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
⊢ ∀ (o : Ordinal.{u}), a ≤ derivFamily f o → ∃ o, derivFamily f o = a

Tactic:
intro o

Goal state after:
ι : 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
o : Ordinal.{u}
⊢ a ≤ derivFamily f o → ∃ o, derivFamily f o = 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 * (↑n + 1) ≤ a

Tactic:
rw [Ordinal.mul_le_iff_le_div, hn] <;> simp

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

Goal state before:
pp: x : Ordinal.{u_1}
| ω ≤ preOmega x

Tactic:
rw [← preOmega_omega0, preOmega_le_preOmega]

Goal state after:
x : Ordinal.{u_1}
| ω ≤ x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
⊢ (deriv fun x ↦ a * x) = HMul.hMul (a ^ ω)

Tactic:
IsNormal.ext_iff (isNormal_deriv _) (isNormal_mul_right (opow_pos ω ha))

Goal state after:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a * x) a_1 = a ^ ω * a_1 → deriv (fun x ↦ a * x) (succ a_1) = a ^ ω * succ a_1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
a : ↑(Iio o)
⊢ ↑a < o

Tactic:
exact a.2

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_1}
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ 2 ^ x

Tactic:
refine ⟨preBeth a, ?_, ?_⟩

Goal state after:
case refine_1.refine_1
a : Ordinal.{u_1}
⊢ preBeth a < preBeth (succ a)

case refine_1.refine_2
a : Ordinal.{u_1}
⊢ preBeth (succ a) ≤ 2 ^ preBeth a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ ω_ ↑n ↔ o ≤ ω_ ↑n

Tactic:
by
  simpa using lift_le (b := ω_ n)

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
⊢ (⨆ i, ↑(f i) + 1).cof.ord ≤ a

Tactic:
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.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_3
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
⊢ f i < (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)

Goal state after:
case refine_3
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'