mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊤
⊢ False

Tactic:
exact (coe_lt_top <| Classical.arbitrary _).not_ge <| h <| by simp

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊥
⊢ x + z ≤ y + z → x ≤ y

Tactic:
lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using le_of_add_le_add_right

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋.toNat ↔ ↑n ≤ a

Tactic:
Int.le_toNat (Int.floor_nonneg.2 ha),

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ≤ ⌊a⌋ ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d + ↑n ≤ a + ↑n ↔ d + n ≤ ⌊a⌋₊ + n

Tactic:
add_le_add_iff_right,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d ≤ a ↔ d + n ≤ ⌊a⌋₊ + n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d ≤ a ↔ d + n ≤ ⌊a⌋₊ + n

Tactic:
add_le_add_iff_right,

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑d ≤ a ↔ d ≤ ⌊a⌋₊
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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Tactic:
by
  rw [cast_one.symm, ceil_add_natCast ha 1]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Tactic:
invOf_sub_invOf

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

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

Tactic:
by rw [right_distrib, div_mul_cancel₀ _ hc]

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

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

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a : K
⊢ a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
rw [eq_comm, inv_eq_self₀]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ f ↑q = f (↑q.num / ↑q.den)

Tactic:
nnratCast,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q = f (↑q.num / ↑q.den)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)

Tactic:
refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.Bounds.Basic

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

Tactic:
rintro (⟨hs, hts⟩ | ⟨ht, hst⟩) x hx y hy
    · obtain ⟨x', hx', hxx'⟩ := hts.union_right hx
      obtain ⟨y', hy', hyy'⟩ := hts.union_right hy
      obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
      exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩
    · 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.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
⊢ a = c ∧ b = d

Tactic:
obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
⊢ a = c ∧ b = d
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
mul_two,

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a ≤ a + a ↔ 0 ≤ a
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
mul_two,

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a < a + a ↔ 0 < a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn)

Goal state after:
case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun a ↦ 0) '' s) 0

Tactic:
obtain rfl | ne := s.eq_empty_or_nonempty

Goal state after:
case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsLUB ∅ b
⊢ IsLUB ((fun a ↦ 0) '' ∅) 0

case inr.inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
ne : s.Nonempty
⊢ IsLUB ((fun a ↦ 0) '' s) 0
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get ⟨n, h⟩]

Tactic:
rw [drop_eq_getElem_cons h, take, take]
  simp

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 : α
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a

Tactic:
div_lt_iff_of_neg' hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
⊢ b * (1 / a) < 1
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, hb.ne, div_lt_one_of_neg]
  · simp [zero_lt_one]
  · simp [hb, hb.not_gt, div_lt_one, hb.ne.symm]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
rel_congr_left (perm_insertIdx _ _ hm),

Goal state after:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ a :: l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L).prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
h' i (Nat.le_of_lt h₁)

Goal state after:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case succ
G : Type u_7
inst✝ : Group G
f : ℕ → G
n : ℕ
h : (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n
⊢ (map (fun k ↦ f k / f (k + 1)) (range (n + 1))).prod = f 0 / f (n + 1)

Tactic:
simp [range_succ, prod_append, map_append, h]

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

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

Tactic:
obtain ⟨b, hb⟩ := b
  simp [toNonneg, hb]

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

Goal state before:
pp: α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
refine map_injective_iff.2 Subtype.coe_injective ?_

Goal state after:
α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ map (fun a ↦ ↑a) (filter p l.attach) =
    map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length + 1 = l.length

Tactic:
erase_eq_eraseP,

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (eraseP (fun x ↦ a == x) l).length + 1 = l.length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (l.erase a) = (map f l).erase (f a)

Tactic:
erase_eq_eraseP,

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = (map f l).erase (f a)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = (map f l).erase (f a)

Tactic:
erase_eq_eraseP,

Goal state after:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
finj : Injective f
a : α
l : List α
this : (fun x ↦ a == x) = fun x ↦ f a == f x
⊢ map f (eraseP (fun x ↦ a == x) l) = eraseP (fun x ↦ f a == x) (map f l)
Module: Mathlib.Algebra.Group.Semiconj.Basic

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

Tactic:
eq_mul_inv_iff_mul_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ a⁻¹ * y * a = x ↔ a * x = y * a
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
hm : IsPrimal 0
⊢ IsPrimal (0 * n)

Tactic:
rwa [zero_mul]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r) a

Tactic:
simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
⊢ newBasic.size = s.basic.size

Tactic:
by apply Array.size_setIfInBounds

Goal state after:
Module: Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm

Goal state before:
pp: matType : Nat → Nat → Type
inst✝ : UsableInSimplexAlgorithm matType
exitIdx enterIdx : Nat
s : Tableau matType
mat✝² : matType s.basic.size s.free.size := s.mat
intersectCoef : Rat := mat✝²[(exitIdx, enterIdx)]!
__s✝ : matType s.basic.size s.free.size
mat✝¹ : matType s.basic.size s.free.size := __s✝
mat✝ : matType s.basic.size s.free.size := setElem mat✝¹ exitIdx enterIdx (-1)
mat : matType s.basic.size s.free.size := divideRow mat✝ exitIdx (-intersectCoef)
newBasic : Array Nat := s.basic.set! exitIdx s.free[enterIdx]!
newFree : Array Nat := s.free.set! enterIdx s.basic[exitIdx]!
hb : newBasic.size = s.basic.size
⊢ newFree.size = s.free.size

Tactic:
by apply Array.size_setIfInBounds

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

Goal state before:
pp: case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ y, range fun s ↦ ↑(f s y)) → x ∈ ⋃₀ C

Tactic:
rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
    refine ⟨_, hs, ?_⟩
    exact (f ⟨s, hs⟩ y).2

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: case pos
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : κ → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∀ (k : κ), I k = I j
⊢ ⨅ a, f (I a) ≤ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i

Tactic:
exact le_iSup₂_of_le (I j) (fun k ↦ (H k) ▸ (hI k)) (iInf_le _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsGLB s (sInf s)

Tactic:
by_cases hs : BddBelow s

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
completeLattice : CompleteLattice α := e.completeLattice
biheytingAlgebra : BiheytingAlgebra α := e.biheytingAlgebra
⊢ CompleteDistribLattice α

Tactic:
apply e.injective.completeDistribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
← Icc_min_max,

Goal state after:
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (min (f a) (f b)) (max (f a) (f b))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
← Icc_min_max,

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (min (f a) (f b)) (max (f a) (f b))
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
simp_rw [mem_uIoc]; rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;> apply le_antisymm <;>
    first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
this : Std.Symm fun a b ↦ r a b ∨ r b a
⊢ ((s ∪ t).Pairwise fun x y ↦ r x y ∨ r y x) ↔
    (s.Pairwise fun x y ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun x y ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
pairwise_union_of_symm

Goal state after:
α : Type u_1
r : α → α → Prop
s t : Set α
this : Std.Symm fun a b ↦ r a b ∨ r b a
⊢ ((s.Pairwise fun x y ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun x y ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a) ↔
    (s.Pairwise fun x y ↦ r x y ∨ r y x) ∧
      (t.Pairwise fun x y ↦ r x y ∨ r y x) ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
⊢ ∀ ⦃y : β⦄, y ∈ ⇑φ '' s → b ≠ y → r'ᶜ b y

Tactic:
b'

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ⇑φ '' s
b' : β
⊢ b' ∈ ⇑φ '' s → b ≠ b' → r'ᶜ b b'
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
rw [← le, mul, mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f a * f b ≤ f a * f c
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
rw [← le, mul, mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f b * f a ≤ f c * f a
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_eq_right.2 le_sup_right

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = |a|ₘ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ (0 + 0) * 1 = 0

Tactic:
Nat.zero_add,

Goal state after:
⊢ 0 * 1 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
succ_add_eq_add_succ n (k + 1)

Goal state after:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n) = ↑q ^ n

Tactic:
rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

Goal state after: