mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ b / a = (a / b)⁻¹

pp: case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1

Tactic:
inv_div

Goal state after:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ b / a = b / a

case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
by
  rw [← not_iff_not, not_or]; exact add_ne_top

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : a ≤ c
h2 : b ≤ c - a
⊢ a + b ≤ c

Tactic:
by
  grw [h2, add_tsub_cancel_of_le h]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b

Tactic:
by rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
m n : ℕ
⊢ -⊤ = ⊤

Tactic:
by ext; simp; simp [bot_eq_zero]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = 0 ↔ p 0

Tactic:
simp [find_eq_iff]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ b ≤ unbotD a y

Tactic:
le_unbotD_iff

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ ↑b ≤ y

α : Type u_1
inst✝ : PartialOrder α
y : WithBot α
a b : α
hy : ↑b ≤ y
⊢ y ≠ ⊥
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rw [findGreatest_of_not hk, ihk]
      grind

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

Goal state before:
pp: case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)

pp: case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)

Tactic:
· rwa [h]

Goal state after:
case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Tactic:
exact ih

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min ↑a ↑b ≤ ↑c ↔ min a b ≤ c

Tactic:
by
  simp only [WithZero.coe_le_coe, min_le_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n

Tactic:
by
  rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h <;> constructor
  · intro a b hab
    obtain ⟨c, hc⟩ := exists_between (WithBot.coe_lt_coe.mpr hab)
    induction c with
    | bot => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
  · simpa [WithBot.exists, WithBot.forall, exists_lt] using DenselyOrdered.dense

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
ha : 0 < a
b c : G₀
⊢ (Equiv.divRight₀ a ⋯) b ≤ (Equiv.divRight₀ a ⋯) c ↔ b ≤ c

Tactic:
simp only [Equiv.divRight₀_apply, div_eq_mul_inv]
    exact mul_le_mul_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
a b : α
⊢ (a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b

Tactic:
simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
    neg_add_rev, neg_neg, add_assoc]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
⊢ Subtype.val '' x ∈ 𝒫 S

Tactic:
rintro _ ⟨a : S, _, rfl⟩

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
a : ↑S
left✝ : a ∈ x
⊢ ↑a ∈ S
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ioo a b
⊢ ¬a ≤ b

Tactic:
by simpa using Set.ext_iff.mp h b

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioo a b = Ioc a b
⊢ ¬a < b

Tactic:
by simpa using Set.ext_iff.mp h b

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ BddAbove (range fun x ↦ f x ⊔ g x)

Tactic:
have ⟨af, haf⟩ := hf

Goal state after:
ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
⊢ BddAbove (range fun x ↦ f x ⊔ g x)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)

Tactic:
insert_eq

Goal state after:
γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (max a b)

Tactic:
insert_eq

Goal state after:
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a

Tactic:
le_one_div (@zero_lt_one α _ _ _ _ _) h1,

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ a ≤ 1 / 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
ha : 0 < a
⊢ 0 < a / b ↔ 0 < b

Tactic:
by
  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a + 2⁻¹ ≤ 1

Tactic:
← le_sub_iff_add_le

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval

Tactic:
by
  simp only [eval_cons, h, zpow'_neg, div_eq_mul_inv, mul_inv]
  ac_rfl

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)
⊢ (map (fun k ↦ f (k + 1) / f k) (range n)).prod = f n / f 0

Tactic:
rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

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

Goal state before:
pp: q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
constructor
  · rintro ⟨qr, rfl⟩
    rw [Rat.mul_self_num, mul_self_den]
    simp only [IsSquare.mul_self, and_self]
  · rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
    refine ⟨nr / dr, ?_⟩
    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑q.den / ↑q.num = (↑q.num / ↑q.den)⁻¹

Tactic:
inv_div

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑q.den / ↑q.num = ↑q.den / ↑q.num
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.negOfNat a).pow b = Int.ofNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc,
    ← h1]
  simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g ∘ f '' t) = sSup ((fun b ↦ g (f b)) '' t)

Tactic:
comp_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup ((fun x ↦ g (f x)) '' t) = sSup ((fun b ↦ g (f b)) '' t)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : SupSet α
inst✝ : SupSet β
f : ι → α × β
⊢ sSup (range (swap ∘ f)) = sSup (range fun i ↦ (f i).swap)

Tactic:
comp_def

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
a : α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1 ∈ Iio a, w < a_1

Tactic:
simpa [and_comm] using exists_between hw

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc a b

Tactic:
inf_eq_left.2 h,

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ Icc a (a ⊔ b) = Icc a b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo (min a b) (max a b) = Ioo a b

Tactic:
inf_eq_left.2 h,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ioo a (max a b) = Ioo a b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ∉ uIoo a b

Tactic:
by simp +contextual [uIoo, le_of_lt]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ∉ uIoo a b

Tactic:
by simp +contextual [uIoo, le_of_lt]

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
have : Std.Symm fun a b ↦ a ≺ b ∨ b ≺ a := { symm _ _ := Or.symm }

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
this : Std.Symm fun a b ↦ r a b ∨ r b a
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
by simpa using of_decide_eq_false h

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = (|a|ₘ / a)⁻¹

