mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → α → α
a b : α
na nb nc da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsNNRat a na da →
      IsNNRat b nb db → (na.mul db).add (nb.mul da) = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 ≤ a
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ a ≤ a / b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ b < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a ≤ 1 / b ↔ b ≤ 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a < 1 / b ↔ b < 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ 0 < 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a ≤ 1 / b
⊢ b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ 0 < 1 / a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : 1 / a < 1 / b
⊢ b < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ a
hb : 1 ≤ b
⊢ a / b ≤ a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
ha : 0 < a
hb : 1 < b
⊢ a / b < a

Tactic:
by

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:
by

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:
by

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 α
⊢ a / 2 ≤ a ↔ 0 ≤ a

Tactic:
by

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 α
⊢ a / 2 < a ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ a < (a + b) / 2 ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
⊢ (a + b) / 2 < b ↔ a < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / (b * e) ≤ c / (d * e)

Tactic:
by

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

Goal state before:
pp: 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
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
l : List ι
⊢ (map (fun x ↦ 1) l).prod = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b c d : α
h : a * (b / c) ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : Semifield α
inst✝³ : PartialOrder α
inst✝² : PosMulReflectLT α
inst✝¹ : IsStrictOrderedRing α
β : Type u_4
inst✝ : Preorder β
f : β → α
hf : StrictMono f
c : α
hc : 0 < c
⊢ StrictMono fun x ↦ f x / c

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
⊢ { map := m, mapConst := mc } = { map := m', mapConst := mc' }

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: γ : Type u_1
⊢ LawfulFunctor (Const γ)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db → (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
by

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

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

Tactic:
by

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 α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
by

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 α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n

Tactic:
by

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 α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = m ^ l.length

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : Monoid M
inst✝ : Monoid N
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (map f l).prod (map g l).prod
⊢ r (map f (a :: l)).prod (map g (a :: l)).prod

Tactic:
by

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 α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ < (a ^ m)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
by

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

Goal state before:
pp: ⊢ @iterate = @iterateTR

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → α → α
a b : α
na nb nc da db dc k : ℕ
⊢ f = HMul.hMul →
    IsNNRat a na da → IsNNRat b nb db → na.mul nb = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
⊢ ∃ c, 0 < c ∧ b * c < a

Tactic:
by

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < c⁻¹ * a

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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 c : α
hc : c < 0
⊢ b / c ≤ a ↔ c * a ≤ b

Tactic:
by

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 c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c

Tactic:
by

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 c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ c * a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HMul.hMul → IsRat a na da → IsRat b nb db → na.mul nb = (↑k).mul nc → da.mul db = k.mul dc → IsRat (f a b) nc dc

Tactic:
by

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

Goal state before:
pp: «$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$mα'» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$mα» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
⊢ AddMonoidWithOne «$α»

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionSemiring α
x✝³ x✝² : α
x✝¹ x✝ : ℕ
h : IsNNRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsNNRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝

Tactic:
by

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 c : α
hc : c < 0
⊢ b / c < a ↔ c * a < b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
⊢ (↑n✝).succ = ↑n✝.succ

Tactic:
by

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

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(n✝¹.sub n✝)

Tactic:
by

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 c : α
hc : c < 0
⊢ a < b / c ↔ b < a * c

Tactic:
by

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

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(n✝¹.mod n✝)

Tactic:
by

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

Goal state before:
pp: n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(n✝¹.div n✝)

Tactic:
by

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 c : α
hc : c < 0
⊢ a < b / c ↔ b < c * a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : b ≤ a
hb : b ≤ 0
⊢ a / b ≤ 1

Tactic:
by

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

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

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

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

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

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

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 c : α
ha : c < a
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ take n x = x → x.length ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ x = take n x ↔ x.length ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
by

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 c : α
ha : b < c
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by

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 c : α
ha : b < c
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by
  by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
by

Goal state after: