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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : 0 < a
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Icc a b)

Tactic:
convert! sub_inv_antitoneOn_Icc_right ha
  exact (sub_zero _).symm

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a - a / 2 < b - b / 2

Tactic:
sub_self_div_two,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a / 2 < b - b / 2
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a / 2 < b - b / 2

Tactic:
sub_self_div_two,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a / 2 < b / 2
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rw [perm_comm, this (Nat.le_of_not_ge hle), perm_comm]

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

Goal state before:
pp: case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

pp: case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂

Tactic:
· rintro rfl
    exact ⟨rfl, fun _ _ _ ↦ rfl⟩

Goal state after:
case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ some l[idxOf a l] = some a

Tactic:
getElem_idxOf

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ some a = some a
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
rw [sum_cons, length, add_comm]

Goal state after:
case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + L.length ≤ j + L.sum
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z

Tactic:
isRelPrime_mul_unit_right_right hu

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y z ↔ IsRelPrime y z
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (normalize (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) (q₁.den * q₂.den) ⋯).den ∣ q₁.den.lcm q₂.den

Tactic:
normalize_eq,

Goal state after:
q₁ q₂ : ℚ
⊢ {
        num :=
          (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) / ↑((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯,
        reduced := ⋯ }.den ∣
    q₁.den.lcm q₂.den
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Tactic:
rw [mul_le_mul_iff_right₀, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd,
    mul_le_mul_iff_right₀]

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c

Tactic:
by
  subst_vars; simp [add_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = ⨆ b, bif b then x else y

Tactic:
iSup_bool_eq,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = (bif true then x else y) ⊔ bif false then x else y
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ ⨆ a ∈ s, f a = sSup (⇑f.symm ⁻¹' s)

Tactic:
← sSup_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ sSup (⇑f '' s) = sSup (⇑f.symm ⁻¹' s)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b)

Tactic:
← sSup_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g '' f '' t) = ⨆ b ∈ t, g (f b)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g '' f '' t) = ⨆ b ∈ t, g (f b)

Tactic:
← sSup_image,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ sSup (g '' f '' t) = sSup ((fun b ↦ g (f b)) '' t)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ⋃ (_ : s.Nonempty), s = s

Tactic:
by
  rw [iUnion_nonempty_index, biUnion_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
by
  simp_rw [iSup_prod, mem_prod, iSup_and]
  exact iSup_congr fun _ => iSup_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

Tactic:
simp only [sdiff_subset_iff, ← biUnion_union]

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ ⋃ x ∈ s₁, t x ⊆ ⋃ x ∈ s₂ ∪ s₁ \ s₂, t x
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ ⨆ b_1 ∈ {b, c}, a ⊓ b_1 ≤ sSup {a ⊓ b, a ⊓ c}

Tactic:
← sSup_image,

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ sSup (min a '' {b, c}) ≤ sSup {a ⊓ b, a ⊓ c}
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ f (a ⊓ sSup s) ≤ f (⨆ b ∈ s, a ⊓ b)

Tactic:
← sSup_image,

Goal state after:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ f (a ⊓ sSup s) ≤ f (sSup (min a '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : 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
⊢ sSup s = sSup t

pp: case neg
α : 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)
⊢ sSup s = sSup t

Tactic:
· have Bs : BddAbove s := by
      rcases B with hB | ⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)
    have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩ | hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB
    apply le_antisymm
    · apply csSup_le s_ne (fun x hx ↦ ?_)
      rcases hs x hx with ⟨y, yt, hxy⟩
      exact hxy.trans (le_csSup Bt yt)
    · apply csSup_le t_ne (fun y hy ↦ ?_)
      rcases ht y hy with ⟨x, xs, hyx⟩
      exact hyx.trans (le_csSup Bs xs)

Goal state after:
case neg
α : 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)
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
· rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)
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
⊢ a < b

Tactic:
grind [Set.nonempty_Ico]

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

Goal state before:
pp: case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a

Tactic:
· exact (WithTop.isLUB_sSup' h).2 ha

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Icc x y = Icc (e x) (e y)

Tactic:
← e.preimage_Icc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' ⇑e ⁻¹' Icc (e x) (e y) = Icc (e x) (e y)
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
c c₁ c₂ s✝ t : Set α
a b x y : α
inst✝¹ : PartialOrder α
inst✝ : DecidableLE α
s : Set α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ (a b : ↑s), a ≤ b ∨ b ≤ a

Tactic:
by
    rintro ⟨a, ha⟩ ⟨b, hb⟩
    exact hs.total ha hb

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

Tactic:
exact h.eq ha hb hab

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ a / ↑b' = ↑q

Tactic:
simp only [Nat.blt_eq] at h₂

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ a / ↑b' = ↑q
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ⊔ (a ⊔ (a⁻¹ ⊔ 1)) = |a|ₘ

Tactic:
← @sup_assoc _ _ a,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ⊔ (a ⊔ a⁻¹ ⊔ 1) = |a|ₘ
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
clear! ra rb

Goal state after:
$u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» «$nb» : ℕ
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»
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
    exact not_succ_le_zero k h

Goal state after:
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₁ = (x₂ -ᵥ y) +ᵥ x₂
⊢ x₁ = x₂

Tactic:
vadd_eq_vadd_iff_sub_eq_vsub,

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₁ -ᵥ y) = x₁ -ᵥ x₂
⊢ x₁ = x₂
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ {x | x ∈ l}

Tactic:
mem_ofPred_eq,

Goal state after:
α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ x ∈ l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)

Tactic:
by
  rw [← singleton_add, ← singleton_add, Multiset.add_assoc]

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = (a ::ₘ t).card
⊢ Rel r m (a ::ₘ t)

Tactic:
card_cons

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
⊢ Rel r m (a ::ₘ t)
Module: Mathlib.Data.Multiset.MapFold

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

Tactic:
by
  induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
  rcases eq_or_ne y x with rfl | hxy
  · simp
  replace h : x ∈ s := by simpa [hxy.symm] using h
  rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
    have := count_pos_iff.2 ha
    have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
    rw [h, count_cons_self] at this
    lia

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
have h₂ : x ∉ t₂ := h h₁

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ IsWellFounded (Multiset β) fun x1 x2 ↦ x1 ⊂ x2

Tactic:
exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.val.toList.Nodup

Tactic:
← Multiset.coe_nodup,

Goal state after:
α : Type u_1
s : Finset α
⊢ (↑s.val.toList).Nodup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
s : Multiset α
inst✝ : DecidableEq β
b : β
⊢ count b (map f s) = (filter (fun a ↦ b = f a) s).card

Tactic:
simp [count, countP_map]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
by
  suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl
  · rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
    · simp
    · simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
htq : x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s
w✝ : α
hx : w✝ ∈ x✝
⊢ False

Tactic:
exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nontrivial
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := hs

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
rw [Finset.mem_union, Xor]
  have := disjoint_left.1 h
  tauto

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

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

Tactic:
← rev_lt_rev,

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev < i.rev.rev ↔ j.rev < i
Module: Mathlib.Data.Fin.Rev

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

Tactic:
← rev_lt_rev,

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev.rev < i.rev ↔ j < i.rev
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
by_cases h0 : 0 ≠ i ∧ 0 ≠ j

Goal state after:
case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : 0 ≠ i ∧ 0 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi < j ↔ i < j.succ

Tactic:
← succ_lt_succ_iff,

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ (i.pred hi).succ < j.succ ↔ i < j.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j < i.pred hi ↔ j.succ < i

Tactic:
← succ_lt_succ_iff,

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j.succ < (i.pred hi).succ ↔ j.succ < i
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)
j : Fin n
⊢ ((fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)) → (fun x1 x2 ↦ x1 < x2) i j.succ → r (f i) (f j.succ)

Tactic:
ihj

Goal state after:
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)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
⊢ (fun x1 x2 ↦ x1 < x2) i j.succ → r (f i) (f j.succ)
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * (↑i + 1)

Tactic:
Nat.mul_add,

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * ↑i + m * 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

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
· rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩

Goal state after:
case mp
α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d