mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.biUnion Iic).sup (disjointed f) = (univ.biUnion Iic).sup f

Tactic:
sup_biUnion,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.sup fun x ↦ (Iic x).sup (disjointed f)) = (univ.biUnion Iic).sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.sup fun x ↦ (Iic x).sup (disjointed f)) = (univ.biUnion Iic).sup f

Tactic:
sup_biUnion,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ (univ.sup fun x ↦ (Iic x).sup (disjointed f)) = univ.sup fun x ↦ (Iic x).sup f
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ toZ i0 (succ^[n] i0) = ↑n

Tactic:
suffices IsMax (succ^[n] i0) from absurd this hn

Goal state after:
case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : ¬m = n
⊢ IsMax (succ^[n] i0)
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n

Tactic:
by
  rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]

Goal state after:
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
⊢ IsIdempotentElem (a + b - a * b)

Tactic:
simp only [IsIdempotentElem, h.eq, mul_sub, mul_add, sub_mul, add_mul, ha.eq,
    mul_assoc, add_sub_cancel_right, hb.eq, hb.mul_self_mul, add_sub_cancel_left, sub_right_inj]
  rw [← h.eq, ha.mul_self_mul, h.eq, hb.mul_self_mul, add_sub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * x + a * y + (b * y - a * y) = x✝¹

Tactic:
add_add_sub_cancel,

Goal state after:
α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * x + b * y = x✝¹
Module: Mathlib.Data.Nat.Choose.Sum

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

Tactic:
rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ Ideal.span {1 - (1 - e)} = Ideal.span {e}

Tactic:
sub_sub_cancel

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ Ideal.span {e} = Ideal.span {e}
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (x 0) + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) x) =
    Finsupp.single 0 (y 0) + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) y)

Tactic:
← f.fst_prodOfFinsuppNat,

Goal state after:
case inr.h
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (f.prodOfFinsuppNat x).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) x) =
    Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) y)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
| h n ih =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
⊢ ∀ {x y : Set ℕ}, x ∈ range Ici → y ∈ range Ici → ∃ z ∈ range Ici, z ⊆ x ∩ y

Tactic:
by
        rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
        exact ⟨Ici (max n m), mem_range_self _, Ici_inter_Ici.symm.subset⟩

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

Goal state before:
pp: α : Type u
f g : Filter α
⊢ Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t

Tactic:
by
  simp only [disjoint_iff, ← empty_mem_iff_bot, mem_inf_iff, inf_eq_inter, bot_eq_empty,
    @eq_comm _ ∅]

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 : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ t ∈ ⨅ i ∈ dom, l i ↔ ∃ i, (i.1 ∈ dom ∧ p i.1 i.2) ∧ s i.1 i.2 ⊆ t

Tactic:
rw [mem_biInf_of_directed h hdom, Prod.exists]

Goal state after:
α : Type u_1
ι : Type u_6
ι' : Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, ((a, b).1 ∈ dom ∧ p (a, b).1 (a, b).2) ∧ s (a, b).1 (a, b).2 ⊆ t
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 : ι → ι' → Set α
p : ι → ι' → 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'.1 ∈ dom ∧ p ii'.1 ii'.2) fun ii' ↦ s ii'.1 ii'.2

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

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

Goal state before:
pp: ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ i, f i ∈ range f
⊢ ⋃ i, Ici (f i) = Ici (⨅ i, f i)

Tactic:
by
  simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
    iUnion_exists, iUnion_iUnion_eq']

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

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)

Goal state after:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b, ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ b, ∀ (a : α), a₀ ≤ a → r a b

Tactic:
eventually_atTop,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b a, ∀ (b_1 : α), a ≤ b_1 → r b_1 b) ↔ ∃ a, ∀ (b : α), a ≤ b → ∃ b_1, ∀ (a : α), b ≤ a → r a b_1
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G
  let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm
  let e : G ≃ ULift (Fin n) := e.trans f
  let groupH : Group (ULift (Fin n)) := e.symm.group
  exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₁ • b₁ = a₂ • b₂

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₁ • b₁ = a₂ • b₂

Tactic:
rintro ⟨rfl, rfl⟩; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosMono α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • _b ≤ a₂ • _b

Tactic:
rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
    exact smul_le_smul_of_nonneg_right (β := β) ha <| neg_nonneg.2 hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ a • b₂ ≤ a • b₁

Tactic:
by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
  exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∩ t)

Tactic:
← sInter_pair

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (⋂₀ {s, t})
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∪ t)

Tactic:
by
  simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ)

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
S₁ S₂ : Submodule R V
h₁ : Module.Finite R ↥S₁
h₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)

Tactic:
rw [Finite.iff_fg] at *

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
S₁ S₂ : Submodule R V
h₁ : S₁.FG
h₂ : S₂.FG
⊢ (S₁ ⊔ S₂).FG
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ IsNormal f ↔ StrictMono f ∧ ∀ (o : α), IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a

