mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
List.erase,

Goal state after:
case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a *
      (match b == a with
        | true => l
        | false => b :: l.erase a).prod =
    (b :: l).prod
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < zpow' x r

Tactic:
rw [zpow'_of_ne_zero_left _ _ hx.ne']

Goal state after:
M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < x ^ r
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
f : α → Bool
⊢ countP f l + countP (fun a ↦ decide ¬f a = true) l = countP f l + countP (fun x ↦ !f x) l

Tactic:
Bool.not_eq_true,

Goal state after:
α : Type u
l : List α
f : α → Bool
⊢ countP f l + countP (fun a ↦ decide (f a = false)) l = countP f l + countP (fun x ↦ !f x) l
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
h : q.den = 1
⊢ q = ↑q.num

Tactic:
exact (Rat.coe_int_num_of_den_eq_one h).symm

Goal state after:
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q * ↑q.den = ↑q.num

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d

Tactic:
rw [mul_assoc, mul_right_inj' ha]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
⊢ IsPrimal (m * n)

Tactic:
by
  obtain rfl | h0 := eq_or_ne m 0; · rwa [zero_mul]
  intro b c h
  obtain ⟨a₁, a₂, ⟨b, rfl⟩, ⟨c, rfl⟩, rfl⟩ := hm (dvd_of_mul_right_dvd h)
  rw [mul_mul_mul_comm, mul_dvd_mul_iff_left h0] at h
  obtain ⟨a₁', a₂', h₁, h₂, rfl⟩ := hn h
  exact ⟨a₁ * a₁', a₂ * a₂', mul_dvd_mul_left _ h₁, mul_dvd_mul_left _ h₂, mul_mul_mul_comm _ _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f (i + k) = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n + k), f i

Tactic:
· simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMonoOn f s ↔ StrictMono fun a ↦ f ↑a

Tactic:
simp [StrictMono, StrictMonoOn]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ sSup (⋃ i, Iic (f i)) = ⨆ i, f i

Tactic:
by
  apply csSup_eq_csSup_of_forall_exists_le
  · rintro x ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨f i, mem_range_self _, hi⟩
  · rintro x ⟨i, rfl⟩
    exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

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

Goal state before:
pp: β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
by
  classical
  constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsLUB s (sSup s)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · simp [sSup]
  · exact isLUB_sSup' hs

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ f y.1 '' t

Tactic:
exact mem_image_of_mem _ hy.2

Goal state after:
Module: Mathlib.Order.Antichain

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

Tactic:
pairwise_union

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a) ↔
    s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ 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 α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
rw [Rat.invOf_denom_swap]

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < ↑q

Tactic:
by
  rw [Rat.cast_def]
  exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

Goal state after:
Module: Mathlib.Data.Int.CharZero

Goal state before:
pp: k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑(↑m / ↑n) = ↑m / ↑n

Tactic:
cast_div_charZero (Int.ofNat_dvd.mpr n_dvd),

Goal state after:
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℕ
n_dvd : n ∣ m
⊢ ↑↑m / ↑↑n = ↑m / ↑n
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
cases hn
  · rw [factorial_one]
    exact lt_factorial_self (succ_le_succ hi)
  exact add_factorial_succ_lt_factorial_add_succ _ hi

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y

Tactic:
round_add_intCast,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round x + -y = round x - y
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = y + round x

Tactic:
round_add_intCast,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round x + y = y + round x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑k * m.div k + ↑k

Tactic:
Nat.mul_succ

Goal state after:
m k : ℕ+
h : k ∣ m
⊢ ↑k * m.div k + ↑k = ↑k * m.div k + ↑k
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |a - b| < 1

pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ |a - b| < 1

Tactic:
· rw [abs_sub_comm]
    exact this h.symm (le_of_not_ge h0)

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ |a - b| < 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ ⌊a * ↑n⌋ / ↑n = ⌊a⌋

Tactic:
simpa using mul_cast_floor_div_cancel_of_pos (n := n) (by positivity) a

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ (fun x ↦ x ^ n) a < (fun x ↦ x ^ n) b

Tactic:
← one_lt_div',

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (fun x ↦ x ^ n) b / (fun x ↦ x ^ n) a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝³ : CommGroup G
inst✝² : PartialOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
x y : Gᵒᵈ
hy✝ : 1 < y
hy : ofDual y < 1
n : ℕ
hn : (ofDual x)⁻¹ ≤ (ofDual y ^ n)⁻¹
⊢ x ≤ y ^ n

Tactic:
inv_le_inv_iff

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst✝³ : CommGroup G
inst✝² : PartialOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
x y : Gᵒᵈ
hy✝ : 1 < y
hy : ofDual y < 1
n : ℕ
hn : ofDual y ^ n ≤ ofDual x
⊢ x ≤ y ^ n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = -⌊↑n / ↑d⌋

Tactic:
floor_natCast_div_natCast n d,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑(negOfNat n) / ↑d⌉ = -(↑n / ↑d)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat (fract r) 0

Tactic:
by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsNat (fract r) 0

Tactic:
by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat (round r) m

Tactic:
by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsInt (round r) m

Tactic:
by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : a < (c ^ ↑n)⁻¹
⊢ a < c ^ (-↑n)

Tactic:
← zpow_neg

Goal state after:
case inr.inr.inr.refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : a < c ^ (-↑n)
⊢ a < c ^ (-↑n)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inr.refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : (c ^ ↑n)⁻¹ < b
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Tactic:
← zpow_neg

Goal state after:
case inr.inr.inr.refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : c ^ (-↑n) < b
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
    (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
by
  simp only [subset_iff, not_imp_not]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
by_cases hxy : y = x

Goal state after:
case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : y = x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip r) (map f t) s ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
rel_map_left,

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (fun a b ↦ flip r (f a) b) t s ↔ Rel (fun a b ↦ r a (f b)) s t
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) _l → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → decide (p x) = decide (q x)

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : p a
⊢ decide (p a) = true

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : ¬p a
⊢ ¬decide (p a) = true

Tactic:
by simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝¹ : DecidablePred p
f : α → β
hf : Injective f
s : Multiset α
inst✝ : DecidablePred fun b ↦ ∃ a, p a ∧ f a = b
⊢ map f (filter p s) = filter (fun b ↦ ∃ a, p a ∧ f a = b) (map f s)

Tactic:
by
  simp [filter_map, hf.eq_iff]

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

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

Tactic:
count_replicate,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if x = y then n else 0) (count y s) = count y (replicate (min n (count x s)) x)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
· rw [ndinsert_of_mem h] at ht
      subst ht
      rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∪ t) = s ∪ insert a t

Tactic:
union_insert

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∪ t) = insert a (s ∪ t)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nontrivial
⊢ ∀ (a_1 : α), a_1 ∈ s ∧ a_1 ≠ a → a_1 ∈ s.erase a

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s

Tactic:
simp [@and_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
obtain h | h := (rev p).succ_le_or_le_castSucc i

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : ∀ s' ≤ s.val, n < s'.card → ∃ a ∈ s', ¬P a
s' : Finset α
hs' : s' ⊆ s
h : n < #s'
⊢ s'.val ≤ s.val

Tactic:
by simp_all

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

Goal state before:
pp: n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
rw [← val_castLE h]
  exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
obtain (rfl | h') := Fin.eq_or_lt_of_le h

Goal state after:
case inl
n : ℕ
a : Fin (n + 1)
hb : a ≠ last n
h : a ≤ a
⊢ ↑(a.castPred ⋯ - a.castPred hb) = ↑(a - a) - 1

case inr
n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
h' : a < b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
cases j using Fin.cases <;> simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

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

Goal state before:
pp: α : Type u_1
s✝ : Finset α
n : ℕ
a : α
s : Finset α
x✝² : a ∉ s
x✝¹ : #s = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
x✝ : #(cons a s x✝²) = n + 1
⊢ ∃ (h : a ∉ s), cons a s h = cons a s x✝² ∧ #s = n

Tactic:
by simp_all

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ ↑r = ↑(Fin.cast ⋯ (natAdd m r))

Tactic:
simp [hu]

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

Goal state before:
pp: case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
exact ⟨_, by rwa [← e] at this⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
⊢ False

Tactic:
obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
i : Infinite ι
s : Finset ι
c : #s = n + 1
⊢ False
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
(«tacticBy_cases_:_»
 "by_cases"
 [`h ":"]
 (choice
  (_private.Mathlib.Data.List.Sort.0.List.«term_≼__1» `a "≼" `b)
  (_private.Mathlib.Data.List.Sort.0.List.«term_≼_» `a "≼" `b)))

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : ¬r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
by
  rw [insertionSort_cons]
  cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_cons_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self

Goal state after: