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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
⊢ c.toCon = ⊤ ↔ c = ⊤

Tactic:
rw [← toCon_top, toCon_inj]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := ⋯
hy : y ∈ s
⊢ ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))

Tactic:
rw [← Set.singleton_subset_iff] at hy

Goal state after:
case right
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : {y} ⊆ s
⊢ ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))
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 d : M
⊢ BijOn (fun x ↦ x + d) (Ioi a) (Ioi (a + d))

Tactic:
refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩
  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
  rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h
  exact ⟨a + c, h, by rw [add_right_comm]⟩

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j

Tactic:
exact h.1 j hij

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i

Tactic:
rw [lt_isGLB_iff (succFn_spec i)] at hij
  obtain ⟨k, hk_lb, hk⟩ := hij
  rw [mem_lowerBounds] at hk_lb
  exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ q.1 * p.2 = n

Tactic:
← h,

Goal state after:
A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p.1 * p.2 = n
hq : q.1 * q.2 = n
h : p.1 = q.1
⊢ p.1 * p.2 = n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ range (↑a + 1) →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Iic a then f ⟨a_1, h⟩.succ / f ⟨a_1, h⟩.castSucc else 1 else 1) =
        (if hi : a_1 + 1 < n + 1 then f ⟨a_1 + 1, hi⟩ else 1) / if hi : a_1 < n + 1 then f ⟨a_1, hi⟩ else 1

Tactic:
simp_all; grind

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

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

Tactic:
exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x

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

Goal state before:
pp: case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
induction n, h using le_induction with

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

Goal state before:
pp: case cons
α : 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)
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
by_cases! h : n + 1 ≤ c

Goal state after:
case pos
α : 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 : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

case neg
α : 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 + 1
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z
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
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : (Submodule.quotientRel I) c₁ c₂
hm : (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi fun x ↦ I

Tactic:
rw [Submodule.quotientRel_def] at hc hm

Goal state after:
ι : 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
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : c₁ - c₂ ∈ I
hm : m₁ - m₂ ∈ pi fun x ↦ I
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi fun x ↦ I
Module: Mathlib.Order.Filter.AtTopBot.Defs

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

Tactic:
by
  simp only [generate_eq_biInf, atTop, iInf_range]

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

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
not_lt

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
not_lt

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

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

Tactic:
by
  simp [Tendsto]

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

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ x, p x

Tactic:
by
  by_contra H
  replace H : ∀ᶠ x in f, ¬p x := Eventually.of_forall (not_exists.1 H)
  exact hp H

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

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)

Tactic:
refine ⟨fun i ↦ if h : ∃ b, P i b then h.choose else Nonempty.some inferInstance, ?_⟩

Goal state after:
ι : Type u_2
α : ι → Type u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
P : (i : ι) → α i → Prop
F : Filter ι
H : ∀ᶠ (i : ι) in F, ∃ b, P i b
⊢ ∀ᶠ (i : ι) in F, P i ((fun i ↦ if h : ∃ b, P i b then h.choose else ⋯.some) i)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t

Tactic:
simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]

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

Goal state before:
pp: ⊢ map Nat.cast atTop = atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_
  lift n to ℕ using hn
  exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : x ∈ LinearMap.ker (f ^ (n + m))
⊢ (f ^ n) x = 0

Tactic:
← hn _ (n.le_add_right m)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : x ∈ LinearMap.ker (f ^ n)
⊢ (f ^ n) x = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : cof α = 0
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ IsEmpty α

Tactic:
simp_all [mk_eq_zero_iff, isCofinal_empty_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ x ∈ s, ¬IsCofinal x
⊢ cof α ≤ #↑s

Tactic:
simp_rw [not_isCofinal_iff] at h₂

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ x ∈ s, ∃ x_1, ∀ y ∈ x, y < x_1
⊢ cof α ≤ #↑s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ iSup ⇑N

Tactic:
exact le_iSup ..

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 : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = ⨆ a ∈ sp '' ↑s, a

Tactic:
iSup_image,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
⊢ s = ⨆ b ∈ ↑s, sp b
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
val✝ : Fintype M
⊢ span R ↑Finset.univ = ⊤

Tactic:
Finset.coe_univ,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
val✝ : Fintype M
⊢ span R univ = ⊤
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (↑s • ↑t) = ⊤

Tactic:
span_smul_of_span_eq_top hs (↑t : Set M),

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ restrictScalars R (span A ↑t) = ⊤
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
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 ((enum r) ⟨f a, ⋯⟩) ((enum r) ⟨f 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 (fun b ↦ (enum r) ⟨f b, ⋯⟩) ?mpr.type.refine_2)

Tactic:
· refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h

Goal state after:
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, ⋯⟩) ⋯)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a ≤ b ↔ a ≤ succ b

Tactic:
ha.le_succ_iff

Goal state after:
case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
· rw [ha.ordinalPred_eq, ha.le_succ_iff]

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

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

Tactic:
not_lt

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ o₂ ≤ o₁ ↔ o₂ ≤ o₁
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:
rw [enum_lt_enum (r := r), not_lt]

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

Goal state before:
pp: a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔
    ¬(enum fun x1 x2 ↦ x1 < x2) o₂ < (enum fun x1 x2 ↦ x1 < x2) o₁

Tactic:
not_lt

Goal state after:
a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔
    (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x✝¹ : α → α → Prop
x✝ : IsWellOrder α x✝¹
⊢ ∀ {a b : α × PUnit.{u + 1}}, x✝¹ ((prodPUnit α) a) ((prodPUnit α) b) ↔ Prod.Lex x✝¹ emptyRelation a b

Tactic:
simp [Prod.lex_def]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal.{u}
α : Type u
x✝¹ : α → α → Prop
x✝ : IsWellOrder α x✝¹
⊢ ∀ {a b : PUnit.{u + 1} × α}, x✝¹ ((punitProd α) a) ((punitProd α) b) ↔ Prod.Lex emptyRelation x✝¹ a b

Tactic:
simp [Prod.lex_def]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
a b c : Ordinal.{u_4}
x✝² x✝¹ x✝ : WellOrder
α : Type u_4
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u_4
s : β → β → Prop
wo✝¹ : IsWellOrder β s
γ : Type u_4
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
⊢ ∀ {a b : (β ⊕ γ) × α},
    Sum.Lex (Prod.Lex s r) (Prod.Lex t r) ((sumProdDistrib β γ α) a) ((sumProdDistrib β γ α) b) ↔
      Prod.Lex (Sum.Lex s t) r a b

Tactic:
simp [Prod.lex_def]

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

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ b * a

Tactic:
convert! mul_le_mul_left (one_le_iff_pos.2 hb) a

Goal state after:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ a = (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

Tactic:
rw [← enum_typein (α := ToType 1) (· < ·) a]
    congr
    rw [← lt_one_iff]
    apply typein_lt_self

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

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ ¬a < (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩

Tactic:
not_lt

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
h : o < typeLT α
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨o, h⟩ ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
by
  refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_
  · rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
  · rw [ord_le, ← lift_card, card_ord]

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 < a.ord ↔ 0 < a

Tactic:
← ord_zero,

Goal state after:
a : Cardinal.{u_1}
⊢ ord 0 < a.ord ↔ 0 < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ ¬b < c * succ a ↔ c * succ a ≤ b

Tactic:
not_lt

Goal state after:
a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ c * succ a ≤ b ↔ c * succ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a * (b - c) = a * b - a * c

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
b c : Ordinal.{u_4}
⊢ 0 * (b - c) = 0 * b - 0 * c

case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ ¬log b n < log b (n + 1)

Tactic:
not_lt

Goal state after:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ log b (n + 1) ≤ log b n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a % a = 0

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
⊢ 0 % 0 = 0

case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

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

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

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

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ n, o = ↑n

Tactic:
simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

case inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
⊢ a ^ (b * c) = (a ^ b) ^ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ ¬clog b n < clog b (n + 1)

Tactic:
not_lt

Goal state after:
b n : ℕ
hb : 1 < b
⊢ clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hbo : 0 < b
⊢ log b 0 = 0

pp: case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0

Tactic:
· exact log_zero_right b

Goal state after:
case inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
⊢ log b o = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ deriv f = enumOrd (fixedPoints f)

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

Goal state after:
case e'_3
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f
Module: Mathlib.SetTheory.Ordinal.Principal

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

pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a

Tactic:
· rw [← lt_add_one_iff, one_add_one_eq_two]
        exact hao.trans_le ho

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 ≤ a
Module: Mathlib.SetTheory.Ordinal.Principal

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

pp: case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
· rcases le_or_gt o 2 with ho | ho
    · convert! one_mul o
      apply le_antisymm
      · rw [← lt_add_one_iff, one_add_one_eq_two]
        exact hao.trans_le ho
      · rwa [one_le_iff_pos]
    · exact op_eq_self_of_isPrincipal hao (isNormal_mul_right ha₀) h
        (isSuccLimit_of_isPrincipal_mul ho h)

Goal state after:
case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
by
  simpa using preBeth_lt_preBeth (o₁ := 0)

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

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

Tactic:
by
  simpa using c.ord.card_le_preBeth

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1

Tactic:
← h,

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a * b < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b + max a b < c

Tactic:
add_eq_self h

Goal state after:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
← h,

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

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

pp: case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a

Tactic:
· rcases le_or_gt ℵ₀ a with ha | ha
    · 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)
    right
    rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
    norm_cast at h ⊢
    rw [← add_right_inj, h, add_zero]

Goal state after:
case refine_2
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0 → a + b = a
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{v, u} o.card * ⨆ i, lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c * lift.{u, v} c

Tactic:
refine mul_le_mul' ho (ciSup_le' ?_)

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ ∀ (i : o.ToType), lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c