Tactic:
simp [isNormal_iff', mem_lowerBounds, mem_upperBounds]

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

Goal state before:
pp: ⊢ ∀ (b : Ordinal.{max (u + 1) v}), b ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ b < univ.{u, v}

Tactic:
by
    refine fun b => inductionOn b ?_; intro β s _
    rw [univ, ← lift_umax]; constructor <;> intro h
    · obtain ⟨a, e⟩ := h
      rw [← e]
      refine inductionOn a ?_
      intro α r _
      exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩
    · rw [← lift_id (type s)] at h ⊢
      obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h
      obtain ⟨f, a, hf⟩ := f
      exists a
      induction a using inductionOn with | type α r
      refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
      · exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩
      · refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h
      · intro a'
        obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
        exists b
        simp only [RelEmbedding.ofMonotone_coe]
        simp [e]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
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
⊢ type r ≤ type s

Tactic:
have H₂ a : ∃ b, f (Sum.inr a) = Sum.inr b := by
      generalize hx : f (Sum.inr a) = x
      obtain x | x := x
      · rw [← H₁, f.inj] at hx
        contradiction
      · exact ⟨x, rfl⟩

Goal state after:
α✝ : 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
H₂ : ∀ (a : α), ∃ b, f (Sum.inr a) = Sum.inr b
⊢ type r ≤ type s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{v}
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
by
  obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
  · simp
  · rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

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

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
by
  refine ⟨fun h ↦ (le_add_sub a b).trans (by gcongr), fun h ↦ ?_⟩
  obtain h' | h' := le_or_gt b a
  · rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']
  · simp [sub_eq_zero_of_lt h']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < type r

Tactic:
exact typein_lt_type r i

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

Goal state before:
pp: ⊢ enumOrd univ = id

Tactic:
← range_id

Goal state after:
⊢ enumOrd (range id) = id
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : succ (o.bsup f) ≤ o.blsub f
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ≠ o.bsup f
⊢ False

Tactic:
exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b ≤ a * c + d

Tactic:
mul_le_iff_le_div ha,

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b - c ≤ d / a ↔ a * b ≤ a * c + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ a * b ≤ a * c + d

Tactic:
mul_le_iff_le_div ha,

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ b ≤ (a * c + d) / a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
opow_le_iff_le_log hb hx

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

Goal state before:
pp: x o : Ordinal.{u_1}
⊢ x < ω_ o ↔ x.card < ℵ_ o

Tactic:
← (isInitial_omega o).card_lt_card,

Goal state after:
x o : Ordinal.{u_1}
⊢ x.card < (ω_ o).card ↔ x.card < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
by
  convert! mul_le_mul_left (Cardinal.one_le_iff_ne_zero.mpr h) a
  rw [one_mul]

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
max_le_iff

Goal state after:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inl
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a

Tactic:
mul_eq_max_of_aleph0_le_left ha hb,

Goal state after:
case refine_2.inl
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ max a b = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
have hbl := isSuccLimit_of_isPrincipal_mul hb₂ hb

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ a * b ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Tactic:
max_le_iff

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

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ o.cof.ord

Tactic:
by rw [hf.ord_cof, ← hg.ord_cof]; exact a.ord_cof_le

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

Goal state before:
pp: case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ max (⨆ i, f i) c ≤ ⨆ i, f i + c

Tactic:
max_le_iff

Goal state after:
case inr
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c
bdd : BddAbove (range fun x ↦ f x + c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ ⨆ i, f i ≤ ⨆ i, f i + c ∧ c ≤ ⨆ i, f i + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ max (⨆ i, f i) c ≤ ⨆ i, f i * c

Tactic:
max_le_iff

Goal state after:
case pos.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : BddAbove (range f)
this : ∀ (i : ι), f i * c ≤ (⨆ i, f i) * c
bdd : BddAbove (range fun x ↦ f x * c)
hs : ℵ₀ ≤ ⨆ i, f i
⊢ ⨆ i, f i ≤ ⨆ i, f i * c ∧ c ≤ ⨆ i, f i * c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj

Tactic:
rcases lt_or_eq_of_le hij with (hij | rfl)
  · exact (hf.2.1 hi hj hij).le
  · rfl

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ (o + 1)).IsRegular

Tactic:
rw [← succ_aleph]

Goal state after:
o : Ordinal.{u_1}
⊢ (succ (ℵ_ o)).IsRegular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord

Tactic:
rw [lt_ord, pow_two, card_mul, card_omega0, aleph0_mul_aleph0]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
obtain h2 | (h2 : y i = 0) := ys.prop i

Goal state after:
case inr.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : i ∈ ↑ys
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : y i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ (↑s).toFinset ∧ { toFun := f, support' := Trunc.mk s } i ≠ 0 ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0

Tactic:
Multiset.mem_toFinset,

Goal state after:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ ↑s ∧ { toFun := f, support' := Trunc.mk s } i ≠ 0 ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a✝ : (i : ι) → α i
⊢ finChoice ⟦a✝⟧.eval = ⟦a✝⟧

Tactic:
exact finChoice_eq _

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

Goal state before:
pp: case refine_1
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange f hf x = single i u
⊢ ∃ a, f i a = u

Tactic:
exact ⟨x i, by simpa using congr($hx i)⟩

Goal state after: