awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (goal)
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 :
  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)) :
        ℕ)
      ⋯
⊢ (↑(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)) :
      ℕ)
have neg : ∀
  (h :
    (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
        ℕ) <
      (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = 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 : ℕ) sorry = val j)) :
        ℕ)
      sorry <
    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 : ℕ) sorry = val i)) :
        ℕ)
      sorry
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (goal)
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)) :
      ℕ)
⊢ 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)
have apply : (↑(hi.choose (p := fun (j : Fin sli.length) ↦
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
    ℕ) ≠
  (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
    ℕ)
Tactic: apply lt_of_le_of_ne h
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (goal)
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)) :
      ℕ)
⊢ (↑(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)) :
      ℕ)
have contrapose : ∀
  (h_eq :
    (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
        ℕ) =
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = 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 : ℕ) sorry = val i)) :
        ℕ)
      sorry =
    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 : ℕ) sorry = val j)) :
        ℕ)
      sorry
Tactic: contrapose h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.Tactic.PNatToNat (goal)
Goal:
a b : ℕ+
⊢ (↑(a - b) : ℕ) = (↑a : ℕ) - 1 - (↑b : ℕ) + 1
have 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
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Tactic.PNatToNat (goal)
Goal:
b : ℕ+
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
have 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
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Tactic.PNatToNat (goal)
Goal:
val : ℕ
property : 0 < val
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
have mk : (if val_1 < val then val - val_1 else 1) = val - 1 - val_1 + 1
Tactic: simp only [PNat.mk_coe, _root_.PNat.sub_coe, ← _root_.PNat.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Tactic.PNatToNat (goal)
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
⊢ (if val_1 < val then val - val_1 else 1) = val - 1 - val_1 + 1
have pos : val_1 < val → val - val_1 = val - 1 - val_1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Tactic.PNatToNat (goal)
Goal:
val : ℕ
property : 0 < val
val_1 : ℕ
property_1 : 0 < val_1
pos : val_1 < val → val - val_1 = val - 1 - val_1 + 1
⊢ (if val_1 < val then val - val_1 else 1) = val - 1 - val_1 + 1
have neg : ¬val_1 < val → 1 = val - 1 - val_1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
Goal:
p q r : Prop
h : r → p → q
⊢ r ∧ p → r ∧ q
have inl : ∀ (h : ¬r), r → p → r ∧ q
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
Goal:
p q r : Prop
h : r → p → q
inl : ∀ (h : ¬r), r → p → r ∧ q
⊢ r ∧ p → r ∧ q
have inr : ∀ (h : p → q), r → p → r ∧ q
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
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
⊢ r ∧ p → r ∧ q
have inr₂ : ∀ (h : p → q), r → p → r
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
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
⊢ r ∧ p → r ∧ q
have inr₃ : ∀ (h : p → q), r → p → q
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
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
⊢ r ∧ p → r ∧ q
have inr₄ : r → p → ∀ (h : ¬p), q
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Peel (goal)
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
⊢ r ∧ p → r ∧ q
have inr₅ : r → p → ∀ (h : q), q
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 < e
have rw : LT.lt.{u_1} (α := A) 0 (↑n : A)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)
have apply : 0 < n
Tactic: apply Nat.cast_pos.2
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 < e
have rw : LT.lt.{u_1} (α := A) 0 (↑n : A)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ LT.lt.{u_1} (α := A) 0 (↑n : A)
have apply : 0 < n
Tactic: apply Nat.cast_pos'.2
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
Goal:
A : Type u_1
e : A
n : ℕ
inst : Semiring A
inst_1 : PartialOrder A
inst_2 : IsOrderedRing A
h : NormNum.IsNat e n
⊢ 0 ≤ e
have rw : LE.le.{u_1} (α := A) 0 (↑n : A)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ 0 ≤ e
have rw : LE.le.{u_1} (α := A) 0 (↑n : A)
Tactic: rw [NormNum.IsNat.to_eq h rfl]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ e ≠ 0
have rw : Ne.{u_1 + 1} (α := A) (-(↑n : A)) 0
Tactic: rw [NormNum.IsInt.neg_to_eq h rfl]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ Ne.{u_1 + 1} (α := A) (-(↑n : A)) 0
have simp : ¬Eq.{u_1 + 1} (α := A) (↑n : A) 0
Tactic: simp only [ne_eq, neg_eq_zero]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ ¬Eq.{u_1 + 1} (α := A) (↑n : A) 0
have h₁ : LT.lt.{u_1} (α := A) 0 (↑n : A)
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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
⊢ 0 < e
have pos_invOf_d : 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
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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) _)
⊢ 0 < e
have pos_n : 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)
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 < e
have rw : 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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
⊢ 0 < e
have pos_invOf_d : 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
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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) _)
⊢ 0 < e
have pos_n : 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)
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 < e
have rw : 0 < HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 ≤ e
have rw : 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
Tactic: rw [eq, of_decide_eq_true h]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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 ≤ e
have rw : 0 ≤ HMul.hMul (α := A) (↑0 : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _)
Tactic: rw [eq, of_decide_eq_true h]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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
⊢ e ≠ 0
have pos_invOf_d : 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
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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) _)
⊢ e ≠ 0
have neg_n : 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)
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (hypothesis)
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
⊢ e ≠ 0
have neg : 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
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Core (goal)
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
⊢ e ≠ 0
have rw : HMul.hMul (α := A) (↑n : A) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : A) _) ≠ 0
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Tactic.Push (goal)
Goal:
p q : Prop
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
have rw : ¬p ∧ q ∨ p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
Tactic: rw [not_not, or_comm]
-- Lean 4 proof step from Mathlib.Tactic.Push (goal)
Goal:
p q : Prop
rw : ¬p ∧ q ∨ p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
⊢ ¬p ∧ q ∨ ¬¬p ∧ ¬q ↔ p ∧ ¬q ∨ ¬p ∧ q
have rw₁ : p ∧ ¬q ∨ ¬p ∧ q ↔ p ∧ ¬q ∨ ¬p ∧ q
Tactic: rw [not_not, or_comm]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
⊢ e = (↑r : α)
have rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
Tactic: rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
⊢ e = (↑r : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n : ℤ)) : α) (↑r : α)
Tactic: rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n : ℤ)) : α) (↑r : α)
⊢ e = (↑r : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n' : ℤ)) : α) (↑r : α)
Tactic: rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]
-- Lean 4 proof step from Mathlib.Tactic.ReduceModChar (goal)
Goal:
e' r : ℤ
α : Type u_1
inst_1 : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % (↑n' : ℤ)) r
rw : Eq.{u_1 + 1} (α := α) (↑e' : α) (↑r : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n : ℤ)) : α) (↑r : α)
rw₂ : Eq.{u_1 + 1} (α := α) (↑(e' % (↑n' : ℤ)) : α) (↑r : α)
⊢ e = (↑r : α)
have rw₃ : Eq.{u_1 + 1} (α := α) (↑(↑r : ℤ) : α) (↑r : α)
Tactic: rw [he.out, CharP.intCast_eq_intCast_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]