mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : α
⊢ (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
simp only [h.mem_iff, exists_imp, and_imp]

Goal state after:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : Zero B
inst✝ : SMulZeroClass M B
this : Zero A := e.zero
⊢ ∀ (a : M), a • 0 = 0

Tactic:
simp [smul_def, zero_def]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝² : Zero M₀
inst✝¹ : Zero B
inst✝ : SMulWithZero M₀ B
this : Zero A := e.zero
⊢ ∀ (m : A), 0 • m = 0

Tactic:
simp [smul_def, zero_def]

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

Goal state before:
pp: case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
refine ⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩

Goal state after:
case mp
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
⊢ span A (range (f ∘ ULift.down)) = N
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
⊢ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s'' : Finset M
hs'' : span R ↑s'' = span R s
s' : Finset M
hs's : ↑s' ⊆ s
hss' : ↑s'' ⊆ ↑(span R ↑s')
⊢ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'
Module: Mathlib.Algebra.Module.Congruence.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ f (r • x✝¹) = f (r • x✝)

Tactic:
map_smulₛₗ,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : f x✝¹ = f x✝
⊢ φ r • f x✝¹ = φ r • f x✝
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ 1 < cof α ↔ NoTopOrder α

Tactic:
rw [← not_iff_not, not_lt, noTopOrder_iff, cof_le_one_iff]
  simp

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy : y ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ y ∈ f ⁻¹' Iic x

Tactic:
obtain hy | rfl := hy.lt_or_eq

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
y : α
hy✝ : y ∈ Iic (sSup (f ⁻¹' Iic x))
hy : y < sSup (f ⁻¹' Iic x)
⊢ y ∈ f ⁻¹' Iic x

case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x
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)
⊢ ¬f (succ (sSup (f ⁻¹' Iic x))) ≤ x

Tactic:
hf.le_iff_le_sSup ⟨⊥, hx⟩ H,

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)
⊢ ¬succ (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', c = lift.{max (u + 1) v, u} c'

Tactic:
let ⟨a, h', e⟩ := lt_lift_iff.1 h

Goal state after:
c : Cardinal.{max (u + 1) v}
h : c < univ.{u, v}
a : Cardinal.{u + 1}
h' : a < #Ordinal.{u}
e : lift.{v, u + 1} a = c
⊢ ∃ c', c = lift.{max (u + 1) v, u} c'
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: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
have := type_ne_zero_iff_nonempty.1 h

Goal state after:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h ≠ iSup (o.familyOfBFamily f)
a : Ordinal.{max u v}
⊢ a < iSup (o.familyOfBFamily f) → succ a < iSup (o.familyOfBFamily f)

Tactic:
exact succ_lt_iSup_of_ne_iSup fun i => hf _

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

Goal state before:
pp: case type
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s

Tactic:
exact mul_le_of_limit_aux h H

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

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ a ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨o, ⋯⟩

Tactic:
← enum_typein (α := (succ o).ToType) (· < ·) a,

Goal state after:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a, ⋯⟩ ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨o, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
H : ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o

Tactic:
simpa only [typein_enum] using H (enum r ⟨i, h⟩)

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

Goal state before:
pp: case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
simp at hi

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

Goal state before:
pp: case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa

Goal state after:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ ∀ a < o, f a < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
· refine eq_of_forall_ge_iff fun d ↦ ?_
    rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]

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

Goal state before:
pp: b n : ℕ
⊢ b ^ 1 ≤ n ∧ n < b ^ (1 + 1) ↔ b ≤ n ∧ n < b * b

Tactic:
Nat.pow_add,

Goal state after:
b n : ℕ
⊢ b ^ 1 ≤ n ∧ n < b ^ 1 * b ^ 1 ↔ b ≤ n ∧ n < b * b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
mod_def,

Goal state after:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ x * y + z - x * ((x * y + z) / x) = z % x
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:
mod_def,

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

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n / 2 * 2) = log 2 n + 1

Tactic:
bit_div_two,

Goal state after:
b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (n * 2) = log 2 n + 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_total m n with h | h

Goal state after:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m < n * (m / n).succ

Tactic:
mul_comm,

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m < (m / n).succ * n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ type LT.lt = ↑x

Tactic:
type_fintype,

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ ↑(Fintype.card ↑(Iio x)) = ↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ type LT.lt = ↑↑x

Tactic:
type_fintype,

Goal state after:
n : ℕ
x : Fin n
⊢ ↑(Fintype.card ↑(Iio x)) = ↑↑x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o < ℵ₀.ord ↔ ∃ n, o = ↑n

Tactic:
Cardinal.lt_ord,

Goal state after:
o : Ordinal.{u_4}
⊢ o.card < ℵ₀ ↔ ∃ n, o = ↑n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < if 1 < b ∧ 1 < n then (clog.go n b n).snd + 1 else 0

Tactic:
if_pos

Goal state after:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < (clog.go n b n).snd + 1

case hc
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 1 < b ∧ 1 < n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
h : b ≤ 1
x : Ordinal.{u_1}
⊢ log b x = 0

Tactic:
by
  obtain rfl | rfl := le_one_iff.1 h
  · apply (csSup_of_not_bddAbove _).trans csSup_empty
    by_contra! hb
    refine not_bddAbove_Ici 1 (hb.mono fun a ↦ ?_)
    simp +contextual [one_le_iff_ne_zero]
  · simp_rw [log, one_opow, preimage_const]
    split_ifs <;> simp

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

Goal state before:
pp: case mpr.inl
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

pp: case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
· exact (h₂ b hab).trans_lt <| H b hb

Goal state after:
case mpr.inr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ω_ 0 = ω

Tactic:
omega_eq_preOmega,

Goal state after:
⊢ preOmega (ω + 0) = ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preOmega ω = ω

Tactic:
preOmega_omega0

Goal state after:
⊢ ω = ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
omega_eq_preOmega,

Goal state after:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ preOmega (ω + (a - ω)) = preOmega a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
⊢ #α * #α ≤ #α

Tactic:
let s := f ⁻¹'o (· < ·)

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
omega_eq_preOmega,

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = preOmega (ω + o)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
mul_comm,

Goal state after:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max a b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = max a b

Tactic:
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
  · exact mul_eq_max_of_aleph0_le_left ha' hb
  · exact mul_eq_max_of_aleph0_le_right ha hb'

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

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

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

Tactic:
· rw [mul_eq_max_of_aleph0_le_left ha hb0]
    exact le_max_left _ _

Goal state after:
case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀
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) ℵ₀

Tactic:
mul_comm,

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

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

Tactic:
mul_comm,

Goal state after:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ b * a = b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
⊢ b = c

Tactic:
by
  rcases le_or_gt ℵ₀ b with hb | hb
  · have : a < b := ha.trans_le hb
    rw [add_eq_right hb this.le, eq_comm] at h
    rw [eq_of_add_eq_of_aleph0_le h this hb]
  · have hc : c < ℵ₀ := by
      rw [← not_le]
      intro hc
      apply lt_irrefl ℵ₀
      apply (hc.trans (self_le_add_left _ a)).trans_lt
      rw [← h]
      apply add_lt_aleph0 ha hb
    rw [lt_aleph0] at *
    rcases ha with ⟨n, rfl⟩
    rcases hb with ⟨m, rfl⟩
    rcases hc with ⟨k, rfl⟩
    norm_cast at h ⊢
    apply add_left_cancel h

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
⊢ sSup ((fun x ↦ x + 1) '' s) < a

Tactic:
by
  let f := OrderIso.ofRelIsoLT (enum (α := s) (· < ·))
  have : Small.{u} (Iio (typeLT s)) := by
    refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_
    simp [Subtype.val_inj]
  have : range (fun i ↦ (f i).1 + 1) = (· + 1) '' s := by
    convert! range_comp (· + 1) (fun i ↦ (f i).1)
    rw [range_comp', f.range_eq]
    simp
  rw [← this, sSup_range]
  apply lt_of_le_of_ne
  · simp [hs]
  · rintro rfl
    rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
      Cardinal.lift_lift, Cardinal.lift_lt] at ha
    exact ha.not_ge (cof_le_cardinalMk _)

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ c * ⨆ i, f i = ⨆ i, c * f i

Tactic:
mul_comm,

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ (⨆ i, f i) * c = ⨆ i, c * f i
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c.ord

Tactic:
Cardinal.lt_ord,

Goal state after:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ card 0 < c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // Bounded r s } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = #α

case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s // Bounded r s } = #α
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
⊢ ⨆ s, #↑↑s < c

Tactic:
apply Cardinal.iSup_lt_of_lt_cof_ord (mk_range_le.trans_lt _)

Goal state after:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ∀ (i : ↑(range fun i ↦ t i)), #↑↑i < c

c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #ι < c.ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α = 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ⨆ a_1, 2 ^ preBeth ↑a_1 < c

Tactic:
apply lift_iSup_lt_of_lt_cof_ord _ _

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1, u_1 + 1} #↑(Iio a) < (lift.{u_1 + 1, u_1} c).ord.cof

c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
i' : LinearIndepOn R id (range v')
⊢ False

Tactic:
exact r'' (m (range v') i' r)

Goal state after:
Module: Mathlib.Data.List.Pi

Goal state before:
pp: case nil
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
fs : (i : ι) → List (α i)
i : ι
hi : i ∈ 0
⊢ Multiset.Pi.empty α i hi = Pi.nil α i hi

Tactic:
simp at hi

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x // x ≠ 0 }
⊢ (fun x ↦
        match (motive := { f // f.support = s } → (i : ↥s) → { x // x ≠ 0 }) x with
        | ⟨f, hf⟩ => fun x ↦
          match x with
          | ⟨i, hi⟩ => ⟨f i, ⋯⟩)
      ((fun f ↦ ⟨mk s fun i ↦ ↑(f i), ⋯⟩) f) =
    f

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x // x ≠ 0 }
⊢ (fun x ↦
        match (motive := { f // f.support = s } → (i : ↥s) → { x // x ≠ 0 }) x with
        | ⟨f, hf⟩ => fun x ↦
          match x with
          | ⟨i, hi⟩ => ⟨f i, ⋯⟩)
      ((fun f ↦ ⟨mk s fun i ↦ ↑(f i), ⋯⟩) f) =
    f
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s).dualAnnihilator = {f | s ⊆ ↑f.ker}

Tactic:
by
  ext f
  simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_ofPred_eq, ← LinearMap.mem_ker]
  exact span_le

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
f : (i : ι) → M i →ₗ[R] N
i : ι
x : M i
⊢ (coprodMap f) (single i x) = (f i) x

Tactic:
simp [coprodMap]

Goal state after: