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

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ LeftInverse (uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯)) (Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯)

Tactic:
rintro ⟨_⟩; rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.2) ∈ upperBounds s

Tactic:
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ id ≤ f

Tactic:
by
  rw [Pi.le_def]
  by_contra! H
  obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min {i | f i < i} H
  exact hm' _ (hf hm) hm

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

Goal state before:
pp: α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf).symm ⟨f a, ⋯⟩ = a

Tactic:
apply (ofInjective f hf).injective
  simp

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

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
bddAbove_def,

Goal state after:
γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ (∃ x, ∀ y ∈ s, y ≤ x) ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  rw [div_lt_iff₀ (zero_lt_two' α), mul_two, lt_add_iff_pos_left]

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

Goal state before:
pp: case cons
M : Type u_2
inst✝¹ : Mul M
inst✝ : One M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : (∀ (x : M), x ∈ l → p x) → p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ε⁻¹ * (ε ^ 2 * a ^ 2 + b ^ 2) = ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
mul_add,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ε⁻¹ * (ε ^ 2 * a ^ 2) + ε⁻¹ * b ^ 2 = ε * a ^ 2 + ε⁻¹ * b ^ 2
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a (-n) = (zpow' a n)⁻¹

Tactic:
by
  simp +contextual [zpow', apply_ite]
  split_ifs with h
  · tauto
  · tauto

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod * (drop l'.length l).prod * (drop l.length l').prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)

Tactic:
induction l generalizing f with

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

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

Tactic:
rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

Goal state after:
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:
rw [mul_den]
  exact ((Nat.dvd_iff_div_mul_eq _ _).mp (Nat.gcd_dvd_right _ _)).symm

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

Goal state before:
pp: q : ℚ
⊢ (-q)⁻¹ = -q⁻¹

Tactic:
rw [← num_divInt_den q]

Goal state after:
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
n e1 t1 k l : α
e2 : ℕ
h1 : n * e1 = t1
h2 : l * n ^ e2 = k
⊢ k * e1 ^ e2 = l * t1 ^ e2

Tactic:
by
  rw [← h2, ← h1, mul_pow, mul_assoc]

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

Goal state before:
pp: case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * 0 = a * b - a * c

Tactic:
mul_zero,

Goal state after:
case inl
R : Type u
inst✝⁵ : NonUnitalNonAssocSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a b c : R
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ 0 = a * b - a * c
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
⊢ sSup s = ⊤

Tactic:
by_cases hmem : ⊤ ∈ s
  · exact sSup_of_top_mem hmem
  · exact if_neg hmem |>.trans <| if_neg h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

Tactic:
rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case neg
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : ¬i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
· simp [h hij |>.eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
⊢ x ≤ sSup t

Tactic:
rcases hs x hx with ⟨y, yt, hxy⟩

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
y : α
yt : y ∈ t
hxy : x ≤ y
⊢ x ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
refine coe_le_coe.2 (csInf_le ?_ ha)

Goal state after:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)
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))

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

Tactic:
· exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))

Goal state after:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ Ici x = {x} ↔ IsTop x

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
  by_contra! H
  have : y ∈ Ici x := H.le
  rw [h, mem_singleton_iff] at this
  exact lt_irrefl y (this.le.trans_lt H)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h' : s = ∅
x : α
h : ∀ ⦃t : Set α⦄, IsChain r t → ∅ = t
⊢ False

Tactic:
exact singleton_ne_empty x (h IsChain.singleton).symm

Goal state after:
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 : ι
⊢ f x = g x

Tactic:
by
    if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ mulSingle i a i ≠ 1

Tactic:
mulSingle_eq_same

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ a ≠ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)

Tactic:
by
    rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by lia) (Nat.pow_pos <| by lia)

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑⟨q, h⟩ = ↑q

Tactic:
simp only [NNRat.cast_def, NNRat.num_mk, Nat.cast_natAbs, NNRat.den_mk, Rat.cast_def]

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑|q.num| / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : 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⌉) = (⌊2 * (↑⌊x⌋ + fract x)⌋ + 1) / 2

Tactic:
mul_add,

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⌉) = (⌊2 * ↑⌊x⌋ + 2 * fract x⌋ + 1) / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
⊢ 1 + n.natPred = ↑n

Tactic:
rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]

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

Goal state before:
pp: m k : ℕ+
h₀ : 0 + ↑k * 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False

Tactic:
mul_zero,

Goal state after:
m k : ℕ+
h₀ : 0 + 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * (↑c + ↑1) - fract (a * (↑c + ↑1)) = ↑z

Tactic:
mul_add,

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a * ↑1 - fract (a * (↑c + ↑1)) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a * ↑1 - fract (a * (↑c + ↑1)) = ↑z

Tactic:
mul_add,

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a * ↑1 - fract (a * ↑c + a * ↑1) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑n * (↑(m % n) / ↑n + ↑(↑m / ↑n))

Tactic:
mul_add,

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m = ↑n * (↑(m % n) / ↑n) + ↑n * ↑(↑m / ↑n)
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
a : R
z : ℤ
⊢ ⌈a + ↑z⌉ = ⌈a⌉ + z

Tactic:
by
  rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]

Goal state after:
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 b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * (↑⌊a⌋ + 1) ≤ ↑⌊a⌋

Tactic:
rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

Goal state after:
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
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |↑m.pred.succ * δ - q| ≤ δ

Tactic:
Nat.cast_succ,

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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |(↑m.pred + 1) * δ - q| ≤ δ
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case pos
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
· simpa [hx, and_comm, and_or_left] using h

Goal state after:
case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
rw [Multiset.add_comm, singleton_add]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
show l.Nodup = (l.dropLast ++ [l.getLast hl]).Nodup by
          simp [List.dropLast_eq_take],

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ (l.dropLast ++ [l.getLast hl]).Nodup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = a :: l₁ ∪ l₂.dedup

Tactic:
simp only [cons_union] at *

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: l₁ ++ l₂).dedup = List.insert a (l₁ ∪ l₂.dedup)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
dedup_cons_of_mem' h,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ l₂.erase head✝ <+ l₂

Tactic:
by grind [erase_sublist]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ (s + t).dedup = t.dedup

Tactic:
by
  induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
by
  rw [← coe_eq_singleton]; exact Set.eq_singleton_or_nontrivial ha

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
    simp only [mem_inter, mem_insert, or_and_left, this]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
rw [← subset_insert_iff, insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ = ∅ ↔ IsEmpty α

Tactic:
by
  contrapose!; exact univ_nonempty_iff

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

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

Tactic:
Subtype.restrict_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (f ∘ fun a ↦ ↑a) univ.val = Multiset.map (f ∘ Subtype.val) univ.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
inst✝ : DecidableEq γ
g : β → γ
⊢ (image g (image f s)).val = (image (g ∘ f) s).val

Tactic:
simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

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

Goal state before:
pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
← h j hj (hj.trans hi),

Goal state after:
case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ ↑(e ⟨j, ⋯⟩) < ↑(e ⟨i, hi⟩)
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rw [← val_castSucc]

Goal state after:
n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩).castSucc = ↑i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

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

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

Tactic:
| cons_duplicate h =>

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:
| cons_cons y h IH =>

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

Goal state before:
pp: α : 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]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f (a + 1) - (f 0 + 1) ≤ f (b + 1) - (f 0 + 1) ↔ a ≤ b

Tactic:
Nat.sub_le_sub_iff_right,

Goal state after:
α : 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]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f (a + 1) ≤ f (b + 1) ↔ a ≤ b

α : 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]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f 0 + 1 ≤ f (b + 1)
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]?
⊢ ∀ (ix : ℕ), l₁✝[ix]? = (a✝¹ :: l₂✝)[(RelEmbedding.trans f (OrderEmbedding.ofStrictMono (fun x ↦ x + 1) ⋯)) ix]?

Tactic:
simpa using hf

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

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

Tactic:
by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

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

Goal state before:
pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj

Goal state after:
case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi✝ : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj✝ : n✝ + 1 < (replicate 2 x).length
hi : n✝¹ = 0
hj : n✝ = 0
⊢ ⟨n✝¹ + 1, hi✝⟩ < ⟨n✝ + 1, hj✝⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi✝⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj✝⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j)

Tactic:
by
  simp [Pi.le_def, forall_iff_succAbove i]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s

Tactic:
fold_cons'_right,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op (op b a) s = fold op (op a b) s