mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (e - e * e) = 0

Tactic:
he,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (e - e) = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
x y : R
⊢ (mk (span {x})) y = 0 ↔ x ∣ y

Tactic:
by
  rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : c₁ - c₂ ∈ I
hm : m₁ - m₂ ∈ pi fun x ↦ I
i : ι
⊢ (c₁ • m₁ - c₂ • m₂) i ∈ (fun x ↦ I) i

Tactic:
exact I.mul_sub_mul_mem hc (hm i)

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

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : a✝ ∈ (fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))

Tactic:
Set.mem_image

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : ∃ x ∈ ↑f.support, (f x * ↑x) ^ (n + 1) = a✝
⊢ a✝ ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝¹ b✝ : R
inst✝ : I.IsTwoSided
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
b : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a •
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c) =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) b +
      Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
exact congr_arg _ (smul_add _ _ _)

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
mem_iff_inf_principal_compl,

Goal state after:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 sᶜᶜ = ⊥
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
disjoint_principal_right

Goal state after:
α : Type u_1
f : Filter α
s : Set α
⊢ sᶜ ∈ f ↔ sᶜ ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝ : ∀ (j : ι), Nonempty (α j)
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ f.NeBot

Tactic:
by simp [comap_eval_neBot_iff', *]

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

Goal state before:
pp: α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ atTop = pure ⊤

Tactic:
isTop_top.atTop_eq,

Goal state after:
α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 𝓟 (Ici ⊤) = pure ⊤
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:
Finset.coe_singleton

Goal state after:
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₀
⊢ R ∙ x = R ∙ x
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
use .of_not_isCofinal
  rw [not_isCofinal_iff]
  rintro ⟨x, h⟩
  obtain ⟨z, hz⟩ := exists_gt x
  exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ c ≤ ⨅ i, lift.{v, u} #↑↑i ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
le_ciInf_iff'

Goal state after:
α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ (∀ (i : { s // IsCofinal s }), c ≤ lift.{v, u} #↑↑i) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑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
hM' : M'.FG
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
⊢ ∃ n, M' = N n

Tactic:
obtain ⟨S, hS⟩ := hM'

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'
⊢ ∃ n, M' = N n
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : 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 : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 < (_a₂ • b).1
h₂ : (_a₁ • b).2 ≤ (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
exact lt_of_smul_lt_smul_right h₁ hb.1

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
⊢ typeLT α ≤ (cof α).ord

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ typeLT α ≤ (cof α).ord

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ typeLT α ≤ (cof α).ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c d : Ordinal.{u_4}
⊢ a - b - c ≤ d ↔ a - (b + c) ≤ d

Tactic:
sub_le,

Goal state after:
a b c d : Ordinal.{u_4}
⊢ a - b ≤ c + d ↔ a - (b + c) ≤ d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c d : Ordinal.{u_4}
⊢ a - b ≤ c + d ↔ a - (b + c) ≤ d

Tactic:
sub_le,

Goal state after:
a b c d : Ordinal.{u_4}
⊢ a ≤ b + (c + d) ↔ a - (b + c) ≤ d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c d : Ordinal.{u_4}
⊢ a ≤ b + (c + d) ↔ a - (b + c) ≤ d

Tactic:
sub_le,

Goal state after:
a b c d : Ordinal.{u_4}
⊢ a ≤ b + (c + d) ↔ a ≤ b + c + d
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ StrictMono fun x ↦ ↑((StrictMono.orderIso f hf) x)

Tactic:
exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ o.brange f = range (o.familyOfBFamily f)

Tactic:
range_familyOfBFamily

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ o.brange f = o.brange f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub f ↔ ∃ i, a ≤ f i

Tactic:
by
  simpa only [not_forall, not_lt, not_le] using not_congr lsub_le_iff

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

Goal state before:
pp: case succ.inl
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n < b
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
simp [go, hnb, one_le_iff_ne_zero, hn]

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

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

Tactic:
simp at hlt

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
refine eq_of_forall_ge_iff fun d ↦ ?_

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d

Tactic:
sub_le,

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b ≤ a * c + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b - c ≤ d / a ↔ a * b ≤ a * c + d

Tactic:
sub_le,

Goal state after:
case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ b ≤ c + d / a ↔ a * b ≤ a * c + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ (x * y + w) % (x * z) = x * (y % z) + w

Tactic:
rw [mod_def, mul_add_div_mul hw]
  apply sub_eq_of_add_eq
  rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 < log b o

Tactic:
rwa [← add_one_le_iff, zero_add, ← opow_le_iff_le_log hb ho, opow_one]

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

Goal state before:
pp: case inr.inl.inr
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 1
hb : 1 ≤ 1
⊢ log 1 o = 0

Tactic:
· exact log_one_left o

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

Goal state before:
pp: 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
⊢ succ (op a b) ≤ ((fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o

Tactic:
exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod ha (hb.trans_le h)⟩

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

Goal state before:
pp: a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) a

Tactic:
by_contra ha
    rcases exists_lt_add_of_not_isPrincipal_add ha with ⟨b, hb, c, hc, rfl⟩
    exact (H b hb c hc).irrefl

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

Goal state before:
pp: case mp
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ → x ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
rintro ⟨a, rfl⟩
    exact ⟨omega0_le_omega a, isInitial_omega a⟩

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
a : ↑(Iio o)
ha : x < preBeth ↑a
⊢ 2 ^ x ≤ preBeth (↑a + 1)

Tactic:
simpa using power_le_power_left two_ne_zero ha.le

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

Goal state before:
pp: case inr.a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

pp: case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
· obtain ⟨x, xb, ax⟩ :=
        (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h
      grw [ax, ← opow_add, add_omega0_opow xb]

Goal state after:
case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inr
n m : ℕ
h : ↑n + ↑m = ↑n
⊢ ↑m = 0

Tactic:
norm_cast at h ⊢

Goal state after:
case refine_1.inr
n m : ℕ
h : n + m = n
⊢ m = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inr
n m : ℕ
h : n + m = n
⊢ m = 0

Tactic:
← add_right_inj,

Goal state after:
case refine_1.inr
n m : ℕ
h : n + m = n
⊢ ?refine_1.inr.a + m = ?refine_1.inr.a + 0

case refine_1.inr.a
n m : ℕ
h : n + m = n
⊢ ℕ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
n m k : ℕ
h : ↑n + ↑m = ↑n + ↑k
⊢ ↑m = ↑k

Tactic:
norm_cast at h ⊢

Goal state after:
case inr
n m k : ℕ
h : n + m = n + k
⊢ m = k
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = c + b
hb : b < ℵ₀
⊢ a = c

Tactic:
rw [add_comm a b, add_comm c b] at h

Goal state after:
a b c : Cardinal.{u_1}
h : b + a = b + c
hb : b < ℵ₀
⊢ a = c
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:
have H := hf.cof_eq

Goal state after:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
H : a.cof.ord = o
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
⊢ ∃ o f, a.IsFundamentalSequence o f

Tactic:
rcases ord_eq ι with ⟨r, wo, hr⟩

Goal state after:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
⊢ ∃ o f, a.IsFundamentalSequence o f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case pos
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : IsMin o
⊢ (preOmega o).cof = o.cof

Tactic:
simp [h.eq_bot]

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

Goal state before:
pp: c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ #↑(range fun i ↦ t i) * ⨆ s, #↑↑s < c

Tactic:
apply Cardinal.mul_lt_of_lt hc.aleph0_le (mk_range_le.trans_lt hι)

Goal state after:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #↑(t i) < c
⊢ ⨆ s, #↑↑s < c
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 : ℵ₀ ≤ #α
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩

Tactic:
intro a b hab
      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
⊢ Injective fun x ↦ ⟨{x}, ⋯⟩

Tactic:
intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < #α ^ Order.cof α

Tactic:
← card_ord (Order.cof _),

Goal state after:
case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #α < #α ^ (Order.cof α).ord.card
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
⊢ (sum fun n ↦ x ^ n) ≤ max ℵ₀ x

Tactic:
rw [← x.mk_out, ← mk_list_eq_sum_pow]
  exact mk_list_le_max _

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
⊢ f = g

Tactic:
by
  refine AddMonoidHom.eq_of_eqOn_denseM add_closure_iUnion_range_single fun f hf => ?_
  simp only [Set.mem_iUnion, Set.mem_range] at hf
  rcases hf with ⟨x, y, rfl⟩
  apply H

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
δ : Type u_1
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : AddCommMonoid γ
inst✝ : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → β i →+ γ
a : ι
⊢ (g.comp (liftAddHom f)).comp (singleAddHom β a) = g.comp (f a)

Tactic:
AddMonoidHom.comp_assoc,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
δ : Type u_1
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : AddCommMonoid γ
inst✝ : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → β i →+ γ
a : ι
⊢ g.comp ((liftAddHom f).comp (singleAddHom β a)) = g.comp (f a)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ x✝ ∈ f.dualMap.ker ↔ x✝ ∈ f.range.dualAnnihilator

Tactic:
mem_ker,

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ f.dualMap x✝ = 0 ↔ x✝ ∈ f.range.dualAnnihilator
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
replace h := @h (.single 0 s + .single 1 t) 0 ?_
  · exact ⟨by simpa using congr($h 0), by simpa using congr($h 1)⟩
  simpa

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
by
  rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

Goal state after:
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
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]

Tactic:
by
  rw [← pair_symm_iff, add_comm, pair_add_right_iff, pair_symm_iff]

Goal state after:
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
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 1 = a⁻¹ * (a * 1)

Tactic:
simp [a0]

Goal state after:
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
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
a0 : a ≠ 0
⊢ 0 = a⁻¹ * 1 + -a⁻¹ * 1

Tactic:
simp [a0]

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
inst✝² : Monoid S
inst✝¹ : Semiring R
inst✝ : DistribMulAction S R
f : M → N
s : S
x : R[M]
a✝ : N
⊢ (mapDomain f (s • x)).coeff a✝ = (s • mapDomain f x).coeff a✝

Tactic:
simp [Finsupp.mapDomain_smul]

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
by
  rw [image₂_swap f]
  exact image_image₂_distrib fun _ _ => h_antidistrib _ _

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑u ⊆ Prod.fst ⁻¹' s ∧ ↑u ⊆ Prod.snd ⁻¹' t ∧ ∀ x ∈ u, f x.1 x.2 ∈ image₂ (fun a b ↦ f a.1 b.2) u u

Tactic:
exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = t.sup fun y ↦ s.sup fun x ↦ g (f x y)

Tactic:
simp only [image₂, sup_image, sup_product_right]; rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c

Tactic:
by classical simp [mul_def, add_mul, sum_add, sum_add_index]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
a✝ : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0

Tactic:
rcases Prod.mk_inj.mp (J (a0, b0) ⟨Finset.mk_mem_product aA bB, rfl⟩) with ⟨rfl, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
a✝ : (a0, b0) ∈ A ×ˢ B ∧ (a0, b0).1 * (a0, b0).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (a0, b0)
⊢ x = a0 ∧ y = b0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : f (a * b) = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG

Tactic:
he,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
inst✝ : DecidableEq H
f : G →ₙ* H
A B : Finset G
aG bG : G
aH bH : H
hae : f aG = aH
hbe : f bG = bH
huG : UniqueMul ({a ∈ A | f a = aH}) ({b ∈ B | f b = bH}) aG bG
a b : G
huH : f (aG * bG) = aH * bH → f a = aH ∧ f b = bH
ha : a ∈ A
hb : b ∈ B
he : a * b = aG * bG
⊢ a = aG ∧ b = bG
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b2
⊢ b1 = b2

Tactic:
classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2

Goal state after: