mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici x)
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun y ↦ ⟨e ↑y, ⋯⟩) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici (e x))
⊢ (fun y ↦ ⟨e ↑y, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
by

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : ↑(Ici x)},
    { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range g)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc x y)
⊢ e ↑z ∈ Icc (e x) (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc (e x) (e y))
⊢ e.symm ↑z ∈ Icc x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc x y✝)
⊢ (fun z ↦ ⟨e.symm ↑z, ⋯⟩) ((fun z ↦ ⟨e ↑z, ⋯⟩) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc (e x) (e y✝))
⊢ (fun z ↦ ⟨e ↑z, ⋯⟩) ((fun z ↦ ⟨e.symm ↑z, ⋯⟩) y) = y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
⊢ ∀ {a b : ↑(Icc x y)},
    { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
by

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
⊢ a = c ∧ b = d → Icc a b = Icc c d

Tactic:
by

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
⊢ a = c ∧ b = d → Icc a b = Icc c d

Tactic:
by rintro ⟨rfl, rfl⟩; rfl

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
heq : Icc a b = Icc c d
⊢ c ≤ d

Tactic:
by

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
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Icc a ⊤ = Ici a

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ Ioc a ⊤ = Ioi a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioo x y)
a : α
ha : a ∈ Ioo x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioc x y)
a : α
ha : a ∈ Ioc x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioi x)
a : α
ha : a ∈ Ioi x
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
by

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

Goal state before:
pp: ⊢ Iic False = {False}

Tactic:
by

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

Goal state before:
pp: ⊢ Iic True = univ

Tactic:
by

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

Goal state before:
pp: ⊢ Ici False = univ

Tactic:
by

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

Goal state before:
pp: ⊢ Ici True = {True}

Tactic:
by

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

Goal state before:
pp: ⊢ Iio False = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ Iio True = {False}

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ Ioi False = {True}

Tactic:
by

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

Goal state before:
pp: ⊢ Ioi True = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Icc a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ IsGreatest univ a ↔ IsTop a

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderTop γ
⊢ upperBounds univ = {⊤}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoTopOrder α
⊢ ¬BddAbove univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ upperBounds ∅ = univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ IsGLB ∅ a ↔ IsTop a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ upperBounds s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s : Set α
a : α
⊢ BddAbove (insert a s) ↔ BddAbove s

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB (insert a s) (a ⊔ b)

Tactic:
by

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (max a b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : DirectedOn (fun x y ↦ y ≤ x) s
hMin : Minimal (fun x ↦ x ∈ s) a
hb : b ∈ s
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
hs : s.Nonempty
ht : t.Nonempty
ha : IsLUB s a
hb : IsLUB t b
⊢ IsLUB (s ×ˢ t) (a, b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ IsLUB s a ↔ IsLUB s b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ IsGLB s a ↔ IsGLB s b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c ∈ s, b < c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ IsLeast {w | a ≤ b ⊔ w} (a \ b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a : α
⊢ IsGreatest {w | Disjoint w a} aᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ IsLeast {w | Codisjoint a w} (￢a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : ℕ → Prop
n : ℕ
inst✝ : DecidablePred p
⊢ (∀ k < n, ¬p k) ↔ n ∈ lowerBounds {n | p n}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
num : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num * ⅟↑1 = ↑num

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑(Int.ofNat a✝) * ⅟↑denom✝ = ↑a✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ 1 * ↑1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑1 * 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n✝ : ℕ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ denom✝ : ℕ
inv : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑(Int.ofNat num✝) * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1

Tactic:
by

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

Goal state before:
pp: α : Type u
n d : ℕ
inst✝ : DivisionSemiring α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = NNRat.rawCast n d

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℤ
d : ℕ
inst✝ : DivisionRing α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = Rat.rawCast n d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑n * ⅟↑d = ↑n / ↑d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
n d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ NNRat.rawCast n d = ↑n * ⅟↑d

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ Rat.rawCast n d = ↑n * ⅟↑d

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : Semiring A
inst✝² : PartialOrder A
inst✝¹ : IsOrderedRing A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h'' : NeZero 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Semiring A
inst✝¹ : PartialOrder A
inst✝ : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝³ : AddMonoidWithOne A
inst✝² : PartialOrder A
inst✝¹ : AddLeftMono A
inst✝ : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
n₁ : ℕ
x a₁ : α
n₂ : ℕ
a₂ : α
n' : ℕ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ term n₁ x a₁ + term n₂ x a₂ = term n' x a'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
c : ℤ
⊢ smulg c 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x : α
⊢ x = termg 1 x 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝¹ : Semiring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l : ℕ
r : α
tl : ℕ
tr t : α
prl : l = tl
prr : r = tr
prt : smul tl tr = t
⊢ smul l r = t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l : ℤ
r : α
tl : ℤ
tr t : α
prl : l = tl
prr : r = tr
prt : smulg tl tr = t
⊢ smulg l r = t

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝¹ : Ring A
inst✝ : LinearOrder A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
by

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

Goal state before:
pp: A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝² : Ring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
⊢ e ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t

Tactic:
by

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

Goal state before:
pp: α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k * b) = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b

Tactic:
by

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

Goal state before:
pp: α : Type ?u.3
inst✝¹ : Semiring α
a k b : ℕ
inst✝ : Invertible ↑a
h : a = k * b
⊢ ↑a = ↑k * ↑b

Tactic:
by

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

Goal state before:
pp: a✝ : ℕ
⊢ (↑(Int.negOfNat a✝)).natAbs = ↑a✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m

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 * db + nb * da = k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)

Tactic:
by

Goal state after: