mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H

Tactic:
have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ ↑l.length ≤ ENat.card α

Tactic:
cases finite_or_infinite α

Goal state after:
case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑l.length ≤ ENat.card α

case inr
α : Type u_1
l : List α
h : l.Nodup
h✝ : Infinite α
⊢ ↑l.length ≤ ENat.card α
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 \ {a}).ncard + 1

Tactic:
apply lt_add_one

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊂ t
ht : t.Finite
⊢ s.ncard < t.ncard

Tactic:
rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]
  exact (ht.subset h.subset).encard_lt_encard h

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ⇑(leftRel s) = LeftCosetEquivalence ↑s

Tactic:
ext
  rw [leftRel_eq]
  exact (leftCoset_eq_iff s).symm

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
to_encard_tac
    rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]
    apply encard_union_le

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case of
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x y : N
h : rel x y
a b : M
fa : f a = x
fb : f b = y
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
apply ConGen.Rel.of
    rwa [fa, fb]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
⊢ f = g

Tactic:
refine pi_ext fun i x => ?_
  convert! LinearMap.congr_fun (h i) x

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
by
  simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc_of_not_isMin ha b

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = s.toFinset.sup fun i ↦ a ⊓ id i

Tactic:
Finset.sup_eq_iSup

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
⊢ BddBelow (Set.range f)

Tactic:
by
  obtain ⟨M, hM⟩ := Finite.exists_ge f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ ⨆ i, f i ≤ ⨆ i, f i ⊔ a

Tactic:
exact ciSup_le fun i ↦ le_ciSup_of_le i le_sup_left

Goal state after:
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₂
s : Set M
t : Set M₂
hs : 0 ∈ s
ht : 0 ∈ t
⊢ (span R s).prod (span R t) ≤ span R (s ×ˢ t)

Tactic:
simp [Submodule.prod_le_iff, map_span]

Goal state after:
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₂
s : Set M
t : Set M₂
hs : 0 ∈ s
ht : 0 ∈ t
⊢ span R ((fun x ↦ (x, 0)) '' s) ≤ span R (s ×ˢ t) ∧ span R (Prod.mk 0 '' t) ≤ span R (s ×ˢ t)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
⊢ ⇑(partialSups (⇑g ∘ f)) = ⇑g ∘ ⇑(partialSups f)

Tactic:
funext _

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
x✝ : ι
⊢ (partialSups (⇑g ∘ f)) x✝ = (⇑g ∘ ⇑(partialSups f)) x✝
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
⊢ g.graph = ((-g).coprod id).ker

Tactic:
ext x
  change _ = _ ↔ -g x.1 + x.2 = _
  rw [add_comm, add_neg_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))

Tactic:
exact (Ioi_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)

pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)

Tactic:
· have h_eq : pred^[n] i0 = i0 := le_antisymm (pred_iterate_le _ _) h
    rw [h_eq, toZ_of_eq]
    lia

Goal state after:
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
ha : a ∈ I
n : ℕ
hn : 0 < n
⊢ ¬0 < Nat.zero

Tactic:
decide

Goal state after:
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
hqp : IsIdempotentElem (q - p)
⊢ p * q = p ∧ q * p = p

Tactic:
have h : p * (q - p) + (q - p) * p = 0 := hp.add_iff hqp |>.mp ((add_sub_cancel p q).symm ▸ hq)

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ p * q = p ∧ q * p = p
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set α
⊢ span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ span ↑s' = ⊤

Tactic:
by
  simp_rw [eq_top_iff_one]
  exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ span (range x) = span (⋃ i, {x i})

Tactic:
iUnion_singleton_eq_range

Goal state after:
α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
⊢ span (range x) = span (range x)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
range_eq_Ico,

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ¬M = ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
eq_top_iff,

Goal state after:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ¬⊤ ≤ M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ 0 - ↑⟨i, hi⟩ ∈ I

Tactic:
zero_sub

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ -↑⟨i, hi⟩ ∈ I
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
x : α →₀ M
hx : x ∈ submodule p
⊢ x.sum single ∈ ⨆ i, map (lsingle i) (p i)

Tactic:
refine Submodule.sum_mem _ (fun i _ ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
x : α →₀ M
hx : x ∈ submodule p
i : α
x✝ : i ∈ x.support
⊢ single i (x i) ∈ ⨆ i, map (lsingle i) (p i)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂

Tactic:
rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : β
ha : 0 ≤ x✝²
x✝¹ x✝ : α
hb : x✝¹ ≤ x✝
⊢ x✝¹ • x✝² ≤ x✝ • x✝²

Tactic:
simpa using mul_le_mul_of_nonneg_right (h hb) ha

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
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ Module.Finite S P

Tactic:
rw [Module.finite_def, Submodule.fg_def] at hM ⊢

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
hM : ∃ S, S.Finite ∧ span R S = ⊤
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ ∃ S_1, S_1.Finite ∧ span S S_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✝ : SMulPosStrictMono α γ
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 [← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *

Goal state after:
α : 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✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) ≤ ⨆ n, f^[n] a

Tactic:
refine ciSup_le fun n ↦ ?_

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ n, f^[n] a
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ n, f^[n] a ≤ ⨆ i, f (f^[i] a)

Tactic:
refine ciSup_le fun n ↦ ?_

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ i, f (f^[i] a)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_1
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
⊢ β → α

pp: case mpr.type.refine_2
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 : β), s a b → r (?mpr.type.refine_1 a) (?mpr.type.refine_1 b)

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
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone ?mpr.type.refine_1 ?mpr.type.refine_2)

Tactic:
· exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩

Goal state after:
case mpr.type.refine_2
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 : β), s a b → r ((enum r) ⟨f a, ⋯⟩) ((enum r) ⟨f b, ⋯⟩)

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
⊢ Function.Surjective ⇑(RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ?mpr.type.refine_2)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f → StrictMono f ∧ range f = s

Tactic:
rintro rfl
    use (Subtype.strictMono_coe _).comp (enum s hs).strictMono
    simp

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a - b = 0 ↔ a ≤ b

Tactic:
by
  simp [← nonpos_iff_eq_zero, sub_le]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ∀ (i : α ⊕ β), f i ≤ max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ a, f (Sum.inl a) ≤ ⨆ i, f i

pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ b, f (Sum.inr b) ≤ ⨆ i, f i

Tactic:
· rintro (i | i)
    · exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)
    · exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

Goal state after:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ a, f (Sum.inl a) ≤ ⨆ i, f i

α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ b, f (Sum.inr b) ≤ ⨆ i, f i
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ log b y < x ↔ y < b ^ x

Tactic:
rcases log.go_spec hb hy (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩

Goal state after:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
⊢ log b y < x ↔ y < b ^ x
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o

Tactic:
by
  simpa using nat_lt_card (n := 0)

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ a ^ b = ⨆ x, a ^ ↑x

Tactic:
opow_of_ne_zero ha,

Goal state after:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    ⨆ x, limitRecOn (↑x) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
refine ⟨fun h ↦ ?_, by grind [isSuccLimit_add]⟩
  rcases eq_or_ne b 0 with (rfl | h')
  · grind
  rw [← add_sub_cancel a b]
  exact .inl <| isSuccLimit_sub h.isSuccPrelimit <| lt_add_of_pos_right a h'.pos

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

Goal state before:
pp: case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

pp: case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n

Tactic:
· rw [log_zero_right, log_zero_right]

Goal state after:
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup ∅ = sSup ((fun x ↦ o * x) '' s)

Tactic:
csSup_empty,

Goal state after:
case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n) = log 2 n + 1

Tactic:
← log_div_mul_self,

Goal state after:
b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n / 2 * 2) = log 2 n + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a < ω ^ succ b ↔ ∃ n, a < ω ^ b * ↑n

Tactic:
refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (opow_mul_lt_opow (natCast_lt_omega0 n) (lt_succ b))⟩
  obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_pos_of_right zero_lt_one b).ne').1 ha
  refine ⟨n, hn.trans_le ?_⟩
  grw [lt_succ_iff.1 hc]
  exact omega0_pos

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

Goal state before:
pp: case inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
use n + 1
    rw [Function.iterate_succ']
    apply (lt_succ _).trans_le
    exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩

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

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

Tactic:
by
  rw [← mul_eq_right_iff_opow_omega0_dvd]
  exact (isNormal_mul_right ha).strictMono.le_apply.ge_iff_eq'

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ preAleph c.ord

Tactic:
simpa using c.ord.card_le_preAleph

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

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

Tactic:
mul_eq_self

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

case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a = 0 ∨ b = 0 ∨ (∃ n, a = ↑n) ∧ ∃ n, b = ↑n
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Tactic:
rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)

Goal state after:
case neg.inl
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

case neg.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b + a ≤ max (max a b) ℵ₀

Tactic:
add_eq_max hb,

Goal state after:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max b a ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
← Cardinal.lift_le.{u}

Goal state after:
case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = ⨆ i, f i

Tactic:
rw [← lift_id'.{u, v} (iSup _)]

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, f i
⊢ sum f = lift.{u, max u v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ (a ^ b).card ≤ max ℵ₀ (max a.card b.card)

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_natCast_or_omega0_le a
  · obtain ⟨m, rfl⟩ | hb := eq_natCast_or_omega0_le b
    · rw [opow_natCast, ← natCast_pow, card_nat]
      exact le_max_of_le_left natCast_le_aleph0
    · exact (card_opow_le_of_omega0_le_right _ hb).trans (le_max_right _ _)
  · exact (card_opow_le_of_omega0_le_left ha _).trans (le_max_right _ _)

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ o.card

Tactic:
by
  rw [← o.card.lift_id]
  exact cof_blsub_le_lift f

Goal state after: