awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
⊢ False
have this₁ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
Tactic: have := h (-x) (-y)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
⊢ False
have this₁ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
Tactic: have := h x y
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
⊢ False
have this₁ : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
Tactic: have := h x (-y)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
⊢ False
have refine_2 : x ∈ P → False
Tactic: cases (by aesop : x ∈ P ∨ -x ∈ P)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this_1 : HasMemOrNegMem P
x y : R
h_1 : x * y ∈ P.support
this_2 : ¬(x ∈ P.support ∨ y ∈ P.support)
this_3 : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this_4 : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this_5 : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
refine_2 : x ∈ P → False
⊢ False
have refine_2₁ : -x ∈ P → False
Tactic: cases (by aesop : x ∈ P ∨ -x ∈ P)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : RingPreordering R
h :
  Eq.{u_1 + 1} (α := Set R) ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) p)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)
⊢ p = q
have mk : ∀ (toSubsemiring : Subsemiring R) (mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier)
  (neg_one_notMem' : -1 ∉ toSubsemiring.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set R)
      ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
        { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
      ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)),
  { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
q : RingPreordering R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier) q)
⊢ { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    q
have mk : ∀ (toSubsemiring_1 : Subsemiring R) (mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier)
  (neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set R)
      ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
        { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
      ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
        { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
          neg_one_notMem' := neg_one_notMem'_1 })),
  { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1, neg_one_notMem' := neg_one_notMem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
toSubsemiring : Subsemiring R
mem_of_isSquare' : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring.carrier
neg_one_notMem' : -1 ∉ toSubsemiring.carrier
toSubsemiring_1 : Subsemiring R
mem_of_isSquare'_1 : ∀ {x : R} (hx : IsSquare x), x ∈ toSubsemiring_1.carrier
neg_one_notMem'_1 : -1 ∉ toSubsemiring_1.carrier
h :
  Eq.{u_1 + 1} (α := Set R)
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' })
    ((fun (P : RingPreordering R) ↦ (↑P : Subsemiring R).carrier)
      { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1,
        neg_one_notMem' := neg_one_notMem'_1 })
⊢ { toSubsemiring := toSubsemiring, mem_of_isSquare' := @mem_of_isSquare', neg_one_notMem' := neg_one_notMem' :
      RingPreordering R } =
    { toSubsemiring := toSubsemiring_1, mem_of_isSquare' := @mem_of_isSquare'_1, neg_one_notMem' := neg_one_notMem'_1 }
have mk : toSubsemiring = toSubsemiring_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
A B : RingPreordering R
h : (↑A : Subsemiring R) = (↑B : Subsemiring R)
⊢ A = B
have carrier : ∀ (x : R), x ∈ (↑A : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Ordering.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
A B : RingPreordering R
h : (↑A : Subsemiring R) = (↑B : Subsemiring R)
x : R
⊢ x ∈ (↑A : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier
have carrier : x ∈ (↑B : Subsemiring R).carrier ↔ x ∈ (↑B : Subsemiring R).carrier
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
      (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
        a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)
have simp : a * (a * (a * a ^ n)) +
      ((↑n : R) * (b * (a * (a * a ^ n))) + (b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + b * (a * (a * a ^ n)))) +
    ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n)) +
          ((↑n : R) * (b * (b * (a * a ^ n))) + b * (b * (a * a ^ n))) +
        ((↑n : R) * (b * (b * (b * a ^ n))) + b * (b * (b * a ^ n))) +
      b * (b * (a * a ^ n))) =
  a * (a * (a * a ^ n)) + b * (a * (a * a ^ n)) + (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n))) +
    ((↑n : R) * (b * (a * (a * a ^ n))) + (↑n : R) * (b * (b * (a * a ^ n))) +
        ((↑n : R) * (b * (b * (a * a ^ n))) + (↑n : R) * (b * (b * (b * a ^ n)))) +
      (b * (a * (a * a ^ n)) + b * (b * (a * a ^ n)) + (b * (b * (a * a ^ n)) + b * (b * (b * a ^ n)))))
Tactic: simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b) ≤
    HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1)
have hbc : a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b ≤ (a + b) ^ (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 3 - 1) * b ≤ (a + b) ^ (n + 3)
have _ : a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
    (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
      a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
  HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)
Tactic: calc
      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
_ :
  a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
      (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
        a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 3 - 1) * b ≤ (a + b) ^ (n + 3)
have _₁ : HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b) ≤
  HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1)
Tactic: calc
      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ HPow.hPow (β := ℕ) b 2
Hsq' : 0 ≤ HPow.hPow (β := ℕ) (a + b) 2
H : 0 ≤ 2 * a + b
n : ℕ
_ :
  a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 2) * b +
      (HAdd.hAdd (α := R) (↑n : R) 1 * (HPow.hPow (β := ℕ) b 2 * (2 * a + b) * a ^ n) +
        a ^ (n + 1) * HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b)
_₁ :
  HPow.hPow (β := ℕ) (a + b) 2 * (a ^ (n + 1) + (↑(n + 1) : R) * a ^ n * b) ≤
    HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1)
⊢ a ^ (n + 3) + (↑(n + 3) : R) * a ^ (n + 3 - 1) * b ≤ (a + b) ^ (n + 3)
have _₂ : HPow.hPow (β := ℕ) (a + b) 2 * (a + b) ^ (n + 1) = (a + b) ^ (n + 3)
Tactic: calc
      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -2 ≤ a - 1
have rwa : -HAdd.hAdd (α := R) 1 1 ≤ a - 1
Tactic: rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
rwa : -HAdd.hAdd (α := R) 1 1 ≤ a - 1
⊢ -2 ≤ a - 1
have rwa₁ : HAdd.hAdd (α := R) (-1) (-1) ≤ a - 1
Tactic: rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
rwa : -HAdd.hAdd (α := R) 1 1 ≤ a - 1
rwa₁ : HAdd.hAdd (α := R) (-1) (-1) ≤ a - 1
⊢ -2 ≤ a - 1
have rwa₂ : HSub.hSub (α := R) (-1) 1 ≤ a - 1
Tactic: rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Pow (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ 1 + (↑n : R) * (a - 1) ≤ a ^ n
have this : -2 ≤ a - 1
Tactic: have : -2 ≤ a - 1 := by
    rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
⊢ IsUnit x ↔ Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
have rw : ¬IsUnit x ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
Tactic: rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
rw : ¬IsUnit x ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
⊢ IsUnit x ↔ Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
have rw₁ : LT.lt (α := ArchimedeanClass K) 0 (mk (↑x : K)) ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
Tactic: rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
rw : ¬IsUnit x ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₁ : LT.lt (α := ArchimedeanClass K) 0 (mk (↑x : K)) ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
⊢ IsUnit x ↔ Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
have rw₂ : ¬LE.le (α := ArchimedeanClass K) (mk (↑x : K)) 0 ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
Tactic: rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : FiniteElement K
rw : ¬IsUnit x ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₁ : LT.lt (α := ArchimedeanClass K) 0 (mk (↑x : K)) ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
rw₂ : ¬LE.le (α := ArchimedeanClass K) (mk (↑x : K)) 0 ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
⊢ IsUnit x ↔ Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
have rw₃ : ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0 ↔ ¬Eq (α := ArchimedeanClass K) (mk (↑x : K)) 0
Tactic: rw [← not_iff_not, not_isUnit_iff_mk_pos, lt_iff_not_ge, x.2.ge_iff_eq']
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
⊢ ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)
have obtain : ∀ (n : ℕ)
  (hn :
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
          ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
      HSMul.hSMul (β := K) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
              ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
          K)),
  ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)
Tactic: obtain ⟨n, hn⟩ := x.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x : FiniteElement K
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
        ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) (↑x : K) : ArchimedeanOrder K)| ≤
    HSMul.hSMul (β := K) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder K) → K)
            ((ArchimedeanOrder.of : (a : K) → ArchimedeanOrder K) 1 : ArchimedeanOrder K)| :
        K)
⊢ ∃ (n : ℕ), x ≤ (↑n : FiniteElement K)
have refine : |x| ≤ (↑n : FiniteElement K)
Tactic: refine ⟨n, (le_abs_self x).trans ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x y : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
⊢ ∀ (x : Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))),
    Set.OrdConnected (α := FiniteElement K)
      (Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})
have refine : ∀ (x : Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
  ⦃x_1 : FiniteElement K⦄
  (hx :
    Membership.mem (γ := Set (FiniteElement K))
      (Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})
      x_1)
  ⦃y : FiniteElement K⦄
  (hy :
    Membership.mem (γ := Set (FiniteElement K))
      (Set.preimage (β :=
        Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
        (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x})
      y),
  Set.Icc x_1 y ⊆
    Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {x}
Tactic: refine fun x ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    y
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
⊢ Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    z
have this : x ≤ y
Tactic: have := hxz.trans hzy
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy :
  Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    y
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ Membership.mem (γ := Set (FiniteElement K))
    (Set.preimage (β :=
      Quotient (α := FiniteElement K) (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))))
      (Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K)))) {⟦x⟧})
    z
have rw : ∀ (hy : LT.lt (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))) ⦃z : FiniteElement K⦄ (hxz : x ≤ z) (hzy : z ≤ y)
  (this : x ≤ y), LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))
Tactic: rw [Set.mem_preimage, Set.mem_singleton_iff, Quotient.eq, Submodule.quotientRel_def,
    IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, FiniteElement.not_isUnit_iff_mk_pos] at hy ⊢
Cleared hypotheses: hy, z, hxz, hzy, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))
have apply : Membership.mem (γ := Set K) (Set.Ici 0) (↑(z - x) : K)
Tactic: apply hy.trans_le (mk_antitoneOn _ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x_1 y_1 : K
R : Type u_2
inst_3 : LinearOrder R
inst_4 : CommRing R
inst_5 : IsStrictOrderedRing R
inst_6 : Archimedean R
x y : FiniteElement K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk (↑(y - x) : K))
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
apply : Membership.mem (γ := Set K) (Set.Ici 0) (↑(z - x) : K)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (↑(z - x) : K))
have apply₁ : Membership.mem (γ := Set K) (Set.Ici 0) (↑(y - x) : K)
Tactic: apply hy.trans_le (mk_antitoneOn _ _ _)