mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
apply_ite (fun n ↦ (a, b) ∈ n),

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ if m ≤ n then (a, b) ∈ {(m, n - m)} else (a, b) ∈ ∅
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: n : ℕ
⊢ (∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ i ∈ range n, (n - 1 - i)

Tactic:
sum_range_reflect (fun i => i) n,

Goal state after:
n : ℕ
⊢ (∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ j ∈ range n, j
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ map { toFun := Prod.swap, inj' := ⋯ } (antidiagonal n) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
antidiagonal_eq_map,

Goal state after:
n : ℕ
⊢ map { toFun := Prod.swap, inj' := ⋯ } (map { toFun := fun i ↦ (i, n - i), inj' := ⋯ } (range (n + 1))) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
β : Type v
F : Type w
R : Type ?u.7
M : Type ?u.9
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m m' : M
⊢ 0 • m = 0 • m'

Tactic:
zero_smul

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

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ (Quotient.ringCon I).toSetoid ((fun x1 x2 ↦ x1 * x2) b a) 1

Tactic:
simp only [Submodule.quotientRel_def]

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ b * a - 1 ∈ I
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
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
zero_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 = 0
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
h : IsGLB s a
⊢ ⋃ x ∈ s, Ioi x = Ioi a

Tactic:
refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ioi_subset_Ioi (h.1 hx)
  · rcases h.exists_between hx with ⟨y, hys, _, hyx⟩
    exact mem_biUnion hys hyx

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
b : ι
hy : y ∈ (f b).sets
c : ι
ha : f a ≥ f c
hb : f b ≥ f c
⊢ ∃ i, x ∩ y ∈ (f i).sets

Tactic:
exact ⟨c, inter_mem (ha hx) (hb hy)⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ (((fun x1 x2 ↦ x1 ∘ x2) '' w).seq v).seq t ∈ h.seq (g.seq x)

Tactic:
rw [← Set.seq_seq]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ w.seq (v.seq t) ∈ h.seq (g.seq x)
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✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 • b < a • b

Tactic:
zero_smul

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 < a • b
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✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0 • b

Tactic:
zero_smul

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : a • b < 0
hb : 0 ≤ b
⊢ a • b < 0
Module: Mathlib.Algebra.Order.Module.Defs

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

Tactic:
zero_smul

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0
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
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
⊢ u.sup id ≤ sSup (sp '' ↑s)

Tactic:
Finset.sup_id_eq_sSup

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
⊢ sSup ↑u ≤ sSup (sp '' ↑s)
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 α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁

Tactic:
by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
  exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)

Tactic:
exact hs.compl.union hDL ht.compl

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
by
  rw [(pred_le_self o).lt_iff_ne]
  exact pred_eq_iff_isSuccPrelimit.not

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}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
⊢ ⟦{ α := γ, r := t, wo := wo✝ }⟧ * ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤
    ⟦{ α := γ, r := t, wo := wo✝ }⟧ * ⟦{ α := β, r := s, wo := wo✝¹ }⟧

Tactic:
refine
        (RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, a.2)) fun a b h => ?_).ordinal_type_le

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b✝ : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a b : α × γ
h : Prod.Lex r t a b
⊢ Prod.Lex s t (f a.1, a.2) (f b.1, b.2)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
· use a + 1
    simpa [upperBounds]

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

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u_3}
⊢ sSup (range fun i ↦ f i) ≤ sSup ((fun x ↦ x + 1) '' range f)

Tactic:
exact sSup_le_sSup_add_one _

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

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ range (enumOrd s) = range f

Tactic:
range_enumOrd hs,

Goal state after:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ s = range f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
rw [iSup, PrincipalSeg.range_eq]

Goal state after:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n + 1 ≤ o.card ↔ succ ↑n ≤ o

Tactic:
← Nat.cast_add_one,

Goal state after:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑(n + 1) ≤ o.card ↔ succ ↑n ≤ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
← mul_le_iff_le_div b0,

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccLimit b
⊢ (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    ⨆ x, limitRecOn (↑x) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯

Tactic:
limitRecOn_limit _ _ _ _ hb

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

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

Tactic:
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a = 1 ∨ b = 0 → a ^ b = 1

Tactic:
simp +contextual [or_imp]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
⊢ IsNormal (derivFamily f)

Tactic:
refine IsNormal.of_succ_lt (fun o ↦ ?_) @fun o h ↦ ?_
  · rw [derivFamily_succ, ← succ_le_iff]
    exact le_nfpFamily _ _
  · rw [derivFamily_limit _ h, Set.image_eq_range]
    have := h.nonempty_Iio.to_subtype
    exact isLUB_ciSup bddAbove_of_small

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

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

pp: case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
· rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

Goal state after:
case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) b = a * ω + b

Tactic:
revert b

Goal state after:
a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x ↦ a + x) b = a * ω + b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (typeLT α)

Tactic:
← hα

Goal state after:
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ ω ≤ x ∧ x.IsInitial

Tactic:
by
  rw [range_omega, mem_ofPred]

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

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
⊢ deriv (fun x ↦ a * x) b = a ^ ω * b

Tactic:
revert b

Goal state after:
a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun x ↦ a * x) b = a ^ ω * b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ

Tactic:
rw [cof_type, Order.cof_eq_one_iff, type_lt_mem_range_succ_iff]

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o

Tactic:
by
  rw [aleph0_le_cof_iff, one_lt_cof_iff]

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

Goal state before:
pp: α : 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})
⊢ typeLT ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a}) ≤ (Order.cof α).ord

Tactic:
← hs',

Goal state after:
α : 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})
⊢ typeLT ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a}) ≤ (#↑s).ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ max (max a b) ℵ₀

pp: case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
· rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _

Goal state after:
case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof ↑s).ord
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord

Tactic:
cof_eq_of_isCofinal hs

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ (Order.cof α).ord.cof = Order.cof α

Tactic:
← hs',

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ (typeLT ↑s).cof = Order.cof α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ Order.cof ↑s = Order.cof α

Tactic:
cof_eq_of_isCofinal hs

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ Order.cof α = Order.cof α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr.inr.inr
b : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b))
ho₂ : 2 < (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b)
⊢ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ≤ 2 ∨ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
exact Or.inr ⟨b, rfl⟩

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

Goal state before:
pp: β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
by
  have : StrictMono (β := Iio (⨆ i, f i + 1)) (fun i ↦ ⟨f i, ?_⟩) := fun x y h ↦ hf h
  · have := lift_cof_congr_of_strictMono this ?_
    · rw [← Cardinal.lift_inj.{_, max (u + 1) v}, Cardinal.lift_lift.{_, _, v},
        Cardinal.lift_umax.{_, u + 1}, Cardinal.lift_umax.{_, u + 1}, this]
      simp
    · intro ⟨b, hb⟩
      rw [mem_Iio, Ordinal.lt_iSup_add_one_iff] at hb
      obtain ⟨i, hi⟩ := hb
      exact ⟨_, Set.mem_range_self i, hi⟩
  · rw [mem_Iio]
    exact (lt_add_one _).trans_le <| le_ciSup bddAbove_of_small _

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lsub f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
← lift_id'.{u} (lsub f),

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub f)).cof ≤ Cardinal.lift.{v, u} #ι
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ o)

Tactic:
· intro a b ha hb
    rw [lt_omega_iff_card_lt] at ha hb ⊢
    apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))
    rwa [← aleph_zero, aleph_lt_aleph]

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
| #(β' ↪ α)

Tactic:
rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
| #(β' ↪ α × α)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (typeLT α)

Tactic:
← hα

Goal state after:
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ IsSuccPrelimit (#α).ord
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
⊢ #α < #α ^ (Order.cof α).ord.card

Tactic:
← hs',

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 ↑s).card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
      if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) =
    ⟨s, ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
        if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) =
    ↑⟨s, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ⟨t, ⋯⟩ = ⟨t', ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t ↦ Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ↑⟨t, ⋯⟩ = ↑⟨t', ⋯⟩
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine AddSubmonoid.mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

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

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

Tactic:
subst i

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ (finChoice fun x ↦ ⟦a x⟧).eval = fun x ↦ ⟦a x⟧

Tactic:
rw [finChoice_eq]; rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
H : f.support = ∅
⊢ ∀ (i : ι), f i = 0 i

Tactic:
simpa [Finset.ext_iff] using H

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

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ (single i b).prod h✝ = h✝ i b

Tactic:
simp [h, h_zero]

Goal state after:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
⊢ f.sigmaUncurry.sigmaCurry = f

Tactic:
by
    ext i j
    rw [sigmaCurry_apply, sigmaUncurry_apply]

Goal state after: