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

Goal state before:
pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b

Tactic:
exfalso

Goal state after:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
exfalso

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
exfalso

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Symm r
a b : α
⊢ Pairwise (r on fun c ↦ bif c then a else b) ↔ r a b

Tactic:
by
  simpa [Pairwise, Function.onFun] using symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (min a b)) (f (max a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : MonotoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f (Icc (min a b) (max a b)) (Icc (f (max a b)) (f (min a b)))

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]

case hx
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ a ∈ [[a, b]]

case hy
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ b ∈ [[a, b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
mem_uIoc

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f a * f b ≤ f a * f c

Tactic:
← mul,

Goal state after:
α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f (a * b) ≤ f a * f c
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f (a * b) ≤ f a * f c

Tactic:
← mul,

Goal state after:
α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f (a * b) ≤ f (a * c)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
Nat.mul_left_comm j !,

Goal state after:
case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1) * (n * (j ! * n ^ j))
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
h : k.succ ≤ 0
⊢ (0 - k.succ)! * descFactorial 0 k.succ = 0!

Tactic:
exfalso

Goal state after:
k : ℕ
h : k.succ ≤ 0
⊢ False
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
abs_sub_le_iff,

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f x - f y ≤ f (x / y) ∧ f y - f x ≤ f (x / y)
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by rwa [NNRatCast.ofScientific_eq_ite, if_pos rfl]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = (⌊2 * x⌋ + 1) / 2

Tactic:
rw [← floor_add_fract x, round, fract_intCast_add, fract_fract, floor_intCast_add, mul_add,
    ← Int.cast_ofNat, ← Int.cast_mul, floor_intCast_add, ceil_intCast_add, add_assoc,
    Int.mul_add_ediv_left _ _ two_ne_zero, Int.cast_ofNat]

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid G
inst✝³ : LinearOrder G
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
f : G →* M
hf : StrictMono ⇑f
x x✝ : G
h : 1 < x✝
⊢ ∃ n, x ≤ x✝ ^ n

Tactic:
refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_

Goal state after:
G : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid G
inst✝³ : LinearOrder G
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
f : G →* M
hf : StrictMono ⇑f
x x✝ : G
h : 1 < x✝
⊢ ∀ (a : ℕ), f x ≤ f x✝ ^ a → x ≤ x✝ ^ a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False

Tactic:
rw [hn0, pow_zero] at hn

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
obtain rfl | ha := ha.eq_or_lt
  · simp
  have : 0 < a - 1 := by linarith
  refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
  rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
    ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]
  convert ceil_lt_add_one (R := k) _
  field

Goal state after:
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g • ↑m * g⁻¹ • ↑m⁻¹ = 1

Tactic:
smul_mul_smul_comm,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g * g⁻¹) • (↑m * ↑m⁻¹) = 1
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ g⁻¹ • ↑m⁻¹ * g • ↑m = 1

Tactic:
smul_mul_smul_comm,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g⁻¹ * g) • (↑m⁻¹ * ↑m) = 1
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
⊢ (fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f) = f

Tactic:
ext x; simp [map_fract]

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ (pointReflection x) y = y ↔ y = x

Tactic:
pointReflection_apply,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ (x -ᵥ y) +ᵥ x = y ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : (pointReflection x₁) y = (pointReflection x₂) y
⊢ x₁ = x₂

Tactic:
pointReflection_apply,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂) y
⊢ x₁ = x₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : (x₁ -ᵥ y) +ᵥ x₁ = (pointReflection x₂) y
⊢ x₁ = x₂

Tactic:
pointReflection_apply,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : (x₁ -ᵥ y) +ᵥ x₁ = (x₂ -ᵥ y) +ᵥ x₂
⊢ x₁ = x₂
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
subst h
      simp_all

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩

Goal state after:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
replicate_succ

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)

Tactic:
| @cons a b s t hab _hst ih =>

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
erase_of_notMem h,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ s.card = if a ∈ s then s.card.pred else s.card
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha : a ∈ x ::ₘ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
rcases mem_cons.1 ha with ha | ha

Goal state after:
case cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s - t ↔ count a t < count a s

Tactic:
← count_pos,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ 0 < count a (s - t) ↔ count a t < count a s
Module: Mathlib.Data.Multiset.MapFold

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

Tactic:
rcases eq_or_ne y x with rfl | hxy

Goal state after:
case cons.inl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
y : α
s : Multiset α
ih : y ∈ s → map f (s.erase y) = (map f s).erase (f y)
h : y ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)

case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
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
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(l₁.diff l₂) = foldl erase ↑l₁ ↑l₂

Tactic:
rw [diff_eq_foldl l₁ l₂]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) = foldl erase ↑l₁ ↑l₂
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
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 : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ (map (fun x ↦ i ↑x ⋯) s.attach).Nodup

Tactic:
· exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hno : s.Nodup
⊢ s ≤ t.dedup ↔ s ≤ t

Tactic:
simp [le_dedup, hno]

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst ↦ strongDownwardInduction H t₂ ht

Tactic:
rw [strongDownwardInduction]

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ strongDownwardInduction H s a) = H s fun {t} ht _h ↦ strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s.erase a - t + t ∩ s = s

Tactic:
erase_of_notMem h,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - t + t ∩ s = s
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset

Tactic:
toList_toFinset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset = s.toFinset
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
x✝ : α
⊢ ¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
rw [Classical.not_imp, not_not]

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

Goal state before:
pp: α : Type u_2
s₁ s₂ t : Finset α
h₁ : Disjoint s₁ t
h₂ : Disjoint s₂ t
⊢ s₁.disjUnion t h₁ = s₂.disjUnion t h₂ ↔ s₁ = s₂

Tactic:
simp [← val_inj, Multiset.add_left_inj]

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

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

pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1

Tactic:
· exact subsingleton_one.elim _ 1

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
iff_true_right H,

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p
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
⊢ cons x p i.succ = p i

Tactic:
simp [cons]

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

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

Tactic:
simp [cons]

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

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

Tactic:
simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

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

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

Tactic:
simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]

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

Goal state before:
pp: α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ s.strongInductionOn H = H s fun t x ↦ t.strongInductionOn H

Tactic:
by
  dsimp only [strongInductionOn]
  rw [strongInduction]

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

Goal state before:
pp: case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ y :: l₁✝
⊢ x ∈+ y :: l₂✝

Tactic:
rw [duplicate_cons_iff] at hx ⊢
    rcases hx with (⟨rfl, hx⟩ | hx)
    · simp [h.subset hx]
    · simp [IH hx]

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

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

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a ↦ strongDownwardInduction H s a) = H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

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

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
⊢ hd :: tl <+ l'

Tactic:
have : some hd = l'[f 0]? := by simpa using hf 0

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
this : some hd = l'[f 0]?
⊢ hd :: tl <+ l'
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
refine ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), ?_⟩

Goal state after:
case mp.cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x ↦ x + 1) ⋯)) ix]?
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ insertionSort r l ~ l

Tactic:
induction l <;> grind [List.Perm, perm_orderedInsert]

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

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

Tactic:
apply h b <| (mem_insertionSort r).1 _

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ insertionSort r l
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
obtain ⟨d, hc, hd⟩ := hc

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ l
⊢ c <+ insertionSort r l