Tactic:
inv_div

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = a / |a|ₘ
Module: Mathlib.Data.Nat.Factorial.Basic

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

pp: case step
i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + m✝.succ ! < (i + m✝.succ)!

Tactic:
· rw [factorial_one]
    exact lt_factorial_self (succ_le_succ hi)

Goal state after:
case step
i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + m✝.succ ! < (i + m✝.succ)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !

Tactic:
by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ < 1 / (1 - a⁻¹)

Tactic:
convert ceil_lt_add_one (R := k) _

Goal state after:
case e'_4
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ b ∈ {a} ↔ b = a

Tactic:
by
  simp only [← cons_zero, mem_cons, iff_self, or_false, notMem_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
a : α
hx : a ∈ xs
hy : a ∈ ys.dedup
⊢ False

Tactic:
exact h hx (mem_dedup.mp hy)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ t

Tactic:
induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l ~ l'

Tactic:
by
  rw [← Multiset.coe_eq_coe]
  exact Multiset.Nodup.toFinset_inj hl hl' h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ s ∩ t = 0

Tactic:
ext,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val.dedup

Tactic:
dedup_eq_self

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map Subtype.val univ.val = (filter p univ).val

Tactic:
by
  apply (map_val (Function.Embedding.subtype p) univ).symm.trans
  apply congr_arg
  apply univ_map_subtype

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x✝ : ↥(map f s)
x : β
hx : x ∈ map f s
⊢ ∃ a, (fun x ↦ ⟨f ↑x, ⋯⟩) a = ⟨x, hx⟩

Tactic:
obtain ⟨x, hxs, rfl⟩ := mem_map.mp hx
    exact ⟨⟨x, hxs⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.dedup = s.val

Tactic:
dedup_eq_self

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val = s.val
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v

Tactic:
rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega

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

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩

Tactic:
← Fin.val_ne_iff

Goal state after:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mp
α : 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
b : β
h : b ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ b ∈ t

Tactic:
obtain ⟨_, _, rfl⟩ := mem_image.1 h

Goal state after:
case calc_2.mp
α : 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
w✝ : ↥s
left✝ : w✝ ∈ s.attach
h : i ↑w✝ ⋯ ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ i ↑w✝ ⋯ ∈ t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0

Tactic:
rw [Nat.eq_zero_of_le_zero h]

Goal state after:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
· grind [castSucc_ne_zero_iff]

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

Goal state before:
pp: case inr.hf
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := ⋯
⊢ Set.MapsTo f' ↑s ↑t

Tactic:
aesop (add safe unfold Set.MapsTo)

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

Goal state before:
pp: n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i ≠ last n

Tactic:
rw [← lt_last_iff_ne_last] at hj ⊢; exact Fin.lt_of_le_of_lt h hj

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.succ ≤ p

Tactic:
iff_false_right (Fin.not_le.2 H),

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬p.succAbove i < p
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
iff_false_right (Fin.not_le.2 H),

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < p.succAbove i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = p 0

Tactic:
by
  rw [← cons_succ x p]; rfl

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = p (last n)

Tactic:
by
  rw [← cons_succ x p]; rfl

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]

Tactic:
by
  induction h with
  | cons_mem h => simp [ne_nil_of_mem h]
  | cons_duplicate h => simp [ne_nil_of_mem h.mem]

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

Goal state before:
pp: case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

pp: case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
· have : i < n := Nat.lt_of_succ_lt_succ h
      simp [addCases, this]

Goal state after:
case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
i : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j
⊢ i.castSucc = j

Tactic:
induction j using lastCases with
    | cast j =>
      simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h
    | last =>
      simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ (if hlt : j < i then ⋯ ▸ p (j.castPred ⋯) else ⋯ ▸ p (j.pred ⋯)) = ⋯ ▸ p (j.castPred ⋯)

Tactic:
dif_pos h

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ ⋯ ▸ p (j.castPred ⋯) = ⋯ ▸ p (j.castPred ⋯)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ i.succ.insertNth x (cons a p) (i.succ.succAbove j) = cons a (i.insertNth x p) (i.succ.succAbove j)

Tactic:
simp only [insertNth_apply_succAbove]
    cases j using Fin.cases <;> simp

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

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ i.succ.insertNth x (cons a p) (i.succ.succAbove j) = cons a (i.insertNth x p) (i.succ.succAbove j)

Tactic:
| p j =>

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

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
have := Classical.decEq α
  rw [← toFinset_card, toFinset_ofPred, Finset.filter_ne',
    Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
⊢ Fin.find p h = 0 ↔ p 0

Tactic:
simp [find_eq_iff]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ s = insert a s

Tactic:
insert_eq

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ s = {a} ∪ s
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
l : List α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a

Tactic:
induction l using twoStepInduction with
  | nil | singleton => simp
  | cons_cons a b l IH IH2 =>
    simp +contextual [isChain_cons_cons, eq_comm, IH2, replicate_succ]

Goal state after: