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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : ExistsAddOfLE R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n

Tactic:
by
  obtain ⟨k, rfl⟩ := hn; rw [pow_add]; exact mul_self_nonneg _

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Tactic:
by
  calc
    (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
        simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
    _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_right ?_ _
    _ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]
  cases le_total a b
  · exact mul_add_mul_le_mul_add_mul ‹_› ‹_›
  · exact mul_add_mul_le_mul_add_mul' ‹_› ‹_›

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ k ≠ 0

Tactic:
by simpa using h₀

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
⊢ IsCoinitialFor (f '' s) (f '' t)

Tactic:
simp only [IsCoinitialFor, forall_mem_image, exists_mem_image]
  rintro a ha
  obtain ⟨b, hb, hab⟩ := hst ha
  exact ⟨b, hb, hf hab⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
y : ↑(Icc a a)
⊢ ↑y = ↑⟨a, ⋯⟩

Tactic:
by simpa using y.2

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

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
· obtain ⟨x', hx', hxx'⟩ := hst.union_left hx
      obtain ⟨y', hy', hyy'⟩ := hst.union_left hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
      exact ⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

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 α
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a

Tactic:
rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

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 : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
by
  rw [← inv_le_inv_of_neg hb (inv_lt_zero'.2 ha), inv_inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ Forall₂ R l₁ l₂

Tactic:
by
    obtain ⟨h₁, h₂⟩ := h
    induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)

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

Goal state before:
pp: α : Type u
l : List α
x : α
n k : ℕ
hn : k < n
hk : k < l.length
hk' : k < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Tactic:
by
  simp_all [getElem_insertIdx_of_lt]

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

Goal state before:
pp: case mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
intro hα l1 l2 hl

Goal state after:
case mpr
α : Type u
hα : Subsingleton α
l1 l2 : List α
hl : l1.length = l2.length
⊢ l1 = l2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l₁ l₂ : List α
⊢ map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)

Tactic:
by
  simp only [reverseAux_eq, map_append, map_reverse]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = 0 ↔ a = 0

pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
· simp [zpow']

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: n d : ℤ
⊢ ↑n / ↑d = n /. d

Tactic:
rw [divInt_eq_div]

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

Goal state before:
pp: a : ℚ
⊢ a.num ≤ 0 ↔ a ≤ 0

Tactic:
by
  simp +instances [Int.le_iff_lt_or_eq, instLE, Rat.blt]

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

Goal state before:
pp: q : ℚ
⊢ q.num < ↑q.den ↔ q < 1

Tactic:
by simp [Rat.lt_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * d * c ↔ b = a * d

Tactic:
mul_left_inj' hc

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b = a * d ↔ b = a * d
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a * (c * d) = a
⊢ a = a * c

Tactic:
mul_right_eq_self₀,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : c * d = 1 ∨ a = 0
⊢ a = a * c
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
rw [mul_def, normalize_eq]

Goal state after:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣
    q₁.den * q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
rw [mul_def, normalize_eq]

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
rw [mul_def, normalize_eq]

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

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
Int.mul_assoc,

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
Int.mul_assoc,

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * ((↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den)
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
by
  let s := divInt (q.num * r.den + r.num * q.den) (q.den * r.den : ℤ)
  have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
  obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.den + r.num * q.den) hs
  rw [c_mul_num, mul_assoc, mul_comm]
  nth_rw 1 [c_mul_den]
  repeat rw [Int.mul_assoc]
  apply mul_eq_mul_left_iff.2
  rw [or_iff_not_imp_right]
  intro
  have h : _ = s := divInt_add_divInt q.num r.num (mod_cast q.den_ne_zero) (mod_cast r.den_ne_zero)
  rw [num_divInt_den, num_divInt_den] at h
  rw [h]
  rw [mul_comm]
  apply Rat.eq_iff_mul_eq_mul.mp
  rw [← divInt_eq_div]

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

Goal state before:
pp: case nil
α : Type u
⊢ map id nil = nil

Tactic:
rw [map]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')

Tactic:
cancel_factors_eq ha hb had hbd hgcd

Goal state after:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ 1 / gcd * (bd * a') = 1 / gcd * (ad * b') ↔ 1 / gcd * (bd * a') = 1 / gcd * (ad * b')
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
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ 0 = a * c - b * c

Tactic:
tsub_eq_zero_iff_le.2 (mul_le_mul_left hab c)

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
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ 0 = 0
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ i ≥ n, u i ≤ ⨆ i, u (i + n)

pp: case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
· refine fun i hi => le_sSup ⟨i - n, ?_⟩
    dsimp only
    rw [Nat.sub_add_cancel hi]

Goal state after:
case a
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ i, ⨆ (_ : i ≥ n), u i
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s

Tactic:
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s

Tactic:
by rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Tactic:
by
  simp_rw [← union_singleton, iUnion_union]

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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
rw [hi]
    obtain ⟨i₀, hi₀⟩ := htriv
    exact ⟨⟨i₀, hi₀⟩, bot_le⟩

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf x✝¹ x✝)

Tactic:
sInf_apply_eq_sInf_image

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x ↦ ↑(f x i)

Tactic:
rintro ⟨i, hx⟩
    obtain ⟨y, hy⟩ := hf i ⟨x, hx⟩
    exact ⟨y, i, congr_arg Subtype.val hy⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃₀ S)

Tactic:
sUnion_eq_iUnion

Goal state after:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ i, ↑i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddBelow x✝¹
x✝ : ι
⊢ IsGLB (eval x✝ '' x✝¹) (sInf x✝¹ x✝)

Tactic:
sInf_apply_eq_sInf_image

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddBelow x✝¹
x✝ : ι
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (sInf s)

Tactic:
sInf_eq_argmin_on hs

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
· exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inr.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 : a = b
⊢ a = b

Tactic:
exact hab

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x = y

Tactic:
by_contra! hne

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
⊢ False
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ
⊢ ↑|q| = |↑q|

Tactic:
simp [abs_eq_max_neg]

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

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
⊢ 0 < k → k ! < (k + 1)!

Tactic:
hk

Goal state after:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (k + 1)!
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
by
  rw [← mabs_div_eq_leOnePart_sq, inv_div]

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

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = n.descFactorialBinary k

Tactic:
rw [descFactorialBinary]

Goal state after:
n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑(round x) ≤ x + 1 / 2

Tactic:
by
  rw [round_eq x]
  exact Int.floor_le (x + 1 / 2)

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
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
← hz

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a ∧ a < a - b + 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den

Tactic:
exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌊a⌋ < ⌈a⌉

Tactic:
lt_ceil

Goal state after:
case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ↑⌊a⌋ < a
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l

Tactic:
refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩
  rintro ⟨l, h₁, h₂⟩
  obtain ⟨l', h₂⟩ := h₂.exists_perm_append
  exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

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

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
rw [mapₓ] at perm

Goal state after:
case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁
Module: Mathlib.Data.List.Nodup

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

Tactic:
suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases q a

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases q a

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then {a}.card else card 0) + (filter (fun a ↦ p (f a)) t).card

Tactic:
card_zero,

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) =
    (if p (f a) then {a}.card else 0) + (filter (fun a ↦ p (f a)) t).card
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
inst✝ : DecidableEq α
a : α
l₁ : List α
x✝ : a :: l₁ <:+: []
s t : List α
te : s ++ a :: l₁ ++ t = []
⊢ False

Tactic:
by simp at te

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t), t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
intro t

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : (i : α) → i ∈ cons a s has → f i
⊢ prodPiCons f has (consPiProd f has x✝) = x✝

Tactic:
by grind [prodPiCons, consPiProd]

Goal state after: