mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: 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
hS : S.FG
⊢ (span A ↑S).FG

Tactic:
by
  obtain ⟨t, ht⟩ := hS
  use t
  rw [← ht, Submodule.span_span_of_tower]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
⊢ IsLUB d b → b ∈ {a}

Tactic:
hb

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ b ∈ {a}
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 ⊢
      obtain ⟨f⟩ := lift_type_lt.{_,_,v}.1 h
      obtain ⟨f, a, hf⟩ := f
      exists a
      induction a using inductionOn with | type α r
      refine lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
        ⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
      · exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩
      · refine fun a b h => (typein_lt_typein r).1 ?_
        rw [typein_enum, typein_enum]
        exact f.map_rel_iff.2 h
      · intro a'
        obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
        exists b
        simp only [RelEmbedding.ofMonotone_coe]
        simp [e]

Goal state after:
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)
x✝¹ x✝ : α
h : r x✝¹ x✝
⊢ Sum.Lex t r (Sum.inr x✝¹) (Sum.inr x✝)

Tactic:
Sum.lex_inr_inr

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✝
⊢ r x✝¹ x✝
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

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

Tactic:
· cases nonempty_unique α
      have := BoundedOrder.ofUnique α
      simp

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

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

Tactic:
hb

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

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

Tactic:
obtain h | h := le_or_gt b a
  · exact (Ordinal.add_sub_cancel_of_le h).ge
  · simpa [sub_eq_zero_of_lt h] using h.le

Goal state after:
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}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
⊢ ⟦{ α := γ, r := t, wo := wo✝ }⟧ * ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤
    ⟦{ α := γ, r := t, wo := wo✝ }⟧ * ⟦{ α := β, r := s, wo := wo✝¹ }⟧

Tactic:
refine
        (RelEmbedding.ofMonotone (fun a : α × γ => (f a.1, a.2)) fun a b h => ?_).ordinal_type_le
      obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h
      · exact Prod.Lex.left _ _ (f.toRelEmbedding.map_rel_iff.2 h')
      · exact Prod.Lex.right _ h'

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}
⊢ b < sInf t → enumOrd s b < a

Tactic:
hb

Goal state after:
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
⊢ enumOrd s b < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_2
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a✝ < c
a b : { x // Prod.Lex s r x (b✝, a✝) }
⊢ Subrel (Prod.Lex s r) (fun x ↦ Prod.Lex s r x (b✝, a✝)) a b →
    Sum.Lex (Prod.Lex (Subrel s fun x ↦ s x b✝) r) (Subrel r fun x ↦ r x a✝)
      (Subtype.casesOn a fun val h ↦
        Prod.casesOn (motive := fun x ↦ Prod.Lex s r x (b✝, a✝) → { x // s x b✝ } × α ⊕ { x // r x a✝ }) val
          (fun b' a' h ↦ if e : b✝ = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)
      (Subtype.casesOn b fun val h ↦
        Prod.casesOn (motive := fun x ↦ Prod.Lex s r x (b✝, a✝) → { x // s x b✝ } × α ⊕ { x // r x a✝ }) val
          (fun b' a' h ↦ if e : b✝ = b' then Sum.inr ⟨a', ⋯⟩ else Sum.inl (⟨b', ⋯⟩, a')) h)

Tactic:
grind [subrel_val, Sum.Lex.sep, asymm_of s]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (a / b)

Tactic:
rw [lt_mul_iff_div_lt h, lt_succ_iff]

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

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

Tactic:
by
  simpa only [mul_succ] using lt_mul_succ_div a h

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

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
have := H o ho

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.blsub fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
have := H o ho

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.blsub fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
obtain rfl | hc := eq_zero_or_pos c

Goal state after:
case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
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
b : Ordinal.{u_4}
⊢ b < ω → ω * (x / ω) + b ≤ a

Tactic:
hb

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
b : Ordinal.{u_4}
hb : b < ω
⊢ ω * (x / ω) + b ≤ a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ clog b n ≤ c + 1 ↔ clog b ((n + b - 1) / b) + 1 ≤ c + 1

Tactic:
simp only [clog_le_iff_le_pow, Nat.pow_add_one, Nat.add_le_add_iff_right, Nat.zero_lt_of_lt hb,
      div_le_iff_le_mul, hb]

Goal state after:
case succ
b n : ℕ
hb : 1 < b
hn : 1 < n
c : ℕ
⊢ n ≤ b ^ c * b ↔ n + b - 1 ≤ b ^ c * b + b - 1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
⊢ b < o → op a b < o

Tactic:
hb

Goal state after:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
⊢ y < b → ∃ b ∈ s, op x y < b

Tactic:
hb

Goal state after:
case pos.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
⊢ ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o → op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o

Tactic:
hb

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
hb : b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ op a b < nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
· rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]
    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 (le_self_add.trans (le_succ _)))

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a < 2
⊢ b < 2 → (fun x1 x2 ↦ x1 * x2) a b < 2

Tactic:
hb

Goal state after:
a b : Ordinal.{u_1}
ha : a < 2
hb : b < 2
⊢ (fun x1 x2 ↦ x1 * x2) a b < 2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Tactic:
· rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
    · rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
    all_goals simp

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

Goal state before:
pp: a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ b ≤ a

Tactic:
← hg.ord_cof

Goal state after:
a b o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : ↑(Iio b) → ↑(Iio a)
hf : IsFundamentalSeq f
hg : IsFundamentalSeq g
⊢ a.cof.ord ≤ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof

Tactic:
simpa [← lift_cof] using ha

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

Goal state before:
pp: a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.IsFundamentalSequence a.cof.ord fun i hi ↦ f i ⋯

Tactic:
exact hf

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

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

Tactic:
grw [h.1]

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

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

Tactic:
exact ⟨by grw [h.1], mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩

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

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

Tactic:
rw [opow_natCast, ← natCast_pow, card_nat]

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

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ 0)

Tactic:
rw [omega_zero]

Goal state after:
case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) ω
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
⊢ b < ω_ o → (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o

Tactic:
hb

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a < ω_ o
hb : b < ω_ o
⊢ (fun x1 x2 ↦ x1 ^ x2) a b < ω_ o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
⊢ b < c.ord → (fun x1 x2 ↦ x1 + x2) a b < c.ord

Tactic:
hb

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 ↦ x1 + x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
exact cof_map_of_isNormal (isNormal_add_right a) hb

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
⊢ b < c.ord → (fun x1 x2 ↦ x1 * x2) a b < c.ord

Tactic:
hb

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 ↦ x1 * x2) a b < c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s // Bounded r s }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · apply bounded_singleton
      rw [← hr]
      apply isSuccLimit_ord ha
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ (if p i then single i x else 0) = single i x

Tactic:
if_pos h

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ single i x = single i x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (filter (fun x ↦ i = x) f) i✝ = (single i (f i)) i✝

Tactic:
filter_apply,

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = (single i (f i)) i✝
Module: Mathlib.Data.List.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Type u_2
l : List ι
fs : (i : ι) → List (α i)
f : (i : ι) → i ∈ l → α i
⊢ f ∈ l.pi fs ↔ ∀ (i : ι) (hi : i ∈ l), f i hi ∈ fs i

Tactic:
simpa [Multiset.pi_coe] using! Multiset.mem_pi ↑l (fs ·) f

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

Goal state before:
pp: ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ f.update i b = f - single i (f i) + single i b

Tactic:
rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) (f - g) =
    (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
sumAddHom_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) f - (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
sumAddHom_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
this :
  ((f - g).sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) =
    (f.sum fun x ↦ ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) - (sumAddHom fun a ↦ AddMonoidHom.ofMapSub (h a) ⋯) g
⊢ (f - g).sum h = f.sum h - g.sum h
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.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
x : ι
hx : x ∉ s
⊢ ↑(μ x) = 0

Tactic:
← mem_bot R

Goal state after:
case h.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
x : ι
hx : x ∉ s
⊢ ↑(μ x) ∈ ⊥
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
this : ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
let thisI : AddCommGroup (Π₀ i, p i) := inferInstance

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
this : ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
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
hbd : b = 0 ∧ d = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
by_cases hac : a = 0 ∧ c = 0

Goal state after:
case pos
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
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

case neg
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
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), r • v i ∈ span R (v '' s) → r = 0
⊢ LinearIndepOn R v (s ∪ {i})

Tactic:
refine hs.union (.singleton' fun r hr ↦ hx _ <| by simp [hr]) ?_

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), r • v i ∈ span R (v '' s) → r = 0
⊢ Disjoint (span R (v '' s)) (span R (v '' {i}))
Module: Mathlib.Data.Finset.NAry

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

Tactic:
exact image_image2_antidistrib_left h_antidistrib

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (f.coeff.sum fun m₁ r₁ ↦ g.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = a0 * b0 then r₁ * r₂ else 0) = f.coeff a0 * g.coeff b0

Tactic:
sum,

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (∑ a ∈ f.coeff.support, ∑ x ∈ g.coeff.support, if a * x = a0 * b0 then f.coeff a * g.coeff x else 0) =
    f.coeff a0 * g.coeff 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
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
⊢ b ∈ B.preimage ⇑f ⋯ → a * b = a0 * b0 → a = a0 ∧ b = b0

Tactic:
hb

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
⊢ a * b = a0 * b0 → a = a0 ∧ b = b0