mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ Set.InjOn (HSub.hSub n) ↑(Ico k m)

Tactic:
simp only [mem_Ico, Set.InjOn, mem_coe]

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∀ ⦃x₁ : ℕ⦄, k ≤ x₁ ∧ x₁ < m → ∀ ⦃x₂ : ℕ⦄, k ≤ x₂ ∧ x₂ < m → n - x₁ = n - x₂ → x₁ = x₂
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤

Tactic:
rw [or_iff_not_imp_right]
  change _ ≠ _ → _
  rw [Ideal.ne_top_iff_one]
  intro h1
  rw [eq_bot_iff]
  intro r hr
  by_cases H : r = 0; · simpa
  simpa [H, h1] using I.mul_mem_left r⁻¹ hr

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

Goal state before:
pp: case pos
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 ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

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 ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
· rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]

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 ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

Tactic:
rintro ⟨ya, hya, b, hb, rfl⟩

Goal state after:
case mp
α : Type u
inst✝ : Semiring α
y : α
I : Ideal α
ya : α
hya : ya ∈ span {y}
b : α
hb : b ∈ I
⊢ ∃ a, ∃ b_1 ∈ I, a * y + b_1 = ya + b
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (1 ∉ I ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
    1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
← Ideal.eq_top_iff_one

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

Goal state before:
pp: 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

Tactic:
use 0

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 + 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) = 0 * a ^ (n + 1) + z
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
by
  trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j
  · refine (sum_fiberwise_of_maps_to ?_ _).symm
    intro y hy
    rw [mem_range, Nat.lt_succ_iff]
    rw [mem_powerset] at hy
    exact card_le_card hy
  · refine sum_congr rfl fun y _ ↦ ?_
    rw [← card_powersetCard, ← sum_const]
    refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_
    rw [(mem_powersetCard.1 hz).2]

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

Goal state before:
pp: case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ 0 + 1 ∈ J

Tactic:
← sub_self (x * y),

Goal state after:
case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ x * y - x * y + 1 ∈ J
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ (d + (0, n + 1).2).choose d + ∑ p ∈ antidiagonal n, (d + (p.1 + 1, p.2).2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
hn,

Goal state after:
case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
F : FilterBasis α
⊢ F.filter.ker = ⋂₀ F.sets

Tactic:
by
  aesop (add simp [ker, FilterBasis.filter])

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

Goal state before:
pp: α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
apply Subsingleton.induction_on hf <;> simp

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

Goal state before:
pp: α : Type u
f₁ f₂ : Filter (Filter α)
x : Set α
⊢ x ∈ f₁.join ⊔ f₂.join ↔ x ∈ (f₁ ⊔ f₂).join

Tactic:
simp only [mem_sup, mem_join]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
⊢ f₁.bind g₁ ≤ f₂.bind g₂

Tactic:
refine le_trans (fun s hs => ?_) (join_mono <| map_mono hf)
  simp only [mem_join, mem_bind', mem_map] at hs ⊢
  filter_upwards [hg, hs] with _ hx hs using hx hs

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ MulOneClass α

Tactic:
apply e.injective.mulOneClass _ <;> intros

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
⊢ MulOneClass α

Tactic:
by
  let one := e.one
  let mul := e.mul
  apply e.injective.mulOneClass _ <;> intros <;> exact e.apply_symm_apply _

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:
by
    simpa using mul_le_mul_of_nonneg_right (h hb) ha

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : 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 β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ sSup (f ⁻¹' Iic x) < succ (sSup (f ⁻¹' Iic x))

Tactic:
lt_succ_iff

Goal state after:
case refine_2
α : 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 β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ sSup (f ⁻¹' Iic x) ≤ sSup (f ⁻¹' Iic x)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
c' : Cardinal.{u}
h' : lift.{u + 1, u} c' < univ.{u, u + 1}
e : lift.{v, u + 1} (lift.{u + 1, u} c') = c
⊢ c = lift.{max (u + 1) v, u} c'

Tactic:
simp only [e.symm, lift_lift]

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

Goal state before:
pp: case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)

Tactic:
lt_succ_iff

Goal state after:
case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ (typein r).toRelEmbedding x ≤ (typein r).toRelEmbedding x
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≼i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≼i s

Tactic:
exact (RelIso.preimage Equiv.ulift r).symm.toInitialSeg.trans
      (f.trans (RelIso.preimage Equiv.ulift s).toInitialSeg)

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} β
⊢ iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Tactic:
apply (Ordinal.iSup_le _).antisymm (max_le _ _)

Goal state after:
α : 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))

α : 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.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u_3}
⊢ ⨆ i, f i ≤ ⨆ i, f i + 1

Tactic:
rw [iSup, iSup, range_comp' (· + 1)]
  exact sSup_le_sSup_add_one _

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

Goal state before:
pp: a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c < succ b
⊢ enumOrd s c < a

Tactic:
lt_succ_iff

Goal state after:
a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
c : Ordinal.{u}
hc : c ≤ b
⊢ enumOrd s c < a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a < succ a

Tactic:
lt_succ_iff

Goal state after:
case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o < succ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a) ↔ o < typeLT α

Tactic:
lt_succ_iff

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
o : Ordinal.{u}
⊢ o ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a ↔ o < typeLT α
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inr
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b ^ 2) fuel).fst = n / b ^ (2 * (go n (b ^ 2) fuel).snd)
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 2)
⊢ (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
        else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
              else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd +
            1)

Tactic:
split <;> simp_all

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o.card < succ c

Tactic:
lt_succ_iff

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
⊢ o.card ≤ c ↔ o.card ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * c' ≤ a * c

Tactic:
by
      grw [le_succ c', IH _ h, le_self_add (a := b), ba, ← mul_succ, succ_le_of_lt <| l.succ_lt h]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a / b < succ (a / b)

Tactic:
lt_succ_iff

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

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

Tactic:
have H := mul_ne_zero hc.ne_zero hd

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)

Tactic:
exact zero_le _

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

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

Tactic:
rw [← add_lt_add_iff_left, div_add_mod]
  exact lt_mul_div_add a h

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

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
l : IsSuccLimit a
hb : b ≠ 0
e : b = 0
⊢ IsSuccLimit (a ^ b)

Tactic:
exact absurd e hb

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

Goal state before:
pp: b k n : ℕ
⊢ log (b ^ k) n = log b n / k

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · rcases k.eq_zero_or_pos with rfl | hk
    · simp
    · rcases Nat.lt_or_ge 1 b with hb | hb
      · refine eq_of_forall_le_iff fun c ↦ ?_
        rw [le_log_iff_pow_le (Nat.one_lt_pow (Nat.ne_of_gt hk) hb) hn, Nat.le_div_iff_mul_le hk,
          le_log_iff_pow_le hb hn, Nat.pow_mul']
      · rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]
        rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

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

Goal state before:
pp: case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m

Tactic:
exact zero_le _

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n

Tactic:
exact zero_le _

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

Goal state before:
pp: case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Tactic:
exact zero_le _

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

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
exact H.strictMono.le_apply.trans (Ordinal.le_iSup _ _)

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

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

Tactic:
lt_succ_iff

Goal state after:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ log b x
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Tactic:
by
  simp [IsPrincipal]

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

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ 0)

pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
· rw [opow_zero, isPrincipal_one_iff, add_zero]

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ a * b < c

Tactic:
by
  apply (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt
  obtain h | h := lt_or_ge (max a b) ℵ₀
  · exact (mul_lt_aleph0 h h).trans_le hc
  · rw [mul_eq_self h]
    exact max_lt ha hb

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < succ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
lt_succ_iff

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ ℵ₀ ↔ c ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case refine_1.refine_1
a : Ordinal.{u_1}
⊢ a < succ a

Tactic:
lt_succ_iff

Goal state after:
case refine_1.refine_1
a : Ordinal.{u_1}
⊢ a ≤ a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iic i) < #α

Tactic:
rw [← Iio_insert, mk_insert self_notMem_Iio]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iio i) + 1 < #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ sSup ((fun x ↦ x + 1) '' range f) < a

Tactic:
apply sSup_add_one_lt_of_lt_cof _ (by simpa)

Goal state after:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, v} #β < (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ #↑(range f) < (lift.{u + 1, u} a).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
hlt : a < μ
⊢ (↑n + 1) * a < (↑n + 1) * μ

Tactic:
simpa using! (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)

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

Goal state before:
pp: ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: case inl
β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
a : α
ha : ℵ₀ ≤ #↑(f ⁻¹' {a})
⊢ ∃ a, succ #α ≤ #↑(f ⁻¹' {a})

Tactic:
exact ⟨a, ha.trans' (succ_le_of_lt hα)⟩

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

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{?u.55, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ lift.{?u.60, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = if h : i = i✝ then Eq.recOn h (f i) else 0

Tactic:
split

Goal state after:
case isTrue
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : i = i✝
⊢ f i✝ = Eq.recOn h✝ (f i)

case isFalse
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : ¬i = i✝
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
i' : ι
j' : α i'
⊢ ((single ⟨i, j⟩ x).sigmaCurry i') j' = ((single i (single j x)) i') j'

Tactic:
sigmaCurry_apply

Goal state after:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
i' : ι
j' : α i'
⊢ (single ⟨i, j⟩ x) ⟨i', j'⟩ = ((single i (single j x)) i') j'