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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ a⁻¹ * (y * a) = x ↔ a * x = y * a

Tactic:
inv_mul_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ y * a = a * x ↔ a * x = y * a
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den

Tactic:
simp [num_coe, den_coe]

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

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
hn : n ≠ 0
⊢ n = m * (m⁻¹ * n)

Tactic:
rw [mul_inv_cancel_left₀ (mt h hn)]

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

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ n * b

Tactic:
← e

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
← Int.cast_natCast d₁,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑n₂ * ↑↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
mul_den

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den) * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ (fun h ↦ h r) <$> pure (node v l) = pure (node v l r)

Tactic:
map_pure

Goal state after:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : BinaryTree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ pure (node v l r) = pure (node v l r)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
a : R
⊢ Odd a → 0 < a

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
k : R
⊢ 0 < 2 * k + 1
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
isLUB_iff_le_iff,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ b ∈ upperBounds s
hb₀ : ∀ (b : β), b₀ ≤ b ↔ b ∈ upperBounds t
⊢ IsLUB (image2 l s t) (l a₀ b₀)
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
isLUB_iff_le_iff,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a

Tactic:
have : Nonempty s := Set.nonempty_coe_sort.mpr hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i ∈ s, a = a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty

Tactic:
exact ⟨x, m⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a

Tactic:
have : Nonempty s := Set.nonempty_coe_sort.mpr hs

Goal state after:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
this : Nonempty ↑s
⊢ (⨆ a, ↑a) ∆ a ≤ ⨆ a_1, ↑a_1 ∆ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
exact False.elim (not_top_le_coe a (ha h₁))

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
· exact isLUB_sSup' hs

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t ≠ ∅
⊢ t.Nonempty

Tactic:
← nonempty_iff_ne_empty

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t.Nonempty
⊢ t.Nonempty
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s h.choose
⊢ SuperChain r s (SuccChain r s)

Tactic:
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c

Tactic:
obtain ⟨c, rfl⟩ := hf c

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr
m n : ℕ
hm : 1 < m
⊢ m ! = n ! ↔ n = m

Tactic:
factorial_inj hm,

Goal state after:
case inr
m n : ℕ
hm : 1 < m
⊢ m = n ↔ n = m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k

Tactic:
rw [dvd_iff]

Goal state after:
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k
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:
by
  rw [← one_le_div', ← div_zpow]; exact one_le_zpow (one_le_div'.2 hab) hn

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
⊢ f (n • a) = f 0 + n • b

Tactic:
by
  simpa using map_add_nsmul f 0 n

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

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
y : R
inst✝ : ExistsAddOfLE R
x : R
hy1 : 1 < y
⊢ ∃ n, x < y ^ n

Tactic:
obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ n, x < (1 + z) ^ n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case left
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ⋯
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ (↑q.den / ↑q.num).num = ↑q.den

Tactic:
exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Tactic:
rintro ⟨l₁⟩ ⟨l₂⟩

Goal state after:
case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a

Tactic:
← e

Goal state after:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m

Tactic:
simp at hf

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ map f m ≍ map f' m
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun a_1 ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
simp only [decide_not, bne, Bool.and_comm, decide_mem_cons, Bool.not_or]

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

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
H : ¬hd = x
⊢ (update f x y hd :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = hd ∨ x ∈ tl then (f hd :: map f tl).set (idxOf x (hd :: tl)) y else f hd :: map f tl

Tactic:
simp [Ne.symm H, H, ← apply_ite (cons (f hd))]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
by_cases h : x ∈ xs

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
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
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
by_cases h'' : n ≤ xs.length

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
⊢ List.drop n xs ~ ys ∩ List.drop n xs

case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ List.drop n xs ~ ys ∩ List.drop n xs
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ l₂ = l₁ ++ drop l₁.length l₂

Tactic:
induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ s = t

Tactic:
rw [← insert_erase hs, ← insert_erase ht, h]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
constructor <;> simp +contextual [disjoint_left]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : Fintype α
⊢ Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t

Tactic:
classical simp [codisjoint_iff, eq_univ_iff_forall, or_iff_not_imp_left]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ s ⇔ t ↔ (a ∈ s ↔ a ∈ t)

Tactic:
simp [bihimp, iff_def']

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev = j ↔ i = j.rev

Tactic:
by
  rw [← rev_inj, rev_rev]

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 2 ↔ a ≠ b

Tactic:
aesop (add simp card_insert_eq_ite)

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

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : DecidableEq α
⊢ #{a, b, c} = 3 ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
aesop (add simp card_insert_eq_ite)

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

Goal state before:
pp: case mk
α : Type u_1
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ #{ val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}

Tactic:
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]

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

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

Tactic:
simpa using congr_fun h (Fin.succ i)

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

Goal state before:
pp: case pos
n : ℕ
p i : Fin n
hi : i ≤ p
⊢ ∃ a, p.predAbove a = i

pp: case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i

Tactic:
· exact ⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩

Goal state after:
case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
obtain h | h := p.le_or_gt i

Goal state after:
case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i

case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i
Module: Mathlib.Data.Fintype.Card

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

Tactic:
← e

Goal state after:
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this✝ : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
this : Multiset.Nodup ⟦l⟧ ∧ ∀ (x : α), x ∈ ⟦l⟧
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
l : Fin n
⊢ «repeat» m.succ a (Fin.cast ⋯ (castAdd (m * n) l)) =
    (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m * n) l))

Tactic:
simp [modNat, Nat.mod_eq_of_lt l.is_lt]

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↑↑hs.toFinset = ↑s

Tactic:
hs.coe_toFinset

Goal state after:
α : Type u
s : Set α
hs : s.Finite
⊢ ↑s = ↑s
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
dif_neg (Fin.ne_of_gt h),

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
⊢ a ∉ s → s.Finite → (∀ (hts : s ⊆ s✝), motive s ⋯) → ∀ (hts : Insert.insert a s ⊆ s✝), motive (Insert.insert a s) ⋯

Tactic:
has

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
⊢ s.Finite → (∀ (hts : s ⊆ s✝), motive s ⋯) → ∀ (hts : Insert.insert a s ⊆ s✝), motive (Insert.insert a s) ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
simp_rw [← not_lt, find_lt_iff, not_exists, not_and]

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

Goal state before:
pp: case refine_1
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
l' : List α
hne : 1 < l'.length
x✝ : l' <:+: l
l₁ l₂ : List α
hl : l₁ ++ l' ++ l₂ = l
⊢ R (l'.head ⋯) (l'.getLast ⋯)

pp: case refine_2
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ R l[i] l[j]

Tactic:
· grind [getElem_append_left', getElem_append_right']

Goal state after:
case refine_2
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ R l[i] l[j]
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b

pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
· exact ⟨[], .singleton _, rfl⟩

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l

Tactic:
rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1

Goal state after:
case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
a : α
s : Multiset α
f : α → Multiset β
⊢ (a ::ₘ s).bind f = f a + s.bind f

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
a : α
f : α → Multiset β
⊢ {a}.bind f = f a

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
s t : Multiset α
f : α → Multiset β
⊢ (s + t).bind f = s.bind f + t.bind f

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ s.bind f ↔ ∃ a, a ∈ s ∧ b ∈ f a

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).card = (map (card ∘ f) s).sum

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : α → Multiset β
f : β → γ
⊢ map f (m.bind n) = m.bind fun a ↦ map f (n a)

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ (s.bind t).prod = (map (fun a ↦ (t a).prod) s).prod

Tactic:
simp [bind]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.cyclicPermutations.length
⊢ l.cyclicPermutations[n] = l.rotate n

Tactic:
cases l with
  | nil => simp
  | cons a l =>
    simp only [cyclicPermutations_cons, getElem_dropLast, getElem_zipWith, getElem_tails,
      getElem_inits]
    rw [rotate_eq_drop_append_take (by simpa using h.le)]

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

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ (∃ n, l'.rotate ↑n = l) → l ~r l'

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case mp
α : Type u
l' : List α
k : Fin l'.cyclicPermutations.length
⊢ l'.rotate ↑k ~r l'
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
← add_mul_div_left,

Goal state after:
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = (n * (n - 1) + 2 * n) / 2

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
⊢ ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (cons m a b₁ f₁ a_1 ha) (cons m a b₂ f₂ a_1 ha)

Tactic:
intro a ha
  dsimp [cons]
  split_ifs with H
  · cases H
    exact hb
  · exact hf _ _

Goal state after: