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

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
⊢ sSup ∅ = default

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = default

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddBelow t
h : sInf (Subtype.val '' t) ∈ s
⊢ sInf (Subtype.val '' t) = ↑(sInf t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
⊢ sInf ∅ = default

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = default

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y} ↦ ↑y) '' t) ↑(sSup t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x} ↦ ↑x) '' t) ↑(sInf t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = sSup ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = sInf ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ sSup (Subtype.val '' S) ∈ Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
⊢ IsLUB S (if hS : S = ∅ then ⟨a, ⋯⟩ else ⟨sSup (Subtype.val '' S), ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ sInf (Subtype.val '' S) ∈ Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
⊢ IsGLB S (if hS : S = ∅ then ⟨b, ⋯⟩ else ⟨sInf (Subtype.val '' S), ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
S : Set ↑(Iic a)
⊢ sSup (Subtype.val '' S) ∈ Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
S : Set ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' S) ∈ Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
⊢ ∀ (a_1 : ↑(Iic a)), a_1 ≤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
a : α
⊢ ∀ (a_1 : ↑(Iic a)), ⊥ ≤ a_1

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨆ i, ⨆ (_ : p i), f i) = ⨆ i, ⨆ (_ : p i), ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(⨅ i, f i) = a ⊓ ⨅ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
p : ι → Prop
⊢ ↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
⊢ 0 ≤ ↑q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨↑r, ⋯⟩ * ⟨(↑r)⁻¹, ⋯⟩ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ ⟨(↑r)⁻¹, ⋯⟩ * ⟨↑r, ⋯⟩ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 ≤ r }ˣ
⊢ (fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) ((fun r ↦ ⟨↑↑r, ⋯⟩) r) = r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝³ : DivisionSemiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : PosMulReflectLT R
r : { r // 0 < r }
⊢ (fun r ↦ ⟨↑↑r, ⋯⟩) ((fun r ↦ { val := ⟨↑r, ⋯⟩, inv := ⟨(↑r)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }) r) = r

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsNat a na
⊢ IsNat |a| na

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : Lattice α
inst✝ : IsOrderedRing α
a : α
na : ℕ
pa : IsInt a (Int.negOfNat na)
⊢ IsNat |a| na

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsNNRat a num den
⊢ IsNNRat |a| num den

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : DivisionRing α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
num den : ℕ
ra : IsRat a (Int.negOfNat num) den
⊢ IsNNRat |a| num den

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : n✝¹.beq n✝ = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : CharZero α
num✝¹ num✝ denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul denom✝ = num✝.mul denom✝¹) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
by

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

Goal state before:
pp: n✝ : ℤ
⊢ ↑n✝ / ↑0 = ↑0

Tactic:
by

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

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a / b = ↑q

Tactic:
by

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

Goal state before:
pp: a b q q' : ℤ
h : IsInt (a / -b) q
hq : -q = q'
⊢ a / b = ↑q'

Tactic:
by

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

Goal state before:
pp: a : ℤ
b : ℕ
h : IsInt a (Int.negOfNat b)
⊢ -a = ↑b

Tactic:
by

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

Goal state before:
pp: x✝¹ x✝ : ℤ
e : IsInt x✝¹ x✝
⊢ IsInt (x✝¹ % ↑0) x✝

Tactic:
by

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

Goal state before:
pp: a b q m a' : ℤ
b' r : ℕ
ha : IsInt a a'
hb : IsNat b b'
hm : q * ↑b' = m
h : ↑r + m = a'
h₂ : r.blt b' = true
⊢ a % b = ↑r

Tactic:
by

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

Goal state before:
pp: a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % b = ↑r

Tactic:
by

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

Goal state before:
pp: n✝¹ n✝ : ℤ
e : (n✝.emod n✝¹ != 0) = true
⊢ ¬↑n✝ % ↑n✝¹ = 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < ↑q

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ
⊢ p < q → ↑p < ↑q

Tactic:
by

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ 0 ≤ ↑q ↔ 0 ≤ q

Tactic:
by

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
by

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ 0 < ↑q ↔ 0 < q

Tactic:
by

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
⊢ ↑q < 0 ↔ q < 0

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
rw [← cast_le (K := K), cast_intCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
rw [← cast_le (K := K), cast_intCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p < ↑q

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ≥0
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ≥0
⊢ 0 < ↑q ↔ 0 < q

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
q : ℚ≥0
⊢ ↑q < 0 ↔ q < 0

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ ↑p ≤ 1 ↔ p ≤ 1

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ 1 ≤ ↑p ↔ 1 ≤ p

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ ↑p < 1 ↔ p < 1

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p : ℚ≥0
⊢ 1 < ↑p ↔ 1 < p

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ mulSupport f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 1) ∧ ∀ (x : ι), ¬x ∈ s → f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
⊢ f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = insert x (mulSupport f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
⊢ mulSupport (update f x 1) = mulSupport f \ {x}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : One M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
f : ι → M
x : ι
y : M
⊢ mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
⊢ extend f g 1 x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
⊢ f '' mulSupport g ⊆ mulSupport (extend f g 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
mulSupport_disjoint_iff

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ EqOn f 1 s ↔ EqOn f 1 s
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ mulSupport f = ∅ ↔ f = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹.mul db ≤ num✝.mul da) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (mulSupport f).Nonempty ↔ f ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * db < num✝ * da) = true
h : ↑(num✝¹ * db) < ↑(num✝ * da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * db < num✝ * da) = true
h : ↑(num✝¹ * db) < ↑(num✝ * da)
ha : 0 < ⅟↑da
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
c : M
hc : c ≠ 1
⊢ (mulSupport fun x ↦ c) = univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : ι → M
g : ι → N
x : ι
hx : x ∈ mulSupport fun x ↦ op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x ↦ op (f x) (g x)) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
g : M → N
hg : g 1 = 1
f : ι → M
x : ι
h : f x = 1
⊢ (g ∘ f) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
⊢ (g ∘ f) x = 1 ↔ f x = 1

Tactic:
by

Goal state after: