mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ x✝ ∈ ⇑f ⁻¹' {f a} ↔ x✝ ∈ a • ↑f.ker

Tactic:
by
      rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (Subtype.val '' ↑t').ncard = t'.card

Tactic:
ncard_image_of_injective _ Subtype.coe_injective

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp only [three_lt_ncard_iff hs, exists_and_left]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card

Tactic:
· simp

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
rw [← encard_eq_three, ncard_def]

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard.toNat = 3 ↔ s.encard = 3
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : IsEmpty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : Nonempty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : Nonempty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
this : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
by grind

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

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

Tactic:
| refl x =>

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

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

Tactic:
induction h generalizing a b with
  | of x y h =>
    apply ConGen.Rel.of
    rwa [fa, fb]
  | refl x =>
    rw [f.injective (fa.trans fb.symm)]
    exact ConGen.Rel.refl _
  | symm _ h => exact ConGen.Rel.symm (h fb fa)
  | trans _ _ ih ih1 =>
    exact Exists.casesOn (f.surjective _) fun c' hc' ↦ ConGen.Rel.trans (ih fa hc') (ih1 hc' fb)
  | @mul w x y z _ _ ih ih1 =>
    rw [← f.eq_symm_apply, map_mul] at fa fb
    rw [fa, fb]
    exact ConGen.Rel.mul (ih (by simp) (by simp)) (ih1 (by simp) (by simp))

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₂
⊢ (inr R M M₂).range = (fst R M M₂).ker

Tactic:
ext x
  simp only [mem_ker, mem_range]
  constructor
  · rintro ⟨y, rfl⟩
    rfl
  · intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule 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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
⊢ map (p.liftQ f h) q ≤ map f (comap p.mkQ q)

Tactic:
by rintro _ ⟨⟨x⟩, hxq, rfl⟩; exact ⟨x, hxq, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Icc, coe_Icc]
  exact Set.image_add_const_Icc _ _ _

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

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
⊢ disjointed s 0 = s 0

pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iio (k + 1)).sup s = s k

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ (Iio (k + 1)).sup s = s k
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case zero
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
hn : ¬IsMin (pred^[0] i0)
⊢ toZ i0 (pred^[0] i0) = -↑0

pp: case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
· simp

Goal state after:
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case zero
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ j ∈ range 0, f (0 - 1 - j) = ∏ j ∈ range 0, f j

pp: case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ range (n✝ + 1), f (n✝ + 1 - 1 - j) = ∏ j ∈ range (n✝ + 1), f j

Tactic:
· simp

Goal state after:
case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ range (n✝ + 1), f (n✝ + 1 - 1 - j) = ∏ j ∈ range (n✝ + 1), f j
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (List.Nat.antidiagonal n).length = n + 1

Tactic:
List.Nat.length_antidiagonal

Goal state after:
n : ℕ
⊢ n + 1 = n + 1
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) = 1

Tactic:
by grind

Goal state after:
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 (↑a + 1),
    a_1 ∉ range n →
      ((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) = 1

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | a.2 ≤ k} =
    map ({ toFun := fun x ↦ x + (n - k), inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal k)

Tactic:
by
  ext ⟨i, j⟩
  suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
  refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
  · rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
    rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
    exact Nat.sub_add_cancel h

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
a : α
x✝ : ∃ y, x ↑y = a
j : ↑{x_1 | x x_1 ≠ 0}
hj : x ↑j = a
⊢ ¬a = 0

Tactic:
by grind

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
by
  rw [sub_eq_add_neg, add_pow]
  congr! 1 with m hm
  have : (-1 : R) ^ (n - m) = (-1) ^ (n + m) := by
    rw [mem_range] at hm
    simp [show n + m = n - m + 2 * m by lia, pow_add]
  rw [neg_pow, this]
  ring

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

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

Tactic:
obtain ⟨c, rfl⟩ := hu

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
v : α
hv : a ∣ v
c : α
ha : a = a * c * v
huv : ¬IsUnit (a * c) ∧ ¬IsUnit v
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
S T : Ideal R
inst✝¹ : S.IsTwoSided
inst✝ : T.IsTwoSided
H : S ≤ T
⊢ (factor H).comp (mk S) = mk T

Tactic:
by
  ext x
  rw [RingHom.comp_apply, factor_mk]

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

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

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ ((((inr R P M ∘ₗ f) ^ 0) ∘ₗ inl R P M) (x 0)).1 = x 0

pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
n : ℕ
x✝ : n ∈ x.support
hn : n ≠ 0
⊢ ((((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) (x n)).1 = 0

Tactic:
· simp

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
n : ℕ
x✝ : n ∈ x.support
hn : n ≠ 0
⊢ ((((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) (x n)).1 = 0
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
⊢ ¬Disjoint f f ↔ f.NeBot

Tactic:
disjoint_self,

Goal state after:
α : Type u
f : Filter α
⊢ ¬f = ⊥ ↔ f.NeBot
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f

Tactic:
← image_univ

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f
Module: Mathlib.Order.Filter.Map

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

Tactic:
mem_kernMap_iff_compl,

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ t, tᶜ ∈ f ∧ m '' t = sᶜᶜ) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl ⊤ ⊓ map inr ⊤ ≤ ⊥

Tactic:
· simp

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Tactic:
simp only [Filter.Frequently, eventually_inf_principal, not_and]

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

Goal state before:
pp: k b : ℕ
x✝ : 0 ≤ b
⊢ b ≤ b + k - k

Tactic:
rw [Nat.add_sub_cancel_right]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).Finite ↔ Module.Finite A B

Tactic:
rw [Finite, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Nonempty α
s : Set α
hs : IsCofinal s
⊢ s.Nonempty

Tactic:
by
  inhabit α
  exact (hs default).imp fun _ ↦ And.left

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

Goal state before:
pp: case h.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)
s : M
hs : s ∈ ↑S
⊢ s ∈ ↑(N (S.attach.sup f))

Tactic:
exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)

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

Goal state before:
pp: case mpr
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 : IsCompactElement s
⊢ s.FG

Tactic:
rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h

Goal state after:
case mpr
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.FG
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
by grind

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsEmpty o.ToType ↔ o = 0

Tactic:
by
  rw [← @type_eq_zero_iff_isEmpty o.ToType (· < ·), type_toType]

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

Goal state before:
pp: case inl
b a : Ordinal.{u_4}
⊢ (succ a).pred ≤ b ↔ succ a ≤ succ b

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

Tactic:
· simp

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
⊢ (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)

pp: case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
· simp

Goal state after:
case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred

pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
· simp

Goal state after:
case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ (range fun x ↦ ↑((StrictMono.orderIso f hf) x)) = range f

Tactic:
· simp

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))

