awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun (a b : α) ↦ decide (a ≤ b)
this_1 :
  ∀ (i : Fin n),
    ∃ (j : Fin sli.length),
      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ = val i
i j : Fin n
pf : ∀ (j : Fin sli.length), (↑j : ℕ) < sli.length
hi : ∃ (j : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i
hj : ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j
h_eq :
  ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hi.choose (p := fun (j : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
          ℕ)
        ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
          ℕ)
        ⋯
this :
  ∀ (i j : Fin (li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).length) (_hij : i < j),
    decide ((li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).get j) =
      true
h :
  (↑(hi.choose (p := fun (j : Fin sli.length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
      ℕ) ≤
    (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
      ℕ)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
      (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ)
      ⋯ ≤
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
        ℕ)
      ⋯

Tactic:
simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose h_eq; simp [h_eq])

Premises used: Exists.choose
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i ≤ toInt val j ↔ val i ≤ val j

Tactic:
simp [toInt, (exists_translation val).choose_spec]

Premises used: Exists.choose_spec, Mathlib.Tactic.Order.ToInt.toInt, Mathlib.Tactic.Order.ToInt.exists_translation
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i < toInt val j ↔ val i < val j

Tactic:
simpa using (toInt_le_toInt val j i).not

Premises used: Mathlib.Tactic.Order.ToInt.toInt_le_toInt, Iff.not
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i = toInt val j ↔ val i = val j

Tactic:
simp [toInt_le_toInt, le_antisymm_iff]

Premises used: Mathlib.Tactic.Order.ToInt.toInt_le_toInt, le_antisymm_iff
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ toInt val i ≠ toInt val j ↔ val i ≠ val j

Tactic:
simpa using (toInt_eq_toInt val i j).not

Premises used: Iff.not, Mathlib.Tactic.Order.ToInt.toInt_eq_toInt
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i ≤ toInt val j ↔ ¬val i ≤ val j

Tactic:
simpa using toInt_lt_toInt val j i

Premises used: Mathlib.Tactic.Order.ToInt.toInt_lt_toInt
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j : Fin n
⊢ ¬toInt val i < toInt val j ↔ ¬val i < val j

Tactic:
simpa using toInt_le_toInt val j i

Premises used: Mathlib.Tactic.Order.ToInt.toInt_le_toInt
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j k : Fin n
⊢ max (toInt val i) (toInt val j) = toInt val k ↔ max (val i) (val j) = val k

Tactic:
simp [le_antisymm_iff, sup_le_iff, le_sup_iff, toInt_le_toInt]

Premises used: Mathlib.Tactic.Order.ToInt.toInt_le_toInt, sup_le_iff, le_antisymm_iff, le_sup_iff
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
i j k : Fin n
⊢ min (toInt val i) (toInt val j) = toInt val k ↔ min (val i) (val j) = val k

Tactic:
simp [le_antisymm_iff, inf_le_iff, le_inf_iff, toInt_le_toInt]

Premises used: Mathlib.Tactic.Order.ToInt.toInt_le_toInt, inf_le_iff, le_inf_iff, le_antisymm_iff
-- Module: Mathlib.Tactic.Order.ToInt
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
n : ℕ
val : Fin n → α_1
i j k : Fin n
u : Level
α :
  let u := u;
  Q(Type u)
atoms : Array Q(«$α»)
h : ¬atoms.isEmpty = true
⊢ 0 < atoms.size

Tactic:
simpa [Array.size_pos_iff] using h

Premises used: Array.size_pos_iff
-- Module: Mathlib.Tactic.PNatToNat
Goal:
m n : ℕ+
⊢ m = n ↔ (↑m : ℕ) = (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.PNatToNat
Goal:
m n : ℕ+
⊢ m ≤ n ↔ (↑m : ℕ) ≤ (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.PNatToNat
Goal:
m n : ℕ+
⊢ m < n ↔ (↑m : ℕ) < (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Tactic.PNatToNat
Goal:
a b : ℕ+
mk :
  ∀ (val : ℕ) (property : 0 < val),
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property - b) : ℕ) =
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property) : ℕ) - 1 - (↑b : ℕ) + 1
⊢ (↑(a - b) : ℕ) = (↑a : ℕ) - 1 - (↑b : ℕ) + 1

Tactic:
cases a
-- Module: Mathlib.Tactic.PNatToNat
Goal:
b : ℕ+
val : ℕ
property : 0 < val
mk :
  ∀ (val_1 : ℕ) (property_1 : 0 < val_1),
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property - Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val_1 property_1) :
        ℕ) =
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property) : ℕ) - 1 -
          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val_1 property_1) : ℕ) +
        1
⊢ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property - b) : ℕ) =
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property) : ℕ) - 1 - (↑b : ℕ) + 1

Tactic:
cases b
-- Module: Mathlib.Tactic.PNatToNat
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
mk : (if val_1 < val then val - val_1 else 1) = val - 1 - val_1 + 1
⊢ (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property - Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val_1 property_1) : ℕ) =
    (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val property) : ℕ) - 1 -
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) val_1 property_1) : ℕ) +
      1

Tactic:
simp only [PNat.mk_coe, _root_.PNat.sub_coe, ← _root_.PNat.coe_lt_coe]

Premises used: PNat.sub_coe, PNat.coe_lt_coe, PNat.mk_coe
-- Module: Mathlib.Tactic.PNatToNat
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
pos : val_1 < val → val - val_1 = val - 1 - val_1 + 1
neg : ¬val_1 < val → 1 = val - 1 - val_1 + 1
⊢ (if val_1 < val then val - val_1 else 1) = val - 1 - val_1 + 1

Tactic:
split_ifs
-- Module: Mathlib.Tactic.PNatToNat
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
h : val_1 < val
⊢ val - val_1 = val - 1 - val_1 + 1

Tactic:
lia
-- Module: Mathlib.Tactic.PNatToNat
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
h : ¬val_1 < val
⊢ 1 = val - 1 - val_1 + 1

Tactic:
lia
-- Module: Mathlib.Tactic.Peel
Goal:
p q r : Prop
h : r → p → q
inl : ∀ (h : ¬r), r → p → r ∧ q
inr inr₁ : ∀ (h : p → q), r → p → r ∧ q
inr₂ : ∀ (h : p → q), r → p → r
inr₃ : ∀ (h : p → q), r → p → q
inr₄ : r → p → ∀ (h : ¬p), q
inr₅ inr₆ inr₇ : r → p → ∀ (h : q), q
⊢ r ∧ p → r ∧ q

Tactic:
tauto
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x → q x
hp : ∀ᶠ (x : α) in f, p x
⊢ ∀ᶠ (x : α) in f, q x

Tactic:
Filter.Eventually.mp hp (Filter.Eventually.of_forall hq)

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x → q x
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ᶠ (x : α) in f, q x

Tactic:
Filter.Frequently.mp hp (Filter.Eventually.of_forall hq)

Premises used: Filter.Eventually.of_forall, Filter.Frequently.mp
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq a : ∀ (x : α), p x ↔ q x
⊢ (∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x

Tactic:
congr! 2
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x : α
⊢ p x ↔ q x

Tactic:
hq _
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x : α
⊢ p x ↔ q x

Tactic:
exact hq _
-- Module: Mathlib.Tactic.Peel
Goal:
α : Type u_1
p q : α → Prop
f : Filter α
hq a : ∀ (x : α), p x ↔ q x
⊢ (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x

Tactic:
congr! 2
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
α : Sort u_1
a c b : α
hab : a ≠ c
hbc : a = b
⊢ b ≠ c

Tactic:
hbc ▸ hab

Premises used: Eq.rec
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
inst_3 : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
rw : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
inst_3 : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
apply : 0 < n
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)

Tactic:
apply Nat.cast_pos.2

Premises used: Iff.mpr, Nat.cast_pos
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
inst_3 : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n

Tactic:
simpa using w
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h'' : NeZero.{u_1} (R := A) 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
rw : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h'' : NeZero.{u_1} (R := A) 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
apply : 0 < n
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)

Tactic:
apply Nat.cast_pos'.2

Premises used: Iff.mpr, Nat.cast_pos'
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h'' : NeZero.{u_1} (R := A) 1
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n

Tactic:
simpa using w
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
h : NormNum.IsNat e n
rw : LE.le.{u_1} (α := A) 0 (↑n : A)
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
h : NormNum.IsNat e n
⊢ LE.le.{u_1} (α := A) 0 (↑n : A)

Tactic:
Nat.cast_nonneg n

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
h : NormNum.IsNat e n
⊢ LE.le.{u_1} (α := A) 0 (↑n : A)

Tactic:
exact Nat.cast_nonneg n

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h : NormNum.IsNat e n
rw : LE.le.{u_1} (α := A) 0 (↑n : A)
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsNat.to_eq, rfl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ LE.le.{u_1} (α := A) 0 (↑n : A)

Tactic:
Nat.cast_nonneg' n

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : AddMonoidWithOne A
inst_1 : PartialOrder A
inst_2 : AddLeftMono A
inst_3 : ZeroLEOneClass A
h : NormNum.IsNat e n
⊢ LE.le.{u_1} (α := A) 0 (↑n : A)

Tactic:
exact Nat.cast_nonneg' n

Premises used: Nat.cast_nonneg'
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Ring A
inst_1 : PartialOrder A
inst_2 : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
rw : Ne.{u_1 + 1} (α := A) (-(↑n : A)) 0
⊢ e ≠ 0

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Premises used: Mathlib.Meta.NormNum.IsInt.neg_to_eq, rfl
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Ring A
inst_1 : PartialOrder A
inst_2 : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
simp : ¬Eq.{u_1 + 1} (α := A) (↑n : A) 0
⊢ Ne.{u_1 + 1} (α := A) (-(↑n : A)) 0

Tactic:
simp only [ne_eq, neg_eq_zero]

Premises used: neg_eq_zero, ne_eq
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Ring A
inst_1 : PartialOrder A
inst_2 : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
h₁ : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ ¬Eq.{u_1 + 1} (α := A) (↑n : A) 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℕ
inst : Ring A
inst_1 : PartialOrder A
inst_2 : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)

Tactic:
simpa using w
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
⊢ LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)

Tactic:
have pos_n : (0 < (n : A)) := Nat.cast_pos (n := n) |>.2 (of_decide_eq_true h)
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
rw : 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ 0 < e

Tactic:
rw [eq]
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
mul_pos pos_n pos_invOf_d

Premises used: mul_pos
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
exact mul_pos pos_n pos_invOf_d

Premises used: mul_pos
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
⊢ LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)

Tactic:
have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
rw : 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ 0 < e

Tactic:
rw [eq]
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
mul_pos pos_n pos_invOf_d

Premises used: mul_pos
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (0 < n) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
pos_n : LT.lt.{u_1} (α := A) 0 (↑n : A)
⊢ 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
exact mul_pos pos_n pos_invOf_d

Premises used: mul_pos
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n = 0) = true
rw : 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]

Premises used: of_decide_eq_true
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n d : ℕ
inst : Semiring A
inst_1 : LinearOrder A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n = 0) = true
⊢ 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
simp
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n = 0) = true
rw : 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]

Premises used: of_decide_eq_true
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n = 0) = true
⊢ 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
simp
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
⊢ LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)

Tactic:
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
⊢ LT.lt.{u_1} (α := A) (↑n : A) 0

Tactic:
have neg_n : ((n : A) < 0) := Int.cast_lt_zero (n := n) |>.2 (of_decide_eq_true h)
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
neg_n : LT.lt.{u_1} (α := A) (↑n : A) 0
⊢ HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) < 0

Tactic:
have neg := mul_neg_of_neg_of_pos neg_n pos_invOf_d
-- Module: Mathlib.Tactic.Positivity.Core
Goal:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst : Ring A
inst_1 : LinearOrder A
inst_2 : IsStrictOrderedRing A
inv : Invertible (α := A) (↑d : A)
eq : e = HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
h : decide (n < 0) = true
pos_invOf_d : LT.lt.{u_1} (α := A) 0 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
neg_n : LT.lt.{u_1} (α := A) (↑n : A) 0
neg : HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) < 0
rw : HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) ≠ 0
⊢ e ≠ 0

Tactic:
rw [eq]