mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ

Tactic:
← sup_div_inf_eq_mabs_div,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) ^ 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: m x : ℤ
h1 : m ∣ x
h2 : |x| < m
⊢ x = 0

Tactic:
by
  by_contra h
  have := Int.natAbs_le_of_dvd_ne_zero h1 h
  rw [Int.abs_eq_natAbs] at h2
  lia

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y r r' : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (r, s, t) → x.P y (r', s', t') → x.P y (r.xgcdAux s t r' s' t')

Tactic:
induction r, r' using gcd.induction with

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a : WithBot α
⊢ a < 0 ↔ a = ⊥

Tactic:
by
  induction a <;> simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
⊢ - -a = a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤
    · simp
    · apply left_neg_eq_right_neg (a := -a) <;> simp [add_comm, add_neg_cancel_of_ne_top, ha]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x ↦ x - b

Tactic:
simpa [sub_eq_add_neg] using add_left_injective_of_ne_top (-b) (by simpa)

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

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ f x = 0 ↔ x = 0

Tactic:
refine ⟨?_, by simp +contextual⟩

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ f x = 0 → x = 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n

Tactic:
rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌊a⌋₊

pp: case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - ↑⌊a⌋₊ ≤ 1

Tactic:
· simpa using (floor_le ha).trans (le_add_of_nonneg_right zero_le_one)

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - ↑⌊a⌋₊ ≤ 1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
a b : α
⊢ |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b

Tactic:
rw [abs_mul_abs_self]
  simp only [mul_add, add_comm, add_left_comm, mul_comm, sub_eq_add_neg, mul_one, mul_neg,
    neg_add_rev, neg_neg, add_assoc]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
by simp [upperBounds, hf.le_iff_le]

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x✝ : ↑(s ∪ t)
x : α
h' : x ∈ s ∪ t
⊢ (fun o ↦
        match o with
        | Sum.inl x => ⟨↑x, ⋯⟩
        | Sum.inr x => ⟨↑x, ⋯⟩)
      ((fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩) ⟨x, h'⟩) =
    ⟨x, h'⟩

Tactic:
by by_cases h : p x <;> simp [h]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inl
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : b < a
⊢ f a = g a

Tactic:
rw [← IH b h] at hb
    cases (hf.injective hb).not_lt h

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.12
a : α
x✝ : ↑{a}
x : α
h : x ∈ {a}
⊢ (fun x ↦ ⟨a, ⋯⟩) ((fun x ↦ PUnit.unit) ⟨x, h⟩) = ⟨x, h⟩

Tactic:
subst x

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.12
a : α
x✝ : ↑{a}
⊢ (fun x ↦ ⟨a, ⋯⟩) ((fun x ↦ PUnit.unit) ⟨a, ⋯⟩) = ⟨a, ⋯⟩
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzt : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

Tactic:
exact ⟨z, hzt, hxz⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
· obtain rfl | ht := t.eq_empty_or_nonempty
    · aesop
    · exact .inr ⟨h, ht⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ a
n : ℕ
h : n = 0
⊢ a / ↑n ≤ a

Tactic:
by simpa [h]

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

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
· simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
have : q b := by rwa [← hpq h₁]

Goal state after:
case pos
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
this : q b = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
| fun x1 x2 ↦ x1 ~ map f x2

Tactic:
rw [← Relation.comp_eq_fun (map f)]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
| Perm ∘r fun x1 x2 ↦ x1 = map f x2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l).flatten.getLast? = l.getLast?

Tactic:
by
  rw [← List.head?_reverse, ← List.head?_reverse, List.reverse_flatten, List.map_replicate,
  List.reverse_replicate, head?_flatten_replicate h]

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

Goal state before:
pp: α : Type u
l : List α
p : α → Prop
⊢ (∃ x, x ∈ l ∧ p x) ↔ ∃ i x, p l[i]

Tactic:
by
  simp only [mem_iff_getElem]
  exact ⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ (fun x ↦
        match x with
        | (r, x) => zpow' x r)
      (r, x) ≠
    0

Tactic:
simp [zpow'_eq_zero_iff, hx]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b

Tactic:
by
  obtain ⟨a, ha⟩ := a
  simp [toNonneg, ha.not_gt]

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

Goal state before:
pp: case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂

Tactic:
· rintro ⟨rfl, rfl, rfl⟩
    rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: num den n : ℕ
⊢ (↑num /. ↑den) ^ n = ↑num ^ n /. ↑(den ^ n)

Tactic:
divInt_pow,

Goal state after:
num den n : ℕ
⊢ ↑num ^ n /. ↑den ^ n = ↑num ^ n /. ↑(den ^ n)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
rcases le_total 0 q with hq | hq

Goal state after:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat ((n₁ + n₂) * ↑d) (d * d) = mkRat (n₁ + n₂) d

Tactic:
mkRat_mul_right h

Goal state after:
n₁ n₂ : ℤ
d : ℕ
h : d ≠ 0
⊢ mkRat (n₁ + n₂) d = mkRat (n₁ + n₂) d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
simp only [Int.ediv_self hn, Int.cast_one, div_self this]

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1

Tactic:
by
  simp [*]

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

Goal state before:
pp: q : ℚ
hq : q ≠ 0
⊢ q⁻¹.den = q.num.natAbs

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Linarith.Lemmas

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0

Tactic:
by
  simp [*]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

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

Tactic:
by
  simp [*]

Goal state after:
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:
rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ x ∈ {a, b}, s x = s a ∩ s b

Tactic:
biInter_insert,

Goal state after:
α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ s a ∩ ⋂ x ∈ {b}, s x = s a ∩ s b
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
t : ι → Set β
⊢ ⨆ a ∈ ⋃ i, t i, a = ⨆ i, ⨆ a ∈ t i, a

Tactic:
iSup_iUnion

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

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

Tactic:
rcases eq_empty_or_nonempty t with rfl | t_ne

Goal state after:
case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
⊢ sSup s = sSup ∅

case inr.inr
α : 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
⊢ sSup s = sSup t
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
c : WithTop β
⊢ c ∈ s → c ∈ {⊤}

Tactic:
hc

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
c : WithTop β
hc : c ∈ s
⊢ c ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
hc

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
constructor <;> refine le_of_not_gt fun h' => ?_

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ x = y

Tactic:
by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
⊢ x ∈ {x | Maximal (fun x ↦ x ∈ s) x}

Tactic:
obtain ⟨y, hyx, hy⟩ := hs x hx

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun x ↦ x ∈ s) y
⊢ x ∈ {x | Maximal (fun x ↦ x ∈ s) x}
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a + 0 ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ 0 ≤ c

Tactic:
hc

Goal state after:
α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
c : α
h : ↑a + 0 ≤ ↑a + c
hc : ↑b = ↑a + c
⊢ 0 ≤ c
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p < ↑q

Tactic:
rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
    Nat.cast_lt (α := K), ← NNRat.lt_def]
  · simp
  · simp

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) * (n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial (k + 1)

Tactic:
descFactorial,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1 - k) * (n + 1).descFactorial k) = (n + 1) * n.descFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k.succ = 0 ↔ n < k.succ

Tactic:
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]

Goal state after:
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
· rw [descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)]
    by_cases hkn : k ≤ n
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n - k < m - k by lia), Nat.zero_mul]
    · rw [descFactorial_eq_zero_iff_lt.mpr (show n < k by lia), Nat.mul_zero]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ ⌊x⌋ ≤ z - 1

Tactic:
rwa [le_sub_one_iff, floor_lt]

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
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
rw [le_floor, Int.cast_add]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ a + b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 1 ≤ ⌈a⌉ ↔ 0 < a

Tactic:
simpa using le_ceil_iff (z := 1)

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
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₃) / (p₂ /ₛ p₃) = p₁ /ₛ p₂

Tactic:
← sdiv_smul_eq_sdiv_div,

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
by_cases! h : 0 ≤ a
  · exact ceil_lt_add_one h
  · rw [ceil_eq_zero.mpr h.le, cast_zero]
    exact neg_lt_iff_pos_add.mp ha

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g = h

Tactic:
← inv_mul_eq_one (G := α)

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g⁻¹ * h = 1
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case pos
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
simp [ha, count_eq_zero_of_not_mem]

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

Goal state before:
pp: case neg
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : ¬a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
simp [ha, count_eq_zero_of_not_mem]

Goal state after:
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₁ /ₛ p₃) / (p₂ /ₛ p₄)

Tactic:
← sdiv_smul_eq_sdiv_div,

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₁ /ₛ p₃) / (p₂ /ₛ p₄)
Module: Mathlib.Data.Set.List

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
a : β
l : List β
ihl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: l ∈ range (map f)

Tactic:
| cons a l ihl =>

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

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
⊢ (l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup

Tactic:
by
  simp only [nodup_append', not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
    disjoint_cons_right]

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

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
⊢ m.card = card 0 → Rel r m 0

Tactic:
hc

Goal state after:
case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ Rel r m 0
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
⊢ m.card = (a ::ₘ t).card → Rel r m (a ::ₘ t)

Tactic:
hc

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 = (a ::ₘ t).card
⊢ Rel r m (a ::ₘ t)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ Rel r (a ::ₘ s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
by
      simp only [ih, cons_add, rel_cons_left]
      constructor
      · intro h
        rcases h with ⟨b, bs', hab, h, rfl⟩
        rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
        exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
      · intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩

Goal state after:
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)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map f s = pmap (fun x x_1 ↦ f x) s ⋯

Tactic:
rw [pmap_eq_map]

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : α
tail✝ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝ → tail✝ = l₁ ++ drop l₁.length tail✝
l₁ : List α
h : l₁ <+: head✝ :: tail✝
⊢ head✝ :: tail✝ = l₁ ++ drop l₁.length (head✝ :: tail✝)

Tactic:
cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

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

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n < (a :: l).tails.length
⊢ (a :: l).tails[n] = drop n (a :: l)

Tactic:
| cons a l ihl =>

Goal state after: