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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ f ⊓ 𝓟 (range m) = f

Tactic:
inf_eq_left.2 (le_principal_iff.2 hf)

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ f = f
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort w
s : ι → Set α
x : Set α
⊢ x ∈ ⨆ x, 𝓟 (s x) ↔ x ∈ 𝓟 (⋃ i, s i)

Tactic:
by simp only [mem_iSup, mem_principal, iUnion_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂
⊢ Tendsto (fun x ↦ if p x then f x else g x) l₁ l₂

Tactic:
simp only [tendsto_def, mem_inf_principal] at *
  intro s hs
  filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
  rw [mem_preimage]
  split_ifs with h
  exacts [hp₀ h, hp₁ h]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) → ∀ B ∈ F, f x ∈ B

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
⊢ ∀ B ∈ F, f x ∈ B
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
h : ∀ B ∈ F, f x ∈ B
⊢ ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x

Tactic:
simp only [Filter.Frequently, eventually_iSup, not_forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ U ⊆ (map f (generate ((fun x ↦ f ⁻¹' x) '' U))).sets

Tactic:
exact fun u hu ↦ mem_generate_of_mem ⟨u, hu, rfl⟩

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) → IsSuccPrelimit a

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
⊢ IsSuccPrelimit a
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit a → IsSuccPrelimit (f a)

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
⊢ IsSuccPrelimit (f a)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁✝ b₂✝ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ ≠ b₂

Tactic:
by rintro rfl; simp at h

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✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ ≠ a₂

Tactic:
by rintro rfl; simp at h

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

Goal state before:
pp: case mpr
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 := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG

Tactic:
intro h

Goal state after:
case mpr
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 : IsCompactElement s
⊢ s.FG
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:
neg_le_neg_iff

Goal state after:
α : 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₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂ i, f i)

Tactic:
rw [← sInter_range f]

Goal state after:
α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂₀ range f)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂ i, f i)

Tactic:
rw [← sInter_range f]

Goal state after:
α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂₀ range f)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂ i, f i)

Tactic:
by
  rw [← sInter_range f]
  exact DirSupClosed.sInter (by simpa)

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✝ : PosSMulReflectLE α β
h : -(-a • b₁) ≤ -(-a • b₂)
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
neg_le_neg_iff

Goal state after:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁
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:
neg_le_neg_iff

Goal state after:
α : 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₁
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding → type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
intro h

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u}) → type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
intro h

Goal state after:
case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
α✝ : 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
a : α
x : β
hx : f (Sum.inr a) = Sum.inr x
⊢ ∃ b, Sum.inr x = Sum.inr b

Tactic:
· exact ⟨x, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ a = (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩

Tactic:
← enum_typein (α := ToType 1) (· < ·) a

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a, ⋯⟩ =
    (enum fun x1 x2 ↦ x1 < x2) ⟨0, uniqueToTypeOne._proof_2⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)

Tactic:
exact (isSuccLimit_mul_right ha hb).isSuccPrelimit

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

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s → #α ≤ (type s).card

Tactic:
intro h

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ #α ≤ (type s).card → (#α).ord ≤ type s

Tactic:
intro h

Goal state after:
case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
card_le_iff,

Goal state after:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < (succ (Cardinal.lift.{v, u} a)).ord
⊢ b ∈ range lift.{v, u}
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1

Tactic:
apply eq_of_forall_gt_iff
  rintro (_ | c)
  · simp
  · have : n / b ≠ 0 := by simp [*, Nat.ne_zero_of_lt h]
    rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul] <;> grind

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

Goal state before:
pp: α : 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
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
by refine lt_of_le_of_lt ?_ (hlt a mem_cons_self); simpa

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

Goal state before:
pp: case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n ≤ m ∧ m ≤ log b n ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
← Nat.lt_succ_iff,

Goal state after:
case inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ log b n < m.succ ∧ m ≤ log b n ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
⊢ (∀ (a : Ordinal.{u}), f a < f (succ a)) →
    ((∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) ↔
      ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o)

Tactic:
intro h

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) ↔
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
⊢ a ≤ b

Tactic:
rcases h with ⟨b, rfl⟩

Goal state after:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ (b + 1)

Tactic:
simpa using mul_pos IH a0

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

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1

Tactic:
div_eq_of_lt h,

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b 0 = log b n - 1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
⊢ ¬Surjective f

Tactic:
intro h

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬Small.{u, u + 1} ↑sᶜ

Tactic:
intro h

Goal state after:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
⊢ False
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1.inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ b ≤ 1

Tactic:
exact zero_opow_le b

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

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n

Tactic:
div_eq_of_lt h,

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (0 * b) = log b n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1

Tactic:
← Nat.lt_succ_iff,

Goal state after:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b < succ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u + log b v

Tactic:
rw [log_eq_iff hb]

Goal state after:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)

case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * ↑n + a % ω ^ log ω a < a

Tactic:
apply (opow_mul_add_lt_opow_mul _ (lt_add_one _)).trans_le

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * (↑n + 1) ≤ a

a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ a % ω ^ log ω a < ω ^ log ω a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preAleph o ↔ 0 < o

Tactic:
by
  rw [← preAleph_zero, preAleph_lt_preAleph]

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.card ≤ ℵ₀

Tactic:
card_le_iff,

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o < (succ ℵ₀).ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
| isSuccPrelimit o ho IH =>

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

Goal state before:
pp: case pos
ι : 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
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c

Tactic:
have bdd : BddAbove (range (f · * c)) := ⟨_, forall_mem_range.mpr this⟩

Goal state after:
case pos
ι : 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)
⊢ (⨆ i, f i) * c ≤ ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl.inl
n m : ℕ
⊢ (↑n ^ m).card ≤ max ℵ₀ (max (↑n).card (↑m).card)

Tactic:
← natCast_pow,

Goal state after:
case inl.inl
n m : ℕ
⊢ (↑(n ^ m)).card ≤ max ℵ₀ (max (↑n).card (↑m).card)
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
exact isRegular_succ (aleph0_le_aleph o)

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

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

Tactic:
exact ⟨a, hα.trans ha.le⟩

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

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
mk_list_eq_mk

Goal state after:
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((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 })

Tactic:
intro h

Goal state after:
case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
⊢ x ∈
    ↑((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 })
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'

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

Goal state before:
pp: case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

Tactic:
apply Embedding.image

Goal state after:
case refine_1
α : Type u
c : Cardinal.{u}
⊢ α ↪ ULift.{u, 0} ℕ ⊕ α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
hc : (ℵ_ o).IsSingular
⊢ ℵ_ ω ≤ ℵ_ o

Tactic:
isSingular_aleph_iff

Goal state after:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ℵ_ ω ≤ ℵ_ o
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj → i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
intro h

Goal state after:
case mp
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x ↦ x = i) f = single i (f i)

Tactic:
by
  simp [eq_comm]

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (f g.fst) g.snd ≠ 0
⊢ ¬f g.fst = 0

Tactic:
intro h

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
this✝ : DecidableEq ι
this : (i : ι) → DecidableEq (η i →₀ N)
g : (i : ι) × η i
hg : (f g.fst) g.snd ≠ 0
h : f g.fst = 0
⊢ False
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
⊢ ∃ u, f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩

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

Goal state before:
pp: case refine_2.mk
ι : 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
⊢ ∃ a, mapRange f hf a = { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ }

Tactic:
refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩

Goal state after:
case refine_2.mk.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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ i ∈ s ∨ y i = 0

case refine_2.mk.refine_2
ι : 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 : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ (mapRange f hf { toFun := y, support' := Trunc.mk ⟨s, ⋯⟩ }) i =
    { toFun := x, support' := Quot.mk ⇑trueSetoid ⟨s, hs⟩ } i
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✝ : κ
⊢ (f + g) (h i✝) = f (h i✝) + g (h 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✝ : κ
⊢ f (h i✝) + g (h i✝) = f (h i✝) + g (h 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✝ : κ
⊢ (f + g) (h i✝) = f (h i✝) + g (h 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✝ : κ
⊢ f (h i✝) + g (h i✝) = f (h i✝) + g (h i✝)