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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → f = ⊥

Tactic:
← empty_mem_iff_bot

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ ∅ ∈ map m f → ∅ ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
f : Filter β
⊢ map (⇑e) (map (⇑e.symm) f) = map (⇑e) (comap (⇑e) f)

Tactic:
rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Tactic:
· refine sets_of_superset (map g f) (image_mem_map ht) ?_
    rintro b ⟨a, ha, rfl⟩
    exact ⟨g, hs, a, ha, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Group.Action.TransferInstance

Goal state before:
pp: M : Type u_1
N : Type u_2
O : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid O
e : N ≃ O
inst✝ : MulDistribMulAction M O
this : Monoid N := e.monoid
⊢ ∀ (r : M) (x y : N), r • (x * y) = r • x * r • y

Tactic:
simp [mul_def, smul_def, smul_mul']

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ span R ↑hs.toFinset = span R s

Tactic:
hs.coe_toFinset

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
hs : s.Finite
⊢ span R s = span R s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case empty
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
⊢ motive (span R ↑∅) ⋯

Tactic:
simpa using singleton 0

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

Goal state before:
pp: case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Tactic:
← e

Goal state after:
case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ span R ↑s ≤ restrictScalars R (span A ↑s)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ a • b₂ < a • b₁

Tactic:
by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_lt_neg_iff]
  exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∩ t)

Tactic:
rw [← sInter_pair]

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (⋂₀ {s, t})
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ∃ S, S.Finite ∧ span A S = ⊤

Tactic:
refine ⟨S, hSfin, eq_top_iff.mpr ?_⟩

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : span R S = ⊤
⊢ ⊤ ≤ span A S
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
← e

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
a : Ordinal.{u}
e : liftInitialSeg.toRelEmbedding a = type s
⊢ liftInitialSeg.toRelEmbedding a < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r fun x1 x2 ↦ x1 < x2)

Tactic:
refine ⟨⟨Embedding.subtype _, ?_⟩⟩

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ ∀ {a b : ↑s}, (Embedding.subtype fun x ↦ x ∈ s) a < (Embedding.subtype fun x ↦ x ∈ s) b ↔ a < b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
ι : Type u_3
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : ι
⊢ bfamilyOfFamily' r f ((typein r).toRelEmbedding i) ⋯ = f i

Tactic:
simp only [bfamilyOfFamily', enum_typein]

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
x✝ : Ordinal.{?u.21}
⊢ x✝ * 0 = 0

Tactic:
exact mul_eq_zero'.2 (.inr rfl)

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

Goal state before:
pp: b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
by
  rcases em (1 < b ∧ n ≠ 0) with (⟨hb, hn⟩ | hbn)
  · rw [le_antisymm_iff, ← Nat.lt_succ_iff, le_log_iff_pow_le, log_lt_iff_lt_pow,
      and_comm] <;> assumption
  have hm : m ≠ 0 := h.resolve_right hbn
  rw [not_and_or, not_lt, Ne, not_not] at hbn
  rcases hbn with (hb | rfl)
  · obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb <;>
      simp only [log_zero_left, log_one_left] <;> lia
  · simp [@eq_comm _ 0, hm]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = f (iSup Nat.cast)

Tactic:
hf.map_iSup bddAbove_of_small

Goal state after:
f : Ordinal.{u} → Ordinal.{v}
hf : IsNormal f
⊢ ⨆ n, f ↑n = ⨆ i, f ↑i
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m * (n + 1)) = ↑m * ↑(n + 1)

Tactic:
by rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]

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

Goal state before:
pp: x : ℕ
⊢ (typein LT.lt).toRelEmbedding x = ↑x

Tactic:
by
  have : Fintype <| Iio x := Nat.fintypeIio x
  rw [← type_Iio_lt, type_fintype, Nat.cast_inj]
  nth_rw 2 [← Fintype.card_fin x]
  exact Fintype.card_congr Fin.equivSubtype.symm

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

Goal state before:
pp: b k n : ℕ
hk : k > 0
hb : 1 ≥ b
this : (k - 1) / k = 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
by grind [clog_of_left_le_one, Nat.pow_le_one_iff]

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

Goal state before:
pp: case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
· rcases Nat.lt_or_ge 1 b with hb | hb
    · refine eq_of_forall_lt_iff fun c ↦ ?_
      rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']
    · suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
      apply Nat.div_eq_of_lt
      grind

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

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (derivFamily f (o✝ + 1)) = derivFamily f (o✝ + 1)

Tactic:
rw [derivFamily_add_one]

Goal state after:
case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o✝ : Ordinal.{u}
a✝ : f i (derivFamily f o✝) = derivFamily f o✝
⊢ f i (nfpFamily f (derivFamily f o✝ + 1)) = nfpFamily f (derivFamily f o✝ + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ log b x ≤ x ∧ x < b ^ (log b x + 1)

Tactic:
use opow_log_le_self b hx, lt_opow_succ_log_self hb x

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

Goal state before:
pp: case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ derivFamily f (o + 1) ≤ a

Tactic:
rw [derivFamily_add_one]

Goal state after:
case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ nfpFamily f (derivFamily f o + 1) ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| a - ω ^ log ω a

Tactic:
left; rw [← div_add_mod a (ω ^ log ω a), hn]

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| ω ^ log ω a * ↑n + a % ω ^ log ω a
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}
⊢ a ∈ s → x < a → ∀ x_1 ∈ s, y < x_1 → ∃ b ∈ s, op x y < b

Tactic:
has

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
⊢ x < a → ∀ x_1 ∈ s, y < x_1 → ∃ b ∈ s, op x y < b
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 * (↑n + 1) ≤ a

Tactic:
Ordinal.mul_le_iff_le_div,

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ a / ω ^ log ω a

case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
⊢ a.card ≤ b.card ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, Ordinal.card_le_card⟩
  rw [← ha.le_ord_iff_card_le] at h
  grw [h, ord_card_le]

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

Goal state before:
pp: o : Ordinal.{u}
ho : o ≤ 1
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
by
  rcases le_one_iff.1 ho with (rfl | rfl)
  · exact isPrincipal_zero
  · exact isPrincipal_add_one

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

Goal state before:
pp: o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Tactic:
exact ⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩

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

Goal state before:
pp: case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ 0)

Tactic:
rw [opow_zero]

Goal state after:
case inl.inl
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
obtain rfl | h := eq_or_ne o 0
  · simp
  · exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

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

Goal state before:
pp: case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : #↑s < (lift.{u + 1, u} (⨆ i, ↑(f i) + 1)).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
← lift_cof,

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : #↑s < Cardinal.lift.{u + 1, u} (⨆ i, ↑(f i) + 1).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u, u + 2} (lift.{u + 2, u + 1} (typeLT ↑s)).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
← lift_cof,

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u, u + 2} (Cardinal.lift.{u + 2, u + 1} (typeLT ↑s).cof)
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : o.card ≤ c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
by
  rw [← Cardinal.lift_le] at hι
  simpa using card_iSup_Iio_le_of_lift hι hf

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

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

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

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ StrictMono fun a ↦ ↑n * a

Tactic:
by
  match n, hn with
  | 1, _ => simpa using! strictMono_id
  | (n + 1) + 1, hneq1 =>
    intro a μ hlt
    push_cast
    conv_lhs => rw [add_mul, one_mul]
    conv_rhs => rw [add_mul, one_mul]
    refine Cardinal.add_lt_add ?_ hlt
    simpa using! (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)

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

Goal state before:
pp: ⊢ (lift.{v, u + 1} (typeLT Ordinal.{u})).cof = Cardinal.univ.{u, v}

Tactic:
← lift_cof,

Goal state after:
⊢ Cardinal.lift.{v, u + 1} (typeLT Ordinal.{u}).cof = Cardinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case add_one
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ derivFamily f (b + 1) < c.ord

Tactic:
rw [derivFamily_add_one]

Goal state after:
case add_one
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ nfpFamily f (derivFamily f b + 1) < c.ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #↑(Iio b) < (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof

Tactic:
← lift_cof,

Goal state after:
case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #↑(Iio b) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
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
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z :
  l none • b i +
      (linearCombination R
          ((fun o ↦
              match o, b i, v with
              | Option.some x, x_1, f => f x
              | none, y, x => y) ∘
            Option.some))
        l.some =
    l' none • b i +
      (linearCombination R
          ((fun o ↦
              match o, b i, v with
              | Option.some x, x_1, f => f x
              | none, y, x => y) ∘
            Option.some))
        l'.some
⊢ l = l'

Tactic:
change _ + linearCombination R v l.some = _ + linearCombination R v l'.some at z

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
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
⊢ l = l'
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:
apply DFinsupp.induction x

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

case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S

Tactic:
· rintro x ⟨v, rfl⟩
    exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

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

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ (single j x) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩

Tactic:
single_eq_of_ne hj,

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ 0 = (single ⟨i, j⟩ x) ⟨i, j'⟩
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Tactic:
rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]

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

Goal state before:
pp: case mk.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ i ∈ (↑((fun ys ↦ ⟨↑⟨sf, hf⟩ + ↑ys, ⋯⟩) ⟨sg, hg⟩)).toFinset,
      ((fun i ↦ ↑(φ i)) i)
        (({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } +
            { toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ })
          i) =
    ∑ i ∈ (↑⟨sf, hf⟩).toFinset, ((fun i ↦ ↑(φ i)) i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } i) +
      ∑ i ∈ (↑⟨sg, hg⟩).toFinset, ((fun i ↦ ↑(φ i)) i) ({ toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ } i)

Tactic:
simp only [AddMonoidHom.toZeroHom_coe, coe_add, coe_mk', Pi.add_apply, map_add,
      Finset.sum_add_distrib]

Goal state after:
case mk.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (f x) + ∑ x ∈ (sf + sg).toFinset, (φ x) (g x) =
    ∑ x ∈ sf.toFinset, (φ x) (f x) + ∑ x ∈ sg.toFinset, (φ x) (g x)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f r

Tactic:
conv_rhs => rw [← mul_one r, ← smul_eq_mul]
  rw [map_smul, smul_eq_mul, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : 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 : ι
mem : i ∈ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i

pp: case neg
ι : 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 : ι
mem : i ∉ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i

Tactic:
· rw [mk_of_mem mem, hg]

Goal state after:
case neg
ι : 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 : ι
mem : i ∉ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i