mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : κ → ι
hI : ∀ (a : κ), I a ∈ s a
⊢ ⨅ a, f (I a) ≤ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i

Tactic:
by_cases! H : ∀ k, I k = I j

Goal state after:
case pos
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : κ → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∀ (k : κ), I k = I j
⊢ ⨅ a, f (I a) ≤ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i

case neg
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : κ → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∃ k, I k ≠ I j
⊢ ⨅ a, f (I a) ≤ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

Tactic:
convert! @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2

Goal state after:
case e'_1.e'_3
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₁ b₁ = Ico b₁ a₁

case e'_1.e'_4
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
e_1✝ : Set α = Set αᵒᵈ
⊢ Ioc a₂ b₂ = Ico b₂ a₂
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h✝ : a < b ∨ c < d
h : Ico a b = Ico c d
this : c ≤ a ∧ b ≤ d
⊢ a = c ∧ b = d

Tactic:
have : a ≤ c ∧ d ≤ b := (Ico_subset_Ico_iff (show c < d by grind)).1 h.superset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h✝ : a < b ∨ c < d
h : Ico a b = Ico c d
this✝ : c ≤ a ∧ b ≤ d
this : a ≤ c ∧ d ≤ b
⊢ a = c ∧ b = d
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this : b ≤ d ∧ c ≤ a
⊢ a = c ∧ b = d

Tactic:
have : d ≤ b ∧ a ≤ c := (Ioc_subset_Ioc_iff (show c < d by grind)).1 h.superset

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this✝ : b ≤ d ∧ c ≤ a
this : d ≤ b ∧ a ≤ c
⊢ a = c ∧ b = d
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊂ Ioi a ↔ a < b

Tactic:
refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
  obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h
  exact ac.trans_le (le_of_not_gt cb)

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

Goal state before:
pp: α : Type u_6
β : Type u_7
f : α → Set β
⊢ (range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)

Tactic:
by
  aesop (add simp [PairwiseDisjoint, Set.Pairwise])

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a = φ a'

Tactic:
haa'

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a' = φ a'
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ = ↑n₂ * ⅟a₂ * a₁ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
← Int.commute_cast,

Goal state after:
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ = ⅟a₂ * ↑n₂ * a₁ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
⊢ f x = g x

Tactic:
notMem_mulSupport.1 hx,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
⊢ 1 = g x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
| fract x + ↑⌊x⌋ - ↑z

Tactic:
add_sub_assoc

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
| fract x + (↑⌊x⌋ - ↑z)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  have hn' : 0 < (n : α) := by
    norm_cast
  rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']

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

Goal state before:
pp: case hbc
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 1) + ↑(n + 1) * a ^ n * b ≤ (a + b) ^ (n + 1)

Tactic:
apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg

Goal state after:
case hbc.Hcomm
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ Commute a b

case hbc.ha
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ a

case hbc.Hsq
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ b ^ 2

case hbc.Hsq'
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ (a + b) ^ 2

case hbc.H
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ 2 * a + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x

pp: case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Tactic:
· rw [le_sub_iff_add_le, zero_add]
    exact (fract_lt_one x).le

Goal state after:
case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ ⌈↑x⌉ = ⌈x⌉

Tactic:
by
  rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ ⌈0⌉ = 0

Tactic:
rw [← cast_zero, ceil_intCast]

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 b : k
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
⊢ ↑⌈a⌉ ≤ b * a

Tactic:
· exact (ceil_lt_mul hb hba).le

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
g : G
p₁ p₂ : P
⊢ g • p₁ /ₛ p₂ = g * (p₁ /ₛ p₂)

Tactic:
apply smul_right_cancel p₂

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ (g • p₁ /ₛ p₂) • p₂ = (g * (p₁ /ₛ p₂)) • p₂
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p q : P
⊢ g • p /ₛ q = g / (q /ₛ p)

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p q : P
⊢ g * (p /ₛ q) = g / (q /ₛ p)
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ • p₁ /ₛ p₂ = v₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ * (p₁ /ₛ p₂) = v₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ (v₁ • p /ₛ p) / v₂ = v₁ / v₂

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p : P
⊢ v₁ * (p /ₛ p) / v₂ = v₁ / v₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ (v • p₁ /ₛ p₂) / v = p₁ /ₛ p₂

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ v * (p₁ /ₛ p₂) / v = p₁ /ₛ p₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ (v₁ • p₁ /ₛ p₂) / v₂ = v₁ / v₂ * (p₁ /ₛ p₂)

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ * (p₁ /ₛ p₂) / v₂ = v₁ / v₂ * (p₁ /ₛ p₂)
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₃ /ₛ (p₃ /ₛ p₂) • p₁ = 1

Tactic:
smul_sdiv_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * (p₃ /ₛ (p₃ /ₛ p₂) • p₁) = 1
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁴ : Group G
inst✝³ : Torsor G P
inst✝² : SMul G Q
inst✝¹ : SDiv G Q
inst✝ : Nonempty Q
f : Q → P
hf : Injective f
smul : ∀ (c : G) (x : Q), f (c • x) = c • f x
sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y
x y : Q
⊢ f ((x /ₛ y) • y) = f x

Tactic:
by simp only [sdiv, smul, sdiv_smul]

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

Goal state before:
pp: α : Type u
l : List α
h : l[0]? = l.getLast?
⊢ l.reverse.tail.Nodup ↔ l.tail.Nodup

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    · simp_all only [List.tail_reverse, List.nodup_reverse,
        List.dropLast_cons_of_ne_nil hl, List.tail_cons]
      simp only [length_cons, Nat.zero_lt_succ, getElem?_eq_getElem,
        Nat.add_one_sub_one, Nat.lt_add_one, Option.some.injEq, List.getElem_cons,
        show l.length ≠ 0 by aesop, ↓reduceDIte, getLast?_eq_getElem?] at h
      rw [h,
        show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],
        List.nodup_append_comm]
      simp [List.getLast_eq_getElem]

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

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → β
s t : Multiset α
⊢ s = t → (∀ (x : α), x ∈ t → f x = g x) → map f s = map g t

Tactic:
rintro rfl h
  induction s using Quot.inductionOn
  exact congr_arg _ (List.map_congr_left h)

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

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

Tactic:
Multiset.card_map,

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ s.card = 0 ↔ s = 0
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case empty
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0

Tactic:
exact ⟨0, map_zero _⟩

Goal state after:
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 r s (map f t) ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
by
  rw [← rel_flip, rel_map_left, ← rel_flip]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys = xs.dedup ++ ys

Tactic:
by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union]
    rw [disjoint_cons_left] at h
    by_cases hx : x ∈ xs
    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
    · rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩

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

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

Tactic:
revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intro s u h₁ h₂
  · simpa only [zero_inter] using h₁
  by_cases h : a ∈ u
  · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
  · rw [cons_inter_of_neg _ h]
    exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRec nil append_singleton [] = nil

Tactic:
grind [reverseRec]

Goal state after:
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
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
eq,

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup

Tactic:
← ndinter_eq_inter d

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅

Tactic:
singleton_inter_of_notMem h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ ∅ = ∅
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev.castSucc = (i.rev.castPred h').castSucc

Tactic:
castSucc_castPred,

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev.castSucc = i.rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).card ≤ (Multiset.map f s.val).dedup.card
Module: Mathlib.Data.Fin.Basic

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

Tactic:
· intro j ihj hij
      rw [← le_castSucc_iff] at hij
      obtain hij | hij := (le_def.1 hij).eq_or_lt
      · obtain rfl := Fin.ext hij
        exact H _
      · exact _root_.trans (ihj hij) (H j)

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
⊢ i = j

Tactic:
split_ifs at hij with hi hj hj

Goal state after:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j

case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ

Tactic:
castSucc_castPred,

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i < j.succ
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
by
  have : Nonempty γ := (h ∅ finite_empty).nonempty
  choose! c hc using h
  set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)
  set u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
  refine ⟨u, fun n ↦ ?_⟩
  convert! hc (u '' Iio n) ((finite_lt_nat _).image _)
  rw [image_eq_range]
  exact Nat.strongRecOn_eq f n

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅

Tactic:
fold_empty,

Goal state after:
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
⊢ fold op b f (image g ∅) = b
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]

Goal state after:
case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
this : x ∉ {i ∈ s | ¬p i}
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons_cons.a
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ head :: head' :: tail = ?cons_cons.l₁ ++ a :: b :: ?cons_cons.l₂

pp: case cons_cons.l₁
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

pp: case cons_cons.l₂
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

Tactic:
eq,

Goal state after:
case cons_cons.a
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ head :: (l₁ ++ a :: b :: l₂) = ?cons_cons.l₁ ++ a :: b :: ?cons_cons.l₂

case cons_cons.l₁
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

case cons_cons.l₂
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as)
        (match true with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum

Tactic:
simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
by
  rw [rotate_eq_rotate']
  induction l generalizing l'
  · simp
  · simp_all [rotate']

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
as m : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
hm : IsChain (fun x1 x2 ↦ x1 > x2) m
hmas : m ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) (a :: m)

Tactic:
cases m with

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map (op ∘ unop) l).prod

Tactic:
op_comp_unop,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = (map id l).prod