mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * x ^ i * y ^ (n - i) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

Tactic:
mul_assoc,

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * x ^ i * (y ^ (n - i) * ↑(n.choose i)) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * x ^ i * (y ^ (n - i) * ↑(n.choose i)) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

Tactic:
mul_assoc,

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * (x ^ i * (y ^ (n - i) * ↑(n.choose i))) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ b * a + b * a - b * (b * a) = b * a

Tactic:
hb.mul_self_mul,

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ b * a + b * a - b * a = b * a
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 + a * (b * a) * a = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
mul_assoc,

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.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * y ^ (n - i.succ)) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * y ^ (n - i.succ) * ↑(n.choose i.succ)) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * y ^ (n - i.succ) * ↑(n.choose i.succ)) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
mul_assoc,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
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
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * (y * (y ^ (n - i.succ) * ↑(n.choose i.succ))) = x ^ i.succ * y * (y ^ (n - i.succ) * ↑(n.choose i.succ))
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
h : a * b * a = 0
⊢ a * a * b + a * b * a = 0

Tactic:
mul_assoc,

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
h : a * b * a = 0
⊢ a * (a * b) + a * b * a = 0
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
h : a * b * a = 0
⊢ a * (a * b) + a * b * a = 0

Tactic:
mul_assoc,

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
h : a * b * a = 0
⊢ a * (a * b) + 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 + q * p * q - p * q = p * q
⊢ Commute p q

Tactic:
mul_assoc,

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.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
⊢ M ⊔ M' = ⊤

Tactic:
by
  contrapose! hne with h
  exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

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

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∑ x ∈ Finset.range (k + 1), ↑(k.choose x) * (a ^ x * b ^ (k - x)) ∈ I

Tactic:
apply I.sum_mem

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∀ c ∈ Finset.range (k + 1), ↑(k.choose c) * (a ^ c * b ^ (k - c)) ∈ I
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * ((1 - e) * e) = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = n * 2 * 2 ^ (n - 1)

Tactic:
mul_assoc,

Goal state after:
n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = n * (2 * 2 ^ (n - 1))
Module: Mathlib.RingTheory.Ideal.Basic

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

Tactic:
have : (Multiset.card s + 1) * n + 1 - c = Multiset.card s * n + 1 + (n - c) := by
      rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]

Goal state after:
case h
α : 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
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.RingTheory.Ideal.Basic

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

Tactic:
mul_assoc,

Goal state after:
case h
α : 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
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * (s.sum ^ (s.card * n + 1) * (s.sum ^ (n - c) * ↑(((s.card + 1) * n + 1).choose c))) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: 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
i : α
⊢ comap (lsingle i) (submodule p) = p i

Tactic:
ext x
  refine ⟨fun hx ↦ by simpa using hx i, fun hx j ↦ ?_⟩
  rcases eq_or_ne i j with rfl|h <;> simp_all

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

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

Tactic:
filter_upwards with i
    simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

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

Goal state before:
pp: case refine_1
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_mem : a ∈ s
x : α
hx : x ∈ s
⊢ Ici x ⊆ Ici a

Tactic:
exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)

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

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

Tactic:
by simp [Tendsto]

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)

Goal state after:
α : Type u_1
f : Filter α
s : Set α
⊢ (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
this : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
by
    simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → ∃ n s, span R (range s) = N

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Tactic:
· rintro ⟨S, Sfin, hS⟩
    obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding
    exact ⟨n, f, hS⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M

Tactic:
· intro H
    constructor
    intro N
    obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ :=
      WellFounded.has_min H.wf { N' : α | N'.1 ≤ N } ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩
    convert! h₁
    refine (e.antisymm ?_).symm
    by_contra h₃
    obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
    apply hx₂
    rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]
    exact (le_sup_left : R ∙ x ≤ _) (Submodule.mem_span_singleton_self _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : a ≤ 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
⊢ IsCofinal {a | ∀ (b : α), r b a → b < a}

Tactic:
intro a
  obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici
  refine ⟨b, fun c hc ↦ ?_, hb⟩
  by_contra! hc'
  exact hb' c (hb.trans hc') hc

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

Tactic:
simp [← ha] at h

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInacc sᶜ ↔ DirSupClosed s

Tactic:
by
  rw [← dirSupClosed_compl, compl_compl]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 < a.1
h₂ : 0.2 ≤ a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

pp: case inr
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 ≤ a.1
h₂ : 0.2 < a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2

Tactic:
· exact .inl ⟨smul_lt_smul_of_pos_right hb h₁, smul_le_smul_of_nonneg_right hb.le h₂⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
a : β × γ
h₁ : 0.1 ≤ a.1
h₂ : 0.2 < a.2
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ (_b₁ • a).1 < (_b₂ • a).1 ∧ (_b₁ • a).2 ≤ (_b₂ • a).2 ∨ (_b₁ • a).1 ≤ (_b₂ • a).1 ∧ (_b₁ • a).2 < (_b₂ • a).2
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✝ : SMulPosReflectLT α γ
b : β
a₁ a₂ : α
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
h : a₁ • f b < a₂ • f b
⊢ a₁ < a₂

Tactic:
exact lt_of_smul_lt_smul_right h hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
⊢ f a ≤ b

Tactic:
le_iff_forall_le hf ha'

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
⊢ ∀ a' < a, f a' ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
have : Nonempty β := ⟨x⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this : Nonempty β
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : γ
hx : f (Sum.inr a) = Sum.inl x
⊢ ∃ b, Sum.inl x = Sum.inr b

Tactic:
← H₁,

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
a : α
x : γ
hx : f (Sum.inr a) = f (Sum.inl x)
⊢ ∃ b, Sum.inl x = Sum.inr b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
⊢ Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ #↑s

Tactic:
rw [← Cardinal.mk_Iio_ordinal]

Goal state after:
s : Set Ordinal.{u}
⊢ #↑(Iio (sInf sᶜ)) ≤ #↑s
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ range (enumOrd s) → a ∈ s

Tactic:
rintro ⟨b, rfl⟩
    exact enumOrd_mem hs b

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}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ o.bsup f
a : Ordinal.{max u v}
⊢ a < o.bsup f → succ a < o.bsup f

Tactic:
rw [← iSup_eq_bsup] at *
  exact succ_lt_iSup_of_ne_iSup fun i => hf _

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

Goal state before:
pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * d * (b / d) ≤ a * b + c

Tactic:
mul_assoc,

Goal state after:
case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * (d * (b / d)) ≤ a * b + c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Tactic:
simp [@eq_comm _ 0, hm]

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

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : a * b ≠ 0
h : b = 0
⊢ False

Tactic:
simp [h] at b0

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) + x * (y % z) + w = x * y + w

Tactic:
mul_assoc,

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * (z * (y / z)) + x * (y % z) + w = x * y + w
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c

Tactic:
mul_assoc,

Goal state after:
a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * (d * (a / (c * d))) + a % (c * d)) % c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a < b
⊢ a ^ c * a < b ^ c * b

Tactic:
exact mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (by gcongr) ab zero_le (opow_pos _ ab.bot_lt)

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

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
isSuccPrelimit_iff_succ_lt,

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ a < c.ord, succ a < c.ord
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * b ^ log b v ≤ b ^ u * v + w

Tactic:
opow_log_le_self b hv,

Goal state after:
case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v ≤ b ^ u * v + w
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
← iSup_iterate_eq_nfp

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < nfp f b ↔ ∃ n, a < f^[n] b

Tactic:
← iSup_iterate_eq_nfp

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ a < ⨆ n, f^[n] b ↔ ∃ n, a < f^[n] b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
← iSup_iterate_eq_nfp

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp 0 a = a

Tactic:
← iSup_iterate_eq_nfp

Goal state after:
a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
simpa using lift_inj (a := ℵ₁)

Goal state after: