mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
by
  by_cases h : j = i
  · rw [h, update_self, update_self]
  · rw [update_of_ne h, update_of_ne h]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ f.ker.prod g.ker ≤ (f.coprod g).ker

Tactic:
rintro ⟨y, z⟩
  simp +contextual

Goal state after:
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ ↑(insert (pred a) (Ico a b)) = ↑(Ico (pred a) b)

Tactic:
by simpa using Set.insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
⊢ map (inr R M M₂) q = ⊥.prod q

Tactic:
ext ⟨x, y⟩; simp [and_left_comm, eq_comm, and_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this✝ : Fintype ι
this : x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed f

Tactic:
rw [← disjointed_partialSups, ← hsups, disjointed_partialSups]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed d
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥

Tactic:
Ideal.ne_top_iff_one

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ 1 ∉ I → I = ⊥
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), (n - i) * n.choose i + ∑ i ∈ range (n + 1), i * n.choose i = ∑ i ∈ range (n + 1), n * n.choose i

Tactic:
rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]

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

Goal state before:

Tactic:
2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]

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

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ (fun x_1 ↦ x_1 ^ ((t.attach.sup fun x ↦ n ⟨↑x, ⋯⟩) - n ⟨↑⟨x, hxt⟩, ⋯⟩ + n ⟨↑⟨x, hxt⟩, ⋯⟩)) x ∈
    ↑(span (range fun x ↦ ↑x ^ n x))

Tactic:
simp_rw [pow_add]

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ↑s → ℕ
t : Finset α
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span α ↑t
x : α
hxt : x ∈ ↑t
⊢ x ^ ((t.attach.sup fun x ↦ n ⟨↑x, ⋯⟩) - n ⟨x, ⋯⟩) * x ^ n ⟨x, ⋯⟩ ∈ ↑(span (range fun x ↦ ↑x ^ n x))
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
p : ι → Prop
s : ι → Set α
h : IsBasis p s
i : ι
hi : p i
j : ι
hj : p j
k : ι
hk : p k
hk' : s k ⊆ s i ∩ s j
⊢ ∃ z ∈ {t | ∃ i, p i ∧ s i = t}, z ⊆ s i ∩ s j

Tactic:
exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

Tactic:
mem_comap_iff_compl,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ (f '' sᶜᶜ)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
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
⊢ ∃ i, x ∩ y ∈ (f i).sets

Tactic:
rcases h a b with ⟨c, ha, hb⟩

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
have : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty

Goal state after:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Tactic:
by
  simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
⊢ SurjOn (map m) (Iic F) (Iic G)

Tactic:
have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) :=
      fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
this : RightInvOn (fun x ↦ F ⊓ comap m x) (map m) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G)
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e✝ e : α ≃ β
inst✝ : Mul β
x✝ : Mul α := e.mul
⊢ α ≃* β

Tactic:
exact
    { e with
      map_mul' := fun x y => by
        simp [mul_def] }

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this✝ : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ False

Tactic:
apply Filter.empty_notMem l

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this✝ : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ ∅ ∈ l
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
⊢ a • 0 < a • b

Tactic:
rwa [smul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
⊢ a • b < a • 0

Tactic:
rwa [smul_zero]

Goal state after:
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]

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case h.a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ M' ≤ N (S.attach.sup f)

Tactic:
rw [← hS, span_le]
    intro s hs
    exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)

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]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
neg_nonneg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u_4}
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
by simpa only [le_antisymm_iff, add_le_add_iff_left] using h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
nth_rw 1 [← enum_typein r x]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r ((enum r) ⟨(typein r).toRelEmbedding x, ⋯⟩) ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.ToType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ a

Tactic:
rw [← familyOfBFamily_enum o f]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.ToType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ o.familyOfBFamily f ((enum fun x1 x2 ↦ x1 < x2) ⟨i, ⋯⟩) ≤ a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g

Tactic:
← hj'

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ g j hj ≤ o'.bsup g
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α

Tactic:
rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff_mem_range_succ,
    type_lt_mem_range_succ_iff]

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsMax x) ↔ ¬∀ (x : α), ¬IsMax x
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: ⊢ enumOrd univ = id

Tactic:
rw [← range_id]

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f

Tactic:
refine ⟨fun h => ?_, fun hf => le_antisymm (iSup_le_lsub f) (lsub_le fun i => ?_)⟩
  · rw [← h]
    exact fun a => succ_lt_iSup_of_ne_iSup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne
  by_contra! hle
  have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩
  have :=
    hf _
      (by
        rw [← heq]
        exact lt_succ (iSup f))
  rw [heq] at this
  exact this.false

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (#↑s).ord < type r

Tactic:
grw [← ord_le_type, ord_lt_ord, ← mk_univ (α := α)]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ #↑s < #↑univ
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c

Tactic:
exact le_antisymm (div_le hb |>.mpr hlt) (mul_le_iff_le_div hb |>.mp hle)

Goal state after:
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]
  exact fun a _ => H.strictMono (lt_succ a)

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

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

Tactic:
rw [bddAbove_iff_small]

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

Goal state before:
pp: case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
induction c using limitRecOn with
    | zero => simp
    | add_one c IH => simpa using mul_le_mul' IH ab
    | limit c l IH =>
      exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
        (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)

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

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

Tactic:
rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]

Goal state after:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ clog b n ≤ clog b m

Tactic:
clog_of_left_le_one hb

Goal state after:
case inl
b n m : ℕ
h : n ≤ m
hb : b ≤ 1
⊢ 0 ≤ clog b m
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
  · apply le_antisymm _ (le_pow_clog hb n)
    apply le_of_lt_succ
    exact (lt_clog_iff_pow_lt hb).mp H
  · rw [lt_clog_iff_pow_lt hb, H]
    exact n.lt_add_one

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

Goal state before:
pp: case inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ log ↑m ↑n = ↑(Nat.log m n)

Tactic:
log_eq_iff (mod_cast hm) (mod_cast hn)

Goal state after:
case inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ ↑m ^ ↑(Nat.log m n) ≤ ↑n ∧ ↑n < ↑m ^ (↑(Nat.log m n) + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) b = a * ω

Tactic:
by
  apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
  · rw [← nfp_add_zero]
    exact nfp_monotone (isNormal_add_right a).monotone zero_le
  · rw [← mul_one_add, one_add_omega0]

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a * x) 0 = 0

Tactic:
rw [← nonpos_iff_eq_zero, nfp_le_iff]

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x ↦ a * x)^[n] 0 ≤ 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0 ^ ω
⊢ nfp (fun x ↦ 0 * x) b = 0 ^ ω

pp: case inr
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) b = a ^ ω

Tactic:
· rw [zero_opow omega0_ne_zero] at hba
    cases hba.not_gt hb

Goal state after:
case inr
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) b = a ^ ω
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
max_comm

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

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

Tactic:
rw [deriv_succ, h]
    exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))

Goal state after:
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
⊢ max b a ≤ max (max a b) ℵ₀

Tactic:
max_comm

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord

Tactic:
by
  simpa using c.ord.card_le_beth

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

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

Tactic:
max_comm

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i

Tactic:
simp_rw [add_comm]

Goal state after:
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
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯

Tactic:
by
  have H := hf.cof_eq
  subst H
  exact hf

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

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max (a ^ b).card a.card ≤ max a.card (b.card + 1)

pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

pp: case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card

Tactic:
max_comm

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (a ^ b).card ≤ max a.card (b.card + 1)

case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ

Tactic:
by grw [h.1]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = o.cof

Tactic:
by
  rw [cof_eq_sInf_lsub]
  exact csInf_mem (cof_lsub_def_nonempty o)

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

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ max a.card ℵ₀ = max ℵ₀ a.card

Tactic:
max_comm

Goal state after:
a : Ordinal.{u_1}
h : 1 < a
⊢ max ℵ₀ a.card = max ℵ₀ a.card
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ (↑(f i) + 1).card ≤ c

Tactic:
card_le_iff

Goal state after:
case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ ↑(f i) + 1 < (succ c).ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ ℵ₀ ≤ κ

Tactic:
by simpa using h₁

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ c ^ ↑n ≤ max c ℵ₀

Tactic:
by
  rcases le_or_gt ℵ₀ c with hc | hc
  · exact le_max_of_le_left (power_nat_le hc)
  · exact le_max_of_le_right (power_lt_aleph0 hc natCast_lt_aleph0).le

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ max ℵ₀ #α = max #α ℵ₀

Tactic:
max_comm

Goal state after:
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ = max #α ℵ₀
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 : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t = t'

Tactic:
refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe]

Goal state after:
case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s

case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
x : β i
⊢ erase i (single i x) = 0

Tactic:
rw [erase_single, if_pos rfl]

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

Goal state before:
pp: case none
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) none = f none

pp: case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) (some i) = f (some i)

Tactic:
· rw [extendWith_none]

Goal state after:
case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f)) (some i) = f (some i)