mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝ : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
by_cases n = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ IsAddLeftRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ IsAddRightRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ c + b = a ↔ a = c + b

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a = c + b ↔ a = c + b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
refine ⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
  rintro rfl
  rw [tsub_zero] at h
  exact h.false

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = max a b

Tactic:
add_comm,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = max a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithBot α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
by
  induction a
  · exact (bot_add _).symm
  · induction b
    · exact (add_bot _).symm
    · rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ z, z ≠ 0 ∧ z < x ∧ z < y

Tactic:
obtain ⟨z', hnz', hzx, hzy⟩ := exists_ne_zero_and_le_and_le hx hy
  obtain ⟨z, hnz, hlt⟩ := exists_ne_zero_and_lt hnz'
  use z, hnz
  constructor <;> exact lt_of_lt_of_le hlt ‹z' ≤ _›

Goal state after:
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 : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + ↑1

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑(n + 1)
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 : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑n + ↑1

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ n ≤ ⌊a⌋₊ ∧ a < ↑(n + 1)
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ DirectedOn (r on f) s ↔ DirectedOn r (f '' s)

Tactic:
refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩
  obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y)
    (Set.mem_image_of_mem f hy)
  grind

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
m : α
inst✝ : Invertible m
n : ℕ
⊢ ⅟m ^ n * m ^ n = 1

Tactic:
rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ a / c + b = (a + b * c) / c

Tactic:
add_comm,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ b + a / c = (a + b * c) / c
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤ
h : u = 1 ∨ u = -1
⊢ IsUnit u

Tactic:
rcases h with (rfl | rfl)

Goal state after:
case inl
⊢ IsUnit 1

case inr
⊢ IsUnit (-1)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

Tactic:
obtain ha | ha := le_total 0 a

Goal state after:
case inl
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : 0 ≤ a
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b

case inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
⊢ (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a + (b + d) < c + (a + b)

Tactic:
← hbd,

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a + 0 < c + (a + b)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
exact hn.pow_nonneg _

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
rw [lt_iff_le_not_ge, AntisymmRel]
  tauto

Goal state after:
Module: Mathlib.Order.WellFounded

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

Tactic:
obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a

Goal state after:
case inr.inr
β : 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 : a < b
c : β
hc : f c = g a
⊢ f a = g a
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
rintro ⟨a, ha⟩

Goal state after:
β : Type u_2
inst✝² : LinearOrder β
f : β → β
inst✝¹ : WellFoundedLT β
inst✝ : NoMaxOrder β
hf : StrictMono f
a : β
ha : a ∈ upperBounds (Set.range f)
⊢ False
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ IsCofinalFor t s ∨ IsCofinalFor s t

Tactic:
by
  rw [or_iff_not_imp_left]
  intro hts x hx
  simp only [IsCofinalFor, not_forall, not_exists, not_and] at hts
  obtain ⟨y, hy, hys⟩ := hts
  obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)
  · cases hys z hzs hyz
  · exact ⟨z, hzt, hxz⟩

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:
| cons a l ih =>

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

Goal state before:
pp: case cons
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
| cons a l ih =>

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

Goal state before:
pp: case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
⊢ a ≤ b

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun x hbx => ?_

Goal state after:
case inr
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ a ≤ x
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: x y : ℕ
⊢ x.ble y = false ↔ ¬x ≤ y

Tactic:
← Bool.not_eq_true,

Goal state after:
x y : ℕ
⊢ ¬x.ble y = true ↔ ¬x ≤ y
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
| cons a l ih =>

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 : α
a2 : 2 ≤ a
⊢ 2⁻¹ + 1 / a ≤ 1

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a + 2⁻¹ ≤ 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Set.Ico 0 b, c < a * b'

Tactic:
simp_rw [mul_comm a] at h ⊢

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
hb : 0 < b
h : c < b * a
⊢ ∃ b' ∈ Set.Ico 0 b, c < b' * a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
d : α
hd✝¹ : a * b < d
a' : α
ha' : a' > a
hd✝ : a' * b < d
b' : α
hb' : b' > b
hd : a' * b' < d
⊢ c ≤ d

Tactic:
exact (h a' ha' b' hb').trans hd.le

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

Goal state before:
pp: case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
· exact SublistForall₂.cons_right (ih _ _ h1 btc)

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

Goal state before:
pp: case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False

Tactic:
rw [h.length_eq] at hn₁

Goal state after:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : (l₂.insertIdx n a).length < n
hn₂ : l₂.length ≥ n
h : l₁ ~ l₂.insertIdx n a
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h

Goal state after:
case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

case inr
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.headI + L.tail.sum - L.headI

Tactic:
add_comm,

Goal state after:
L : List ℕ
⊢ L.tail.sum = L.tail.sum + L.headI - L.headI
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.sum % n = (map (fun x ↦ x % n) l).sum % n
⊢ (a :: l).sum % n = (map (fun x ↦ x % n) (a :: l)).sum % n

Tactic:
| cons a l ih =>

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun a ↦ (f a).toList) (a :: l)

Tactic:
| cons a l ih =>

Goal state after:
case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ filterMap f (a :: l) = flatMap (fun a ↦ (f a).toList) (a :: l)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.prod % n = (map (fun x ↦ x % n) l).prod % n
⊢ (a :: l).prod % n = (map (fun x ↦ x % n) (a :: l)).prod % n

Tactic:
| cons a l ih =>

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)

Tactic:
| cons a l ih =>

Goal state after:
case cons
α : Type u
β : Type v
f : α → Option β
g : α → β
a : α
l : List α
ih : filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)
⊢ filterMap f (a :: l) = map g (a :: l) → ∀ (x : α), x ∈ a :: l → f x = some (g x)
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 1 /. 1 = 1

Tactic:
divInt_one,

Goal state after:
⊢ ↑1 = 1
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: r : ℚ
⊢ ↑r.num / ↑r.den = r

Tactic:
rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]

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

Goal state before:
pp: a : ℤ
b : ℕ
hb : b ≠ 0
⊢ mkRat a b < 0 ↔ a < 0

Tactic:
by
  grind [mkRat_nonneg_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a x y : G
⊢ x * a = a * y ↔ a * y = x * a

Tactic:
eq_comm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ y * a = a * x ↔ a * x = y * a

Tactic:
eq_comm

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

Goal state before:
pp: case refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d

Tactic:
· rwa [num_divInt_den]

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

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n + q).den = q.den

Tactic:
add_comm,

Goal state after:
n : ℤ
q : ℚ
⊢ (q + ↑n).den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n + q).den = q.den

Tactic:
by
  rw [add_comm, add_intCast_den]

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

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ {f 0} ∪ range (f ∘ succ) = range f

Tactic:
rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x

Tactic:
iSup_range

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = u 0 ⊔ ⨆ i, u i.succ
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
iSup_split_single _ i

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
iSup_split_single _ i

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ ⨆ a_1 ∈ range fun i ↦ f i, a_1 ⊓ a = ⨆ i, f i ⊓ a

Tactic:
iSup_range

Goal state after:
α : Type u
ι : Sort w
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ ⨆ i, f i ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨅ i, ⨆ i_1 ∈ range (f i), i_1

Tactic:
iSup_range

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ ⨆ a_1 ∈ range fun i ↦ f i, a_1 ⊓ a = ⨆ i, f i ⊓ a

Tactic:
iSup_range

Goal state after:
α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ ⨆ i, f i ⊓ a = ⨆ i, f i ⊓ a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
⊢ CompleteAtomicBooleanAlgebra α

Tactic:
let completeBooleanAlgebra := e.completeBooleanAlgebra

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
⊢ CompleteAtomicBooleanAlgebra α
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
    rw [Icc_self, mem_singleton_iff] at hz
    rwa [hz]

Goal state after:
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 ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ ∃ c, b = a + c

Tactic:
refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
by
  have ⟨a, ha⟩ := exists_ne (0 : α)
  obtain lt | lt := ha.lt_or_gt
  · exact ⟨0, ⟨-a, neg_nonneg.mpr lt.le⟩, Subtype.coe_ne_coe.mp (neg_ne_zero.mpr ha).symm⟩
  · exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsLUB S ⟨a, ⋯⟩

Tactic:
subst hS

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsLUB ∅ ⟨a, ⋯⟩
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsGLB S ⟨b, ⋯⟩

Tactic:
subst hS

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsGLB ∅ ⟨b, ⋯⟩
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ q • ↑a

Tactic:
by rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg a.2

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

Goal state before:
pp: case inr
m n : ℕ
hm : 1 < m
⊢ m = n ↔ n = m

Tactic:
eq_comm

Goal state after:
case inr
m n : ℕ
hm : 1 < m
⊢ n = m ↔ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
    exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

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

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

Tactic:
add_descFactorial_eq_ascFactorial _ k,

Goal state after:
n k : ℕ
⊢ (n + k + 1) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
· suffices fract x < 1 by simpa
      refine lt_of_le_of_lt ?_ h
      apply le_mul_of_one_le_left <;> simp

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

Goal state before:
pp: a b : ℕ+
h : b < a
⊢ a - b + b = a

Tactic:
add_comm,

Goal state after:
a b : ℕ+
h : b < a
⊢ b + (a - b) = a
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (↑y + x) = y + round x

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = y + round x
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (↑y + x) = ↑y + round x

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (x + ↑y) = ↑y + round x