mathlib-initiative/mathlib-tactics huggingface dataset:
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 *

Goal state after:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
⊢ ∀ s ∈ l₂, (fun x ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

Tactic:
by
  simp only [inf_neBot_iff, frequently_iff, and_comm]; rfl

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

Goal state before:
pp: α : Type u
a : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Tactic:
simp [Filter.Frequently, not_forall]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
tendsto_iff_comap,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ atTop ≤ comap f (𝓟 s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s
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
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
⊢ ∃ n, M' = N n

Tactic:
have (s : S) : ∃ n, (s : M) ∈ N n :=
    (mem_iSup_of_chain N s).mp (by simpa [H, ← hS] using subset_span s.prop)

Goal state after:
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'
this : ∀ (s : ↥S), ∃ n, ↑s ∈ N n
⊢ ∃ n, M' = N n
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
x : A₁
⊢ (algebraMap A₁ B₁) x = (algebraMap A₂ B₁) ((algebraMap A₁ A₂) x)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite R ↥S₁
S₂ : Submodule R V
hS₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)

Tactic:
exact finite_sup S₁ S₂

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ Module.Finite R≥0 R

Tactic:
simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']
  refine ⟨{1, -1}, by simp, fun x ↦ ?_⟩
  obtain hx | hx := le_total 0 x
  · simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨x, hx⟩ (x := 1)
      (Submodule.subset_span <| by simp)
  · simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
      (Submodule.subset_span <| by simp)

Goal state after:
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
h : type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
rw [← lift_id (type s)] at h ⊢

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

Goal state before:
pp: α✝ : 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
g : α → β
hg : ∀ (a : α), f (Sum.inr a) = Sum.inr (g a)
⊢ type r ≤ type s

Tactic:
refine (RelEmbedding.ofMonotone g fun _ _ h ↦ ?_).ordinal_type_le

Goal state after:
α✝ : 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
g : α → β
hg : ∀ (a : α), f (Sum.inr a) = Sum.inr (g a)
x✝¹ x✝ : α
h : r x✝¹ x✝
⊢ s (g x✝¹) (g x✝)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ (o.brange fun x x_1 ↦ c) = {c}

Tactic:
rw [← range_familyOfBFamily]
  exact @Set.range_const _ o.ToType (nonempty_toType_iff.2 ho) c

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f (iSup (familyOfBFamily' r ?ho g)) = (type r).bsup fun a h ↦ f (g a h)

pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

Tactic:
Order.IsNormal.map_iSup H bddAbove_of_small,

Goal state after:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho g i) = (type r).bsup fun a h ↦ f (g a h)

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f

Tactic:
simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_ofPred]

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

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
⊢ ⨆ b, enumOrd s ↑b ≤ a

Tactic:
· exact Ordinal.iSup_le fun x ↦ ha _ x.2

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

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

Tactic:
by
    rw [h]
    apply lt_blsub

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * a + b * (c / b) + b

Tactic:
add_assoc,

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * a + (b * (c / b) + b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
h : ↑n < ω
⊢ succ ↑n < ω

Tactic:
exact natCast_lt_omega0 (n + 1)

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

Goal state before:
pp: case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [h, log_zero_right]

Goal state after:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
add_assoc,

Goal state after:
case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ (u + (log b v + 1))
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 + ω ^ log ω a * ↑n + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
add_assoc,

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a + (ω ^ log ω a * ↑n + a % ω ^ log ω a) - ω ^ log ω a < a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove (fixedPoints f)

Tactic:
convert! not_bddAbove_fp_family fun _ : Unit => H
  exact (Set.iInter_const _).symm

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

Goal state before:
pp: case mp
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n) → ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

pp: case mpr
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)) → ∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n

Tactic:
· intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩
    exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩

Goal state after:
case mpr
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)) → ∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ¬BddAbove {x | x.IsInitial}

Tactic:
rintro ⟨a, ha⟩
  have := ha (isInitial_ord (succ a.card))
  rw [ord_le] at this
  exact (lt_succ _).not_ge this

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preAleph (ω + o + 1) = ℵ_ (o + 1)

Tactic:
add_assoc,

Goal state after:
o : Ordinal.{u_1}
⊢ preAleph (ω + (o + 1)) = ℵ_ (o + 1)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
convert! mul_le_mul_left (Cardinal.one_le_iff_ne_zero.mpr h) a

Goal state after:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = 1 * a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case refine_1
o : Ordinal.{u_1}
⊢ ¬IsSuccPrelimit o → ¬(preBeth o).IsStrongPrelimit

Tactic:
rw [not_isSuccPrelimit_iff_mem_range_succ, not_isStrongPrelimit_iff]

Goal state after:
case refine_1
o : Ordinal.{u_1}
⊢ o ∈ range succ → ∃ x < preBeth o, preBeth o ≤ 2 ^ x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preBeth o).IsStrongPrelimit ↔ IsSuccPrelimit o

Tactic:
by
  refine ⟨?_, fun ho x hx ↦ ?_⟩
  · contrapose!
    rw [not_isSuccPrelimit_iff_mem_range_succ, not_isStrongPrelimit_iff]
    rintro ⟨a, rfl⟩
    refine ⟨preBeth a, ?_, ?_⟩
    · rw [preBeth_lt_preBeth, lt_succ_iff]
    · simp
  · rw [preBeth_limit ho] at hx
    obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx
    apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'
    simpa using power_le_power_left two_ne_zero ha.le

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

Goal state before:
pp: case pos
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : a = 0
⊢ b = 1 ∨ a = 0

Tactic:
exact Or.inr h2a

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

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)
      · exact (not_lt_zero ho₂).elim
      · rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
        · simp
        · exact Or.inr ⟨b, rfl⟩

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

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

Tactic:
rw [card_le_nat]

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

Goal state before:
pp: a : Ordinal.{u}
h : ∃ o f, a.IsFundamentalSequence o f
⊢ ∃ f, a.IsFundamentalSequence a.cof.ord f

Tactic:
rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩

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

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

Tactic:
rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h

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

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

Tactic:
by
  simpa using IsInaccessible.univ.preBeth_ord

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ x ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
by
    apply DFinsupp.induction x
    · exact AddSubmonoid.zero_mem _
    exact fun a b f _ _ hf =>
      AddSubmonoid.add_mem _
        (AddSubmonoid.subset_closure <| Set.mem_iUnion.2 ⟨a, Set.mem_range_self _⟩) hf

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

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

Tactic:
rw [← single_zero i, single_eq_single_iff]
  simp

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

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

Tactic:
by
  rw [← single_zero i, single_eq_single_iff]
  simp

Goal state after:
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:
by
  rw [erase_single, if_pos rfl]

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
⊢ (f + single i b) i = (single i b + f) i

Tactic:
simp [h1]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∉ s
⊢ 0 = -0

Tactic:
rw [neg_zero]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ f = 0 → ∀ i ∈ ↑s, f i = 0

Tactic:
rintro rfl _ _

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
s : { s // ∀ (i : ι), i ∈ s ∨ toFun 0 i = 0 }
i✝ : ι
a✝ : i✝ ∈ ↑s
⊢ 0 i✝ = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_1
ι : 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
i : ι
h1 : ¬g i = 0
h2 : f i (g i) = 0
⊢ h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = 1

Tactic:
simp [h2, h0]

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

Goal state before:
pp: case refine_2
ι : 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
i : ι
h1 : ¬g i = 0
⊢ h i ((mk g.support fun i ↦ f (↑i) (g ↑i)) i) = (fun i b ↦ h i (f i b)) i (g i)

Tactic:
simp [h1]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i x ↦ (e i) x) ⋯ (mapRange (fun i x ↦ (e i).symm x) ⋯ x) = x

Tactic:
rw [← mapRange_comp] <;>
        · simp_rw [AddEquiv.self_comp_symm]
          simp

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

Tactic:
specialize h {i, j} (Pi.single i c + Pi.single j d)
    simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h

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

Goal state before:
pp: X : Type u_1
x✝ : X
⊢ (liftAddHom fun x ↦ (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)) ((lift fun x ↦ single x 1) (of x✝)) =
    (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Tactic:
lift_apply_of,

Goal state after:
X : Type u_1
x✝ : X
⊢ (liftAddHom fun x ↦ (smulAddHom ℤ (FreeAbelianGroup X)).flip (of x)) (single x✝ 1) =
    (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
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 : ι
⊢ ∑ b ∈ image (fun g ↦ g i) (piFinset fun x ↦ s), #({a ∈ piFinset fun x ↦ s | a i = b}) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image₂ f {a} t) = #t

Tactic:
image₂_singleton_left,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image (fun b ↦ f a b) t) = #t
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
a : α
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂

Tactic:
image₂_singleton_left,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
a : α
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image (fun b ↦ f a b) (t₁ ∩ t₂) = image (fun b ↦ f a b) t₁ ∩ image (fun b ↦ f a b) t₂
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : u.card = (insert b₂ s' ∪ t).card
⊢ ↑t ⊆ ↑(insert b₁ t)

Tactic:
by simp [subset_insert]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
e : R ≃+* S
x : R[M]
m : M
⊢ ((mapRingEquiv M e) x).coeff m = e (x.coeff m)

Tactic:
by simp [mapRingEquiv]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
e : R ≃+* S
r : R
m : M
⊢ (mapRingEquiv M e) (single m r) = single m (e r)

Tactic:
by simp [mapRingEquiv]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m' = m₂ then r' * r else 0) = x.coeff m₂ * r

Tactic:
simp +contextual [Finsupp.sum_eq_single m₂]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m' = m₂ then r * r' else 0) = r * x.coeff m₂

Tactic:
simp +contextual [Finsupp.sum_eq_single m₂]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
m : M
r : R
n : ℕ
⊢ single m r ^ (n + 1) = single (m ^ (n + 1)) (r ^ (n + 1))

Tactic:
simp [pow_succ, single_pow _ _ n]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using smul 0 (.of R M 1) (of 1)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ 0 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
by rw [length_sort]; exact card_pos.2 h

Goal state after: