mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
← inv_le_inv_of_neg (inv_lt_zero'.2 hb) ha,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ b⁻¹⁻¹ ≤ a⁻¹ ↔ b ≤ a⁻¹
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Icc a b)

Tactic:
by
  convert! sub_inv_antitoneOn_Icc_left hb
  exact (sub_zero _).symm

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
a : γ
l : List γ
x✝ : List β
⊢ Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b ↦ R (f c) b) (a :: l) x✝

Tactic:
by simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Tactic:
exact exists_mul_left_lt₀ hc

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head✝ :: tail✝)
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
obtain - | ⟨hbc, tbc⟩ | btc := h2

Goal state after:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr.nil
α : Type u
hα : Subsingleton α
l2 : List α
hl : [].length = l2.length
⊢ [] = l2

Tactic:
cases l2

Goal state after:
case mpr.nil.nil
α : Type u
hα : Subsingleton α
hl : [].length = [].length
⊢ [] = []

case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mpr.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
l2 : List α
hl : (head✝ :: tail✝).length = l2.length
⊢ head✝ :: tail✝ = l2

Tactic:
cases l2

Goal state after:
case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

case mpr.cons.cons
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : Div M
l l_n l_d n d : M
h : l = l_n / l_d
hn : l_n = n
hd : l_d = d
⊢ l = n / d

Tactic:
by
  rw [h, hn, hd]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)

Tactic:
ha',

Goal state after:
case pos
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : a' = a
⊢ f a * f a ^ count a as = f a ^ (count a as + 1)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1

Tactic:
rw [dropLast_eq_take, mem_take_iff_idxOf_lt ha]

Goal state after:
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a

Tactic:
foldl_cons,

Goal state after:
α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f (f a b) l = a
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d

Tactic:
exact Rat.divInt_mul_left (mod_cast ha)

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsNNRat a n.succ d → IsNNRat a⁻¹ d n.succ

Tactic:
rintro ⟨_, rfl⟩
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  exact ⟨this, by simp⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat n.succ) d → IsRat a⁻¹ (Int.ofNat d) n.succ

Tactic:
rintro ⟨_, rfl⟩
  have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
  exact ⟨this, by simp⟩

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b

Tactic:
rcases h with ⟨c, rfl⟩

Goal state after:
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s

Tactic:
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]

Goal state after:
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
i_ne_j : ¬i = j
⊢ False

Tactic:
exact Disjoint.ne_of_mem (Es_disj i_ne_j) hix hjx rfl

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ (Pairwise fun x y ↦ r ↑x ↑y) ↔ s.Pairwise r

Tactic:
by
  simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s

Tactic:
rcases eq_or_lt_of_le hxy with (rfl | hxy')

Goal state after:
case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r y x
⊢ False

Tactic:
exact ht hy hx hne.symm h

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = -↑q

Tactic:
← h.out,

Goal state after:
a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = -(a / -b)
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = maxDefault 1 a

Tactic:
← sup_eq_maxDefault

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = (fun x1 x2 ↦ max x1 x2) 1 a
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = maxDefault 1 a⁻¹

Tactic:
← sup_eq_maxDefault

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = (fun x1 x2 ↦ max x1 x2) 1 a⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
rw [factorial_succ (i + _), Nat.add_mul, Nat.one_mul]

Goal state after:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k j : ℕ
⊢ n.ascFactorial (j + 1) ≤ (j + 1)! * n ^ (j + 1)

Tactic:
by
    rcases n.eq_zero_or_pos with rfl | hn
    · simp [zero_ascFactorial]
    rw [ascFactorial_succ, factorial_succ, pow_succ',
      Nat.mul_assoc (j + 1), Nat.mul_left_comm j !, ← Nat.mul_assoc (j + 1)]
    refine Nat.mul_le_mul ?_ (ascFactorial_le_factorial_mul_pow n j)
    rw [add_one_mul, Nat.add_comm, Nat.add_le_add_iff_right]
    exact Nat.le_mul_of_pos_right j hn

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hb, hba⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by lia
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ p /ₛ p = 1

Tactic:
← one_mul (p /ₛ p),

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ 1 * (p /ₛ p) = 1
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ a ::ₘ as = b ::ₘ bs → a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
intro eq

Goal state after:
case mp
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ {b} ⊆ s

Tactic:
singleton_subset

Goal state after:
case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ b ∈ s
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ n = xs.length - n'

Tactic:
rwa [Nat.sub_sub_self]

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n → ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a

pp: case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n

Tactic:
· intro H s' hs' s'_card
    by_contra! rid
    have card := card_le_card (monotone_filter_left P hs') |>.trans H
    exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)

Goal state after:
case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ s ∩ replicate n x = replicate (min (count x s) n) x

Tactic:
by
  rw [inter_comm, replicate_inter, min_comm]

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : ¬a ∈ s
⊢ filter p (s.erase a) - filter p t = filter p s - filter p t

Tactic:
· rw [erase_of_notMem m]

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ [].inits ↔ s <+: []

Tactic:
by simpa only [inits, mem_singleton]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
← val_inj

Goal state after:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons.inl
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

pp: case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs

Tactic:
· exact singleton a

Goal state after:
case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs
Module: Mathlib.Data.Finset.SDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x \ s) {t | s ⊆ t}

Tactic:
by
  grind [Set.InjOn, sdiff_union_of_subset]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
rw [mem_compl, not_not]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
h : (image f s).Nontrivial
⊢ s.Nontrivial

Tactic:
by
  simp only [Finset.Nontrivial, coe_image] at h ⊢
  exact Set.nontrivial_of_image _ _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)

Tactic:
simp_rw [map_eq_image]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (⇑f) (s.erase a) = (image (⇑f) s).erase (f a)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #s = #t

Tactic:
calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #s.attach

case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

Tactic:
exact (NeZero.ne 0 rfl).elim

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

Tactic:
exact (NeZero.ne 0 rfl).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
have hinj' : Set.InjOn f' s.attach := fun x hx y hy hxy ↦ Subtype.ext (hinj _ _ x.2 y.2 hxy)

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2.inl
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) j.castSucc j.castSucc → r (f j.castSucc) (f j.castSucc)
hij✝ : j.castSucc ≤ j.castSucc
hij : ↑j.castSucc = ↑j.castSucc
⊢ r (f j.castSucc) (f j.succ)

Tactic:
exact H _

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ ↑(a.castLT ⋯ - b.castLT hb) = ↑(a - b) + n - m

Tactic:
simp only [val_sub, val_castLT]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ (n - ↑b + ↑a) % n = (m - ↑b + ↑a) % m + n - m
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map (f ∘ ⇑σ) (finRange n) ~ map f (finRange n)

Tactic:
← map_map

Goal state after:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.refine_2
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}

Tactic:
exact fun h => ⟨x, by grind⟩

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := ⋯
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ f m ∈ image (fun i ↦ f ↑i) univ

Tactic:
exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
⊢ WellFounded r

Tactic:
cases nonempty_fintype α
  have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
    Finset.card_lt_card <| by
      simp_rw [lt_iff_le_not_ge, Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
  exact Subrelation.wf (this _ _) (measure _).wf

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
⊢ Injective (snoc x x₀) ↔ Injective x ∧ ¬x₀ ∈ Set.range x

Tactic:
by
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩
  · simpa [Function.comp] using h.comp (Fin.castSucc_injective _)
  · rintro ⟨i, hi⟩
    rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi
    exact ne_last_of_lt i.castSucc_lt_last hi

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
a : α
⊢ Infinite (Equiv.Perm α)

Tactic:
exact Infinite.of_injective _ (Equiv.swap_injective_of_left a)

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ hs.toFinset.Nonempty ↔ s.Nonempty

Tactic:
by
  rw [← Finset.coe_nonempty, Finite.coe_toFinset]

Goal state after:
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ foldl op b (a ::ₘ s) = fold op (op b a) s

Tactic:
foldl_cons,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ foldl op (op b a) s = fold op (op b a) s
Module: Mathlib.Data.List.Range

Goal state before:
pp: case succ.succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m + 1 < n + 1 → r m m.succ
⊢ IsChain r (range (n + 1) ++ [n + 1]) ↔ ∀ (m : ℕ), m < n + 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (List.map f s.toList).prod = (map f s).prod

Tactic:
by
  rw [← Multiset.prod_coe, ← Multiset.map_coe, coe_toList]

Goal state after:
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.cons.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun x1 x2 ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

Tactic:
exact head_le_of_lt hmas

Goal state after:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (a :: l).rotate n = a :: l

Tactic:
rw [hb, rotate_replicate]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (s.toList.erase a).prod = s.toList.prod

Tactic:
List.prod_erase (mem_toList.2 h)

Goal state after:
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ s.toList.prod = s.toList.prod