mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ ↑(insert (succ b) (Ioc a b)) = ↑(Ioc a (succ b))

Tactic:
by simpa using Set.insert_Ioc_right_eq_Ioc_succ h

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
τ : Type u_4
π : τ → Type u_5
inst✝ : (t : τ) → SemilatticeSup (π t)
f : ι → (t : τ) → π t
i : ι
t : τ
⊢ (partialSups f) i t = (partialSups fun x ↦ f x t) i

Tactic:
by
  simp only [partialSups_apply, Finset.sup'_apply]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i : ι
⊢ ∃ j ≤ i, (partialSups f) i = f j

Tactic:
obtain ⟨j, hj_mem, hj_le⟩ : ∃ j ∈ Finset.Iic i, ∀ k ∈ Finset.Iic i, f k ≤ f j :=
    Finset.exists_max_image _ _ ⟨i, Finset.mem_Iic.mpr le_rfl⟩

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : LinearOrder α
f : ι → α
i j : ι
hj_mem : j ∈ Iic i
hj_le : ∀ k ∈ Iic i, f k ≤ f j
⊢ ∃ j ≤ i, (partialSups f) i = f j
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H →+ I
hf' : ∀ (x : H × I), (∃ x_1, f x_1 = x) ↔ f' x.1 = x.2
⊢ ∀ (m : S) (x : H), (↑f').toFun (m • x) = (RingHom.id S) m • (↑f').toFun x

Tactic:
intro s h
      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, RingHom.id_apply]
      refine (hf' (s • h, _)).mp ?_
      rw [← Prod.smul_mk, ← LinearMap.mem_range]
      apply Submodule.smul_mem
      rw [LinearMap.mem_range, hf']

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
⊢ ∀ x_1 ∈ Set.Ioi i, x ≤ x_1

Tactic:
intro y

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
⊢ y ∈ Set.Ioi i → x ≤ y
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x, ∏ x_1 > x, f x x_1 = ∏ x, ∏ x_1 < x, f x_1 x

Tactic:
rw [prod_sigma', prod_sigma']

Goal state after:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ toZ i0 i0 = 0

Tactic:
rw [toZ_of_ge le_rfl]
  norm_cast
  rw [← nonpos_iff_eq_zero]
  apply Nat.find_le
  rw [Function.iterate_zero, id]

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
nth_rw 2 [← hmn]
    rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]
    rw [neg_neg]
    exact Int.natCast_nonneg _

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Tactic:
rw [prod_sigma', prod_sigma']

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m ↦ range (n - m), f x.fst x.snd
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : r ^ 0 ∈ I
⊢ r ∈ I

Tactic:
rw [pow_zero] at H
    exact hI.one_notMem.elim H

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ IsIdempotentElem (1 - a)

Tactic:
rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift I f H)

Tactic:
intro y

Goal state after:
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
y : S
⊢ ∃ a, (lift I f H) a = y
Module: Mathlib.Data.Nat.Choose.Sum

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

Tactic:
intro y

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
⊢ y ∈ x.powerset → #y ∈ range (#x + 1)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
← h.isBasis.filter_eq_generate,

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = ⋯.filter
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (∑ i, mapDomain f (Finsupp.single i (s i))) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
simp [Finset.sum_filter]

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ ∑ c, (Finsupp.single (f c) (s c)) y = ∑ a, if f a = y then s a else 0
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ kernImage m univ = univ

Tactic:
simp [kernImage_eq_compl]

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ (⨅ i ∈ dom, l i).HasBasis (fun ii' ↦ ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' ↦ s ii'.fst ii'.snd

Tactic:
by
  refine ⟨fun t => ?_⟩
  rw [mem_biInf_of_directed h hdom, Sigma.exists]
  grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
by
  simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
simpa only [exists_prop, subset_inter_iff] using
      hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂

Tactic:
by
  filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsCancelMul β
this : Mul α := e.mul
⊢ IsCancelMul α

Tactic:
exact e.injective.isCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Cofinal

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

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

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
P Q R : { P // P.FG }
hPR : ↑P ≤ ↑R
hQR : ↑Q ≤ ↑R
⊢ ↑⟨↑P ⊔ ↑Q, ⋯⟩ ≤ ↑R

Tactic:
exact sup_le hPR hQR

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ a ∈ s → (d ∩ s).Nonempty

Tactic:
hd₃

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
⊢ (d ∩ s).Nonempty
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α ≤i β
a✝ : α
ha : IsSuccLimit a✝
⊢ f a✝ ∈ lowerBounds (upperBounds (⇑f '' Iio a✝))

Tactic:
by
    rw [f.image_Iio]
    exact (f.map_isSuccLimit ha).isLUB_Iio.2

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

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

Tactic:
← StrictMono.range_inj H hf

Goal state after:
case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ range (Subtype.val ∘ ⇑(enum (range f) hs)) = range f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ lift.{max v u, v} ((typein r).toRelEmbedding f.top) = type s

Tactic:
lift_typein_top,

Goal state after:
case h
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ lift.{v, max u v} (type s) = type s
Module: Mathlib.Logic.Small.List

Goal state before:
pp: α : Type v
inst✝ : Small.{u, v} α
⊢ Small.{u, v} (List α)

Tactic:
let e : (Σ n, List.Vector α n) ≃ List α := Equiv.sigmaFiberEquiv List.length

Goal state after:
α : Type v
inst✝ : Small.{u, v} α
e : (n : ℕ) × List.Vector α n ≃ List α := Equiv.sigmaFiberEquiv List.length
⊢ Small.{u, v} (List α)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) ⊆ range (succ ∘ g)

Tactic:
convert! Set.image_mono h <;> apply Set.range_comp

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b

Tactic:
isSuccLimit_add_iff

Goal state after:
a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
Subtype.forall

Goal state after:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : IsSuccLimit b
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ (x * y + w) % (x * z) = x * (y % z) + w

Tactic:
rw [mod_def, mul_add_div_mul hw]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ⨆ n, o * ↑n = o * ω

Tactic:
rw [← iSup_natCast, Ordinal.mul_iSup]

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

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

Tactic:
by
  rcases eq_or_ne o 0 with (rfl | ho)
  · exact log_zero_right b
  rcases le_or_gt b 1 with hb | hb
  · rcases le_one_iff.1 hb with (rfl | rfl)
    · exact log_zero_left o
    · exact log_one_left o
  · rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]

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

Goal state before:
pp: case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
← fp_iff_derivFamily H

Goal state after:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∀ (i : ι), f i a = a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ω ^ c * ↑n ≤ ω ^ b * ↑n

Tactic:
lt_succ_iff.1 hc

Goal state after:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ ω ^ b * ↑n ≤ ω ^ b * ↑n

case hc
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * ↑n
⊢ 0 < ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Tactic:
rwa [← add_assoc, ← mul_one_add, one_add_omega0]

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

Goal state before:
pp: case inl
ho : 0 ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

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

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ b + (c - b) = b + (c - b)

Tactic:
Ordinal.add_sub_cancel_of_le hbc

Goal state after:
a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ c = c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

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

Goal state before:
pp: case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

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

Goal state before:
pp: o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≠ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
by
  rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂
  · exact isPrincipal_add_of_le_one <| lt_two_iff.mp ho₁
  · simp_rw [isPrincipal_add_iff_add_self_lt, ← Ordinal.mul_two]
    exact fun a ha ↦ ho ha ho₂

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
⊢ r ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩

Tactic:
apply (trichotomous_of r _ _).resolve_right

Goal state after:
case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
⊢ ¬(⟨↑x, ⋯⟩ = ⟨↑y, ⋯⟩ ∨ r ⟨↑y, ⋯⟩ ⟨↑x, ⋯⟩)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
lift_id'.{u, v}

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_bsup_le_lift

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = g a

Tactic:
← (g a).xor_false

Goal state after:
case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
lift_id'.{u, v}

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < #α ^ (#α).ord.cof

Tactic:
hα,

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < #α ^ (typeLT α).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #{ t // #↑t ≤ c }

Tactic:
refine ⟨Embedding.subtypeMap ?_ ?_⟩
    · apply Embedding.image
      use Sum.inr
      apply Sum.inr.inj
    intro s hs
    exact mk_image_le.trans hs

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
obtain ⟨g⟩ := id h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ 0 = single j 0

Tactic:
DFinsupp.single_zero

Goal state after:
case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ 0 = 0
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Prop
f : ∀ (a : (i : ι) → α i), C fun x ↦ ⟦a x⟧
q : (i : ι) → Quotient (S i)
⊢ C q

Tactic:
have {m : Multiset ι} (C : (∀ i ∈ m, Quotient (S i)) → Prop) :
      ∀ (_ : ∀ a : ∀ i ∈ m, α i, C (⟦a · ·⟧)) (q : ∀ i ∈ m, Quotient (S i)), C q := by
    induction m using Quotient.ind
    exact list_ind
  exact this (fun q ↦ C (q · (Finset.mem_univ _))) (fun _ ↦ f _) (fun i _ ↦ q i)

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

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (f + g)) i✝ = (comapDomain h hh f + comapDomain h hh g) i✝

Tactic:
add_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
hh : Function.Injective h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (f + g)) i✝ = (comapDomain h hh f) i✝ + (comapDomain h hh g) i✝
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f + comapDomain' h hh' g) i✝

Tactic:
add_apply,

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f) i✝ + (comapDomain' h hh' g) i✝