mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (x y : A) (b : α), (x * y) • b = x • y • b

Tactic:
simp [Equiv.smul_def, mul_smul]

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

Goal state before:
pp: case a
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'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ M'

Tactic:
· rw [← H]
    exact le_iSup ..

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosedOn univ s ↔ DirSupClosed s

Tactic:
simp [DirSupClosedOn, DirSupClosed]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f ⁻¹' Iic x) ∈ f ⁻¹' Iic x

Tactic:
rw [mem_preimage, hf.map_sSup h₁ h₂]

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (f '' f ⁻¹' Iic x) ∈ Iic x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
exact (Ordinal.add_sub_cancel_of_le h).ge

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

Goal state before:
pp: α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (f.transPrincipal (typein s)).toRelEmbedding a = (typein r).toRelEmbedding a

Tactic:
(f.transPrincipal _).eq

Goal state after:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (PrincipalSeg.toRelEmbedding ?g) a = (typein r).toRelEmbedding a

case g
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ r ≺i fun x1 x2 ↦ x1 < x2
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
⊢ b < a ∧ ∀ a_1 < a - b, succ a_1 < a - b

Tactic:
refine ⟨h, fun c hc ↦ ?_⟩

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : c < a - b
⊢ succ c < a - b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
rwa [bddAbove_add_one_image_iff]

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ enumOrd s o ∈ s ∩ {b | ∀ c < o, enumOrd s c < b}

Tactic:
by
  rw [enumOrd]
  exact csInf_mem (enumOrd_nonempty hs o)

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

Goal state before:
pp: case e_6
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a = 0

Tactic:
rw [← lt_one_iff]

Goal state after:
case e_6
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a < 1
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:
by
  simp_rw [Iio, bsup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_ofPred]

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

Goal state before:
pp: case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ ∃ x, IsTop x

pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
⊢ typeLT α ∈ range succ

Tactic:
· refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
    · rw [mem_Iio, ← ha, lt_succ_iff]
    · rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]
      exact typein_lt_type ..

Goal state after:
case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : α
ha : IsTop a
⊢ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
⊢ o ≤ lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding

Tactic:
by_contra! h

Goal state after:
o : Ordinal.{u}
h : lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding < o
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
← csSup_Iic (a := o),

Goal state after:
o : Ordinal.{u_3}
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = sSup (Iic o)
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · by_contra! hf
    exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))
  rintro ⟨_, _, hf⟩
  rw [succ_le_iff, ← hf]
  exact lt_blsub _ _ _

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
⊢ ↑n < o.card ↔ ↑n < o

Tactic:
rw [← natCast_add_one_le_iff, ← succ_le_iff, ← Nat.cast_add_one, nat_le_card]
  rfl

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hmltl : m < l
hlt : ∀ i ∈ l, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
replace hmltl : List.Lex (· < ·) m l := hmltl

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : l.SortedGT
hm : m.SortedGT
hlt : ∀ i ∈ l, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 ↦ x1 < x2) m l
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d

Tactic:
by
  obtain rfl | hd := eq_or_ne d 0
  · rw [mul_zero, div_zero, div_zero]
  · have H := mul_ne_zero hc.ne_zero hd
    apply le_antisymm
    · rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]
      · grw [hc, ← mul_succ]
        gcongr
        rw [succ_le_iff]
        exact lt_mul_succ_div b hd
    · grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

Tactic:
by
  grind [lt_mul_iff]

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

Goal state before:
pp: b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

Tactic:
by
  grind [lt_mul_iff]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n

Tactic:
rw [div_lt_iff_lt_mul (by lia), ← succ_le_iff, ← pred_eq_sub_one,
    succ_pred_eq_of_pos (by lia)]
  exact Nat.add_le_mul hn hb

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

Goal state before:
pp: case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m < ↑(n * (m / n).succ)

Tactic:
Nat.cast_lt,

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m < n * (m / n).succ
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x y : ℕ
⊢ clog b x ≤ y ↔ x ≤ b ^ y

Tactic:
by
  fun_cases clog with
  | case1 h =>
    rcases clog.go_spec h.2 hb (Nat.lt_pow_self hb) with ⟨-, H₁, H₂⟩
    cases Nat.lt_or_ge (clog.go x b x).2 y with
    | inl hy =>
      rw [← Nat.add_one_le_iff] at hy
      exact iff_of_true hy <| Nat.le_trans H₂ <| Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy
    | inr hy =>
      apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]
      exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁
  | case2 h => grind [Nat.one_le_pow]

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ¬BddAbove (⋂ i, fixedPoints (f i))

Tactic:
by
  rw [not_bddAbove_iff]
  refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
  rintro _ ⟨i, rfl⟩
  exact nfpFamily_fp (H i) _

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
⊢ o / b ^ log b o < b

Tactic:
← lt_mul_iff_div_lt (opow_pos _ (zero_lt_one.trans hb)).ne',

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ log b o * b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 1 ≤ o / 2 ^ log 2 o

Tactic:
· simpa [one_le_iff_ne_zero, pos_iff_ne_zero] using div_opow_log_pos 2 ho

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
⊢ 2 ^ x < preBeth o

Tactic:
obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx

Goal state after:
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 o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ ∃ r, (∀ (x : α), #{ y // ¬r x y } < #α) ∧ ∀ (y : α), #{ x // r x y } < #α

Tactic:
obtain ⟨α, _, hα⟩ := exists_ord_eq_type_lt α

Goal state after:
α✝ : Type u_1
inst✝ : Infinite α✝
α : LinearOrder α✝
w✝ : WellFoundedLT α✝
hα : (#α✝).ord = typeLT α✝
⊢ ∃ r, (∀ (x : α✝), #{ y // ¬r x y } < #α✝) ∧ ∀ (y : α✝), #{ x // r x y } < #α✝
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:
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.Cardinal.Ordinal

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card (max a.card b.card) ≤ max a.card (b.card + 1)

Tactic:
rw [← max_assoc, max_self]

Goal state after:
case add_one
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ max a.card b.card ≤ max a.card (b.card + 1)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case add_one.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ (a ^ b).card ≠ 0

Tactic:
rw [ne_eq, card_eq_zero, opow_eq_zero]
      rintro ⟨rfl, -⟩
      cases omega0_pos.not_ge ha

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

Goal state before:
pp: case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card

Tactic:
rwa [aleph0_le_card]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (f a).IsFundamentalSequence o fun b hb ↦ f (g b hb)

Tactic:
refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
  · grind [Ordinal.IsFundamentalSequence, cof_map_of_isNormal]
  · rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]
    exact IsNormal.blsub_eq.{u, u} hf ha

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

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card

Tactic:
rwa [aleph0_le_card]

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

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
⊢ ∃ a, #β ≤ #↑(f ⁻¹' {a})

Tactic:
by_contra! h

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ False
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑Set.univ < #?m.36

pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.37

Tactic:
rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion]

Goal state after:
β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ #↑(⋃ i, ?m.51 ⁻¹' {i}) < #?m.48

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.44

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ Type ?u.43

β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
h : ∀ (a : α), #↑(f ⁻¹' {a}) < #β
⊢ ?m.48 → ?m.50
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ω ≤ o

Tactic:
exact omega0_le_of_isSuccLimit hc.1

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ lift.{u_1, u_1 + 1} #↑(Iio a) < (lift.{u_1 + 1, u_1} c).ord.cof

pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c

Tactic:
· rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : ⟨i, xi⟩ = ⟨j, xj⟩
⊢ single i xi = single j xj

Tactic:
by
  cases h
  rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
⊢ equivFunOnFintype.symm (Pi.single i m) = single i m

Tactic:
simp only [← single_eq_pi_single, equivFunOnFintype_symm_coe]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
a✝¹ b✝ : { l // ∀ (i : ι), i ∈ l }
a✝ : a✝¹ ≈ b✝
a : (i : ι) → α i
⊢ Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧ = Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧

Tactic:
Quotient.map_mk

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)
h1 : ∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1
h2 : ∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1
⊢ f1.prod g1 = f2.prod g2

Tactic:
rw [prod_of_support_subset Finset.subset_union_left h1,
    prod_of_support_subset Finset.subset_union_right h2]
  exact Finset.prod_congr rfl h

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange f hf x = single i u
⊢ f i (x i) = u

Tactic:
by simpa using congr($hx i)

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
i : ι
⊢ 0 ≍ 0

Tactic:
by rw [Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = ((evalEquiv R M) ((evalEquiv R M).symm g)) f

Tactic:
evalEquiv_apply,

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = ((Dual.eval R M) ((evalEquiv R M).symm g)) f
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective (⇑(Dual.eval R M) ∘ ⇑e.symm)
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_2
x : FreeAbelianGroup X
⊢ toFreeAbelianGroup (toFinsupp x) = x

Tactic:
← AddMonoidHom.comp_apply,

Goal state after:
X : Type u_2
x : FreeAbelianGroup X
⊢ (toFreeAbelianGroup.comp toFinsupp) x = x
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
f : X →₀ ℤ
⊢ toFinsupp (toFreeAbelianGroup f) = f

Tactic:
← AddMonoidHom.comp_apply,

Goal state after:
X : Type u_1
f : X →₀ ℤ
⊢ (toFinsupp.comp toFreeAbelianGroup) f = f
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ a.support ↔ (coeff x) a ≠ 0

Tactic:
support,

Goal state after:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ (toFinsupp a).support ↔ (coeff x) a ≠ 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∉ a.support ↔ (coeff x) a = 0

Tactic:
support,

Goal state after:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∉ (toFinsupp a).support ↔ (coeff x) a = 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
⊢ (of x).support = {x}

Tactic:
support,

Goal state after:
X : Type u_1
x : X
⊢ (toFinsupp (of x)).support = {x}
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq α
h : t.Nonempty
⊢ ↑(image₂ (fun x x_1 ↦ x) s t) = ↑s

Tactic:
push_cast
    exact image2_left h

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

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
by
    classical
    obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
    obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
    obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
    exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ n * X

Tactic:
← ih,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = (monomial n) 1 * X
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n

Tactic:
by
  rw [mul_assoc, X_pow_mul, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
by
  rw [X, H, monomial_zero_right, support_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp =
    ∑ x ∈ p.support, ∑ i ∈ q.support, ((monomial (x + i)) (p.toFinsupp.coeff x * q.toFinsupp.coeff i)).toFinsupp

Tactic:
support,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp =
    ∑ x ∈ p.toFinsupp.coeff.support,
      ∑ i ∈ q.toFinsupp.coeff.support, ((monomial (x + i)) (p.toFinsupp.coeff x * q.toFinsupp.coeff i)).toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
support_update,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ Nontrivial R[X]

Tactic:
refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial R[ℕ]
x y : R[ℕ]
hxy : x ≠ y
⊢ { toFinsupp := x } ≠ { toFinsupp := y }
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (((lmapDomain R R g) l).sum fun i a ↦ a • id i) ∈ s

Tactic:
Finsupp.lmapDomain_apply,

Goal state after:
case a.refine_2.left
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ((mapDomain g l).sum fun i a ↦ a • id i) ∈ s
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
intro H l
    obtain ⟨l', hl'⟩ := H (l.length + 1)
    exact ⟨l', by simp [hl']⟩

Goal state after: