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

Goal state before:
pp: case neg
α : Type u
f : Filter α
t : f.NeBot
p : Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
simp [h, t.ne]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ span R ↑{x} = R ∙ x

Tactic:
by rw [Finset.coe_singleton]

Goal state after:
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
P Q : { P // P.FG }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]; exact le_sup_right

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
obtain hb | hb := hb.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
⊢ a₁ < a₂

Tactic:
obtain hb | hb := hb.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 = b
⊢ a₁ < a₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ • b < a₂ • b
hb : 0 < b
⊢ a₁ < a₂
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R ↑t = S
⊢ span A ↑t = span A ↑(span R ↑t)

Tactic:
Submodule.span_span_of_tower

Goal state after:
case h
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R ↑t = S
⊢ span A ↑t = span A ↑t
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Module.Finite B C
algebraizeInst✝ : Module.Finite A B
⊢ (g.comp f).Finite

Tactic:
exact .trans B C

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

Goal state before:
pp: o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.25 < Ordinal.liftPrincipalSeg.top

Tactic:
simpa using h

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
ord_univ

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mpr
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ (∃ d < c, a ≤ b + d) → a < b + c

Tactic:
rintro ⟨d, hd, ha⟩

Goal state after:
case mpr
a b c : Ordinal.{u_4}
hc : c ≠ 0
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d

Tactic:
rintro ⟨d, hd, ha⟩

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ ∃ d < c, a < b + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d

Tactic:
rintro ⟨d, hd, ha⟩

Goal state after:
case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a < b + d
⊢ ∃ d < c, a ≤ b + d
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < lift.{v, u} (succ #ι).ord

Tactic:
by
  rw [lift_ord, Cardinal.lift_succ, ← card_le_iff]
  exact card_sInf_range_compl_le_lift f

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s

Tactic:
by
  let H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono
  refine ⟨fun he ↦ by simpa using he.dirSupClosed_range, ?_⟩
  rw [isNormal_iff, dirSupClosed_iff_of_linearOrder]
  refine fun hs' ↦ ⟨H, fun a ha b hb ↦ ?_⟩
  have bdd : BddAbove (Subtype.val ∘ enum s hs '' Iio a) := by
    use enum s hs a
    simpa [upperBounds] using fun x hx ↦ hx.le
  have : Nonempty α := ⟨a⟩
  let := WellFoundedLT.toOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  trans sSup ((Subtype.val ∘ enum s hs) '' Iio a)
  · refine enum_le_of_forall_lt (hs' ?_ ?_ (isLUB_csSup' bdd)) fun b hb ↦ ?_
    · grind
    · simpa using ha.ne_bot
    · obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb
      refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩
      simpa
  · apply csSup_le'
    simpa [upperBounds]

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

Goal state before:
pp: case mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
b : Ordinal.{u}
hb : b < sInf t
hb' : a ≤ enumOrd s b
⊢ False

Tactic:
exact hb.not_ge (csInf_le' hb')

Goal state after:
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
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha ↦ succ (f a ha)) b hb = a
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
obtain ⟨c, hc, hc'⟩ := h ⟨b, hb, rfl⟩

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
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha ↦ succ (f a ha)) b hb = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
rcases eq_or_ne b 0 with (rfl | h')

Goal state after:
case inl
a : Ordinal.{u_4}
h : IsSuccLimit (a + 0)
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a

case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
a1,

Goal state after:
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ 1 ^ 1 ≤ 1 ^ b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b ^ 2) fuel).fst = b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) < n
ih₃ : n ≤ b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1)
⊢ (if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
          (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
        else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).fst =
      b ^
          ((if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
              else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd +
            1) /
        n ∧
    b ^
          (if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
              (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
            else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd <
        n ∧
      n ≤
        b ^
          ((if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
              else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd +
            1)

Tactic:
split <;> simp_all [Nat.mul_add_one, Nat.pow_add_one']

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

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a

Tactic:
grw [mul_div_le]

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ x + ↑n ≤ a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [ha, zero_opow omega0_ne_zero]
    exact .inr zero_le

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

Goal state before:
pp: case inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
use m + 1

Goal state after:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m + 1] o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑(m + m) ≤ ω ^ o

Tactic:
exact (opow_mul_lt_opow (natCast_lt_omega0 _) hc).le

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
⊢ a * o = o

Tactic:
rcases le_or_gt o 2 with ho | ho
    · convert! one_mul o
      apply le_antisymm
      · rw [← lt_add_one_iff, one_add_one_eq_two]
        exact hao.trans_le ho
      · rwa [one_le_iff_pos]
    · exact op_eq_self_of_isPrincipal hao (isNormal_mul_right ha₀) h
        (isSuccLimit_of_isPrincipal_mul ho h)

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

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

Tactic:
by
  rw [← (isInitial_omega o).card_lt_card, card_omega]

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

Goal state before:
pp: case a
n : ℕ
ha : ↑n ∈ Iio ω
⊢ preBeth ↑⟨↑n, ha⟩ ≤ ℵ₀

Tactic:
preBeth_nat

Goal state after:
case a
n : ℕ
ha : ↑n ∈ Iio ω
⊢ ↑((fun x ↦ 2 ^ x)^[n] 0) ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ preBeth ω ≤ ℵ₀

Tactic:
rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]
    rintro ⟨a, ha⟩
    obtain ⟨n, rfl⟩ := lt_omega0.1 ha
    rw [preBeth_nat]
    exact natCast_le_aleph0

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

Goal state before:
pp: case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{max (u + 1) v, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{max u (u + 1) v, v} (Order.cof β)

Tactic:
Cardinal.lift_umax.{_, u + 1},

Goal state after:
case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{max u (u + 1) v, v} (Order.cof β)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{max u (u + 1) v, v} (Order.cof β)

Tactic:
Cardinal.lift_umax.{_, u + 1},

Goal state after:
case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) = Cardinal.lift.{u + 1, v} (Order.cof β)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg.inr.inr
n : ℕ
h2a : ↑n ≠ 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
rw [← Cardinal.one_le_iff_ne_zero] at h2a hb

Goal state after:
case neg.inr.inr
n : ℕ
h2a : 1 ≤ ↑n
m : ℕ
hb : 1 ≤ ↑m
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rw [add_comm, add_eq_left_iff]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 = lift.{v, u} o ↔ ω_ 1 = o

Tactic:
simpa using lift_inj (a := ω₁)

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).ToType ≤ sum fun i ↦ #(f i).ToType

Tactic:
← mk_sigma,

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).ToType ≤ #((i : ι) × (f i).ToType)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c

Tactic:
rw [← mul_eq_self hc, Cardinal.lift_mul]

Goal state after:
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ Cardinal.lift.{v, u} #ι * ⨆ i, Cardinal.lift.{u, v} (f i).card ≤ Cardinal.lift.{u, v} c * Cardinal.lift.{u, v} c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ (o'.blsub fun i hi ↦ f (g i hi) ⋯) = a

Tactic:
· rw [@blsub_comp.{u, u, u} o _ f (@IsFundamentalSequence.monotone _ _ f hf)]
    · exact hf.2.2
    · exact hg.2.2

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
let f : S → Ordinal := fun s => typein LT.lt s.val

Goal state after:
case refine_2
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
Module: Mathlib.SetTheory.Cardinal.Ordinal

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

Tactic:
opow_natCast,

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

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

Tactic:
by
  by_contra! hf
  apply (lift_iSup_lt_of_lt_cof _ H).false
  rwa [Cardinal.lift_umax, lift_id']

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty (Quotient.out x)
⊢ (sum fun n ↦ x ^ n) = max ℵ₀ x

Tactic:
conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]

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

Goal state before:
pp: case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
    refine fun h ↦ h.aleph0_le.not_gt ?_
    rw [succ_natCast, ← Nat.cast_add_one]
    exact natCast_lt_aleph0

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

Goal state before:
pp: ⊢ ℵ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by
  simpa using IsInaccessible.univ.aleph_ord

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨Finset.univ.val, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
simp_rw [← hl, Equiv.subtypeQuotientEquivQuotientSubtype, listChoice_mk]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a ↦
              Quotient.hrecOn (motive := fun x ↦
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧) ⋯ =
    ⟦a⟧
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
⊢ Function.Injective (mapRange f hf) ↔ ∀ (i : ι), Function.Injective (f i)

Tactic:
by
  classical exact ⟨fun h i x y eq ↦ single_injective (@h (single i x) (single i y) <| by
    simpa using congr_arg _ eq), fun h _ _ eq ↦ DFinsupp.ext fun i ↦ h i congr($eq i)⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ (i : ↑s), LinearIndepOn R v ↑i

Tactic:
simpa using h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ ∀ (i : ↑s), LinearIndepOn R v (t ↑i)

Tactic:
simpa using h

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i ↦ ⟨↑(μ i), ⋯⟩) i) = a

Tactic:
← hμ

Goal state after:
case h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i ↦ ⟨↑(μ i), ⋯⟩) i) = μ.sum fun x xi ↦ ↑xi
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = a

pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
← hμ

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ i)

case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
this : ¬LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
simpa [h]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x✝ : X
⊢ (toFreeAbelianGroup.comp toFinsupp) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Tactic:
toFreeAbelianGroup,

Goal state after:
X : Type u_1
x✝ : X
⊢ ((liftAddHom fun x ↦ (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)).comp toFinsupp) (of x✝) =
    (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)