Tactic:
rintro (i | i)

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

case inr
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
i : β
⊢ f (Sum.inr i) ≤ max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case left
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a₁✝ : α
b₁✝ : γ
a₂✝ : α
b₂✝ : γ
h' : r a₁✝ a₂✝
⊢ Prod.Lex s t (f (a₁✝, b₁✝).1, (a₁✝, b₁✝).2) (f (a₂✝, b₂✝).1, (a₂✝, b₂✝).2)

Tactic:
exact Prod.Lex.left _ _ (f.toRelEmbedding.map_rel_iff.2 h')

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

Goal state before:
pp: case inl
⊢ (sSup ∅).ord = sSup (ord '' ∅)

pp: case inr
s : Set Cardinal.{u_3}
hn : s.Nonempty
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
· simp

Goal state after:
case inr
s : Set Cardinal.{u_3}
hn : s.Nonempty
⊢ (sSup s).ord = sSup (ord '' s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{v}
⊢ lift.{u, v} a ≤ lift.{u, v} b ∧ lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ b ≤ a

Tactic:
lift_le

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

Goal state before:
pp: a b : Ordinal.{v}
⊢ lift.{u, v} a ≤ lift.{u, v} b ∧ ¬lift.{u, v} b ≤ lift.{u, v} a ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
lift_le

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 * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : ¬b = b'
⊢ s b' b

Tactic:
by grind

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
⊢ a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d

pp: case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
· simp

Goal state after:
case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ b > 0

Tactic:
by grind

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

Goal state before:
pp: n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ fuel + 1 ≤ 2 * fuel

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max v u_3}
⊢ lsub f = 0 ↔ IsEmpty ι

Tactic:
refine ⟨fun h => ⟨fun i => ?_⟩, fun h => @lsub_empty _ h _⟩
  have := @lsub_pos.{_, v} _ ⟨i⟩ f
  rw [h] at this
  exact this.false

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
obtain rfl | hb := eq_or_ne b 0
  · simp
  · rw [mul_add_one, lt_add_iff hb]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o ≤ lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding

Tactic:
by_contra! h
      have h := h.trans_eq (type_toType o).symm
      simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) ⟨_, h⟩)

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f

Tactic:
rw [← iSup_eq_bsup, ← lsub_eq_blsub]
  exact iSup_eq_lsub_or_succ_iSup_eq_lsub _

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ω ≤ a.ord ↔ ℵ₀ ≤ a

Tactic:
rw [← ord_aleph0, ord_le_ord]

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀

Tactic:
rw [← ord_aleph0, ord_le_ord]

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
h : a ≤ 0 * c
⊢ a / 0 ≤ c

pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c

Tactic:
· simp

Goal state after:
case inr
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n < 0 ↔ log b (n / b) + 1 < 0

pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
· simp

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
· simp

Goal state after:
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 : ℕ
⊢ Monotone (log b)

Tactic:
by
  refine monotone_nat_of_le_succ fun n => ?_
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb]
    exact zero_le _
  · exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

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

Goal state before:
pp: case inl
⊢ 0 % 0 = 0

pp: case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0

Tactic:
· simp

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n + 1) ≤ log b n → log b n ≤ log b (n + 1)

Tactic:
exact fun _ ↦ log_monotone (le_add_right n 1)

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

Goal state before:
pp: case inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

pp: case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
· simp

Goal state after:
case inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0

pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
· simp

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

pp: case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Tactic:
· simp

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
· simp

Goal state after:
case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
· simp

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

Goal state before:
pp: case inl
o : Ordinal.{u_1}
⊢ o * sSup ∅ = sSup ((fun x ↦ o * x) '' ∅)

pp: case inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
· simp

Goal state after:
case inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)