mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
⊢ j < i → toZ i0 j < toZ i0 i

Tactic:
h_le

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : j < i
⊢ toZ i0 j < toZ i0 i
Module: Mathlib.Algebra.BigOperators.Intervals

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

Tactic:
mul_two

Goal state after:
n : ℕ
⊢ ∑ i ∈ range n, i + ∑ i ∈ range n, i = ∑ i ∈ range n, i + ∑ j ∈ range n, j
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
apply prod_congr_of_eq_on_inter <;> grind

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * x ^ i * y ^ (n.succ - i.succ) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

Tactic:
succ_sub_succ,

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x * x ^ i * y ^ (n - i) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
⊢ f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K

Tactic:
induction n with
  | zero =>
    contrapose! heq
    induction m with
    | zero => exact heq
    | succ m ih =>
      rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
      exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
  | succ n ih =>
    rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
      Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ p, p ≠ ⊥ ∧ p.IsMaximal

Tactic:
contrapose! h
  simp only [← bot_lt_iff_ne_bot] at h
  refine isField_iff_maximal_bot.mpr ⟨⟨bot_ne_top, Ideal.maximal_of_no_maximal h⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = a ∩ b ∪ y

Tactic:
union_eq_self_of_subset_left xy

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = y
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range

Tactic:
· intro hx
    choose y hy using hx
    refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
    constructor
    <;> contrapose
    <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : γ → β
n : β → α
s : Set γ
⊢ sᶜ ∈ comap m (comap n f) ↔ sᶜ ∈ comap (n ∘ m) f

Tactic:
by simp only [compl_mem_comap, image_image, (· ∘ ·)]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Tactic:
by
  rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Tactic:
by
  rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

Tactic:
rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy

Goal state after:
case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)

case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • m₁ = r • m₂
⊢ m₁ = m₂

Tactic:
rw [← sub_eq_zero, ← smul_sub] at hm

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : ∅.Finite
⊢ ∃ a, ∀ b ∈ ∅, f a ≤ f b

Tactic:
exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩

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

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

pp: 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₂

Tactic:
· simp [← hb] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β × γ⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
simp_rw [lt_iff]

Goal state after:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
⊢ ∀ ⦃a : α⦄,
    0 < a →
      ∀ ⦃b₁ b₂ : β × γ⦄,
        b₁.1 < b₂.1 ∧ b₁.2 ≤ b₂.2 ∨ b₁.1 ≤ b₂.1 ∧ b₁.2 < b₂.2 →
          (a • b₁).1 < (a • b₂).1 ∧ (a • b₁).2 ≤ (a • b₂).2 ∨ (a • b₁).1 ≤ (a • b₂).1 ∧ (a • b₁).2 < (a • b₂).2
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b

Tactic:
simp_rw [lt_iff]

Goal state after:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosStrictMono α γ
⊢ ∀ ⦃b : β × γ⦄,
    0.1 < b.1 ∧ 0.2 ≤ b.2 ∨ 0.1 ≤ b.1 ∧ 0.2 < b.2 →
      ∀ ⦃a₁ a₂ : α⦄,
        a₁ < a₂ → (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s)
hcof : IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t

Tactic:
have hcof' : IsCofinalFor d (d ∩ s) := hcof.union_right.mono_left hdst.ge

Goal state after:
α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s)
hcof : IsCofinalFor (d ∩ t) (d ∩ s)
hcof' : IsCofinalFor d (d ∩ s)
⊢ a ∈ s ∪ t
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂

Tactic:
simp_rw [lt_iff]

Goal state after:
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
⊢ ∀ ⦃b : β × γ⦄,
    0 ≤ b →
      ∀ ⦃a₁ a₂ : α⦄,
        (a₁ • b).1 < (a₂ • b).1 ∧ (a₁ • b).2 ≤ (a₂ • b).2 ∨ (a₁ • b).1 ≤ (a₂ • b).1 ∧ (a₁ • b).2 < (a₂ • b).2 → a₁ < a₂
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
isEmpty_prod,

Goal state after:
case type
α : Type u_4
r✝ : α → α → Prop
inst✝¹ : IsWellOrder α r✝
β : Type u_4
s✝ : β → β → Prop
inst✝ : IsWellOrder β s✝
⊢ IsEmpty β ∨ IsEmpty α ↔ IsEmpty α ∨ IsEmpty β
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove (range fun i ↦ f i + 1) ↔ BddAbove (range f)

Tactic:
by
  rw [range_comp' (· + 1), bddAbove_add_one_image_iff]

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
b : Ordinal.{u}
hb : b ∈ s
⊢ ∃ a, enumOrd s a = b

Tactic:
by
  rwa [← range_enumOrd hs] at hb

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : succ (iSup f) < lsub f
⊢ False

Tactic:
rw [heq] at this

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
this : lsub f < lsub f
⊢ False
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: n : ℕ
⊢ (↑n).ord = ↑n

Tactic:
by
  apply (ord_le.2 (card_nat n).ge).antisymm
  induction n with
  | zero => exact zero_le
  | succ n IH => exact (IH.trans_lt <| by simp).succ_le

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

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

Tactic:
by
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_opow', Ordinal.sub_zero]
  · rw [opow_of_ne_zero h, limitRecOn_zero]

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

Goal state before:
pp: a b c : Ordinal.{u_1}
ab : a ≤ b
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c

case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ c ≤ b ^ c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : b ≤ 1
n : ℕ
⊢ clog b n = 0

Tactic:
by
  grind [clog]

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

Goal state before:
pp: n : ℕ
hn : n ≤ 1
b : ℕ
⊢ clog b n = 0

Tactic:
by
  grind [clog]

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
obtain ho | ho := lt_or_ge o ω

Goal state after:
case inl
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
⊢ a < ω

Tactic:
obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha

Goal state after:
n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
b : Ordinal.{u_4}
hb' : b < ω
hb : a ≤ ↑n + b
⊢ a < ω
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a

Tactic:
rcases h with ⟨a0, b, rfl⟩
    exact isSuccPrelimit_mul_left isSuccLimit_omega0

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < clog b n

Tactic:
rw [clog, if_pos]
  exacts [Nat.succ_pos _, ⟨hb, hn⟩]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n < n.succ

Tactic:
exact (lt_clog_iff_pow_lt hb).mp H

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

Goal state before:
pp: case inl
b y : Ordinal.{u_1}
xy : 0 ≤ y
⊢ log b 0 ≤ log b y

pp: case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y

Tactic:
· simp_rw [log_zero_right, zero_le]

Goal state after:
case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m n : ℕ
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
obtain hm | hm := le_or_gt m 1

Goal state after:
case inl
m n : ℕ
hm : m ≤ 1
⊢ ↑(Nat.log m n) = log ↑m ↑n

case inr
m n : ℕ
hm : 1 < m
⊢ ↑(Nat.log m n) = log ↑m ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
hwo : ¬o < ω
⊢ (succ o).card.ord < succ o

Tactic:
simp_all [ord_card_le]

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

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

Tactic:
rw [add_comm, max_comm, add_eq_max ha]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n ≤ lift.{v, u} c ↔ ℵ_ ↑n ≤ c

Tactic:
simpa using lift_le (a := ℵ_ n)

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']

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

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

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

Tactic:
have repr_eq_zero (l) : b.repr (linearCombination R v l) i = 0 := by
    simp [linearCombination_apply, Finsupp.sum, w]

Goal state after:
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
⊢ False
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preOmega c.ord = c.ord

Tactic:
rw [← ord_preAleph, hc.preAleph_ord]

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

Goal state before:
pp: ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (mapRange f hf g).prod h = g.prod fun i b ↦ h i (f i b)

Tactic:
rw [mapRange_def]

Goal state after:
ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (mk g.support fun i ↦ f (↑i) (g ↑i)).prod h = g.prod fun i b ↦ h i (f i b)
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 : Function.Injective (mapRange f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ mapRange f hf (single i x) = mapRange f hf (single i y)

Tactic:
simpa using congr_arg _ eq

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
⊢ ((mapRange.addMonoidHom f) (mk x.support fun x_1 ↦ g ↑x_1)) i = x i

Tactic:
simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]

Goal state after:
case h
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range ≤ ⨆ i, ⨆ (_ : p i), S i

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

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
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (map (Finsupp.linearCombination R v) (Finsupp.supported R R s)) (span R (v '' t))

Tactic:
Finsupp.span_image_eq_map_linearCombination

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (map (Finsupp.linearCombination R v) (Finsupp.supported R R s))
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R t))
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
by
  classical
  rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ f • v ∈ ↑W

Tactic:
by
    rw [← f.sum_coeff_single, Finsupp.sum, Finset.sum_smul]
    simp_rw [← smul_of, smul_assoc]
    exact Submodule.sum_smul_mem W _ fun g _ => h g v hv

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
⊢ m ∈ AddSubmonoid.closure s

Tactic:
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' s) by
    simpa [← AddSubmonoid.toSubmonoid_closure]
  let s' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass s
  have h' : Submonoid.map (of R M) s' = Submonoid.closure (of R M '' s) :=
    MonoidHom.map_mclosure _ _
  rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
  simpa using! of'_mem_span.1 h

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ (∀ x ∈ s, ∀ y ∈ t, f x y ∈ u) ↔ ∀ a ∈ s, image (fun b ↦ f a b) t ⊆ u

Tactic:
image_subset_iff

Goal state after: