internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : sgn (p - q) ≃ 1
x✝ : p ≤ q
⊢ False
Tactic:
have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : sgn (p - q) ≃ 1
x✝ : p ≤ q
this : sgn (p - q) ≄ 1
⊢ False
Theorem: Lean4Axiomatic.Rational.neg_le_sgn
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : sgn (p - q) ≃ 1
x✝ : p ≤ q
this : sgn (p - q) ≄ 1
⊢ False
Tactic:
exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
⊢ p ≮ p
Tactic:
intro (_ : p < p)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
⊢ False
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
⊢ False
Tactic:
let TriSame := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
⊢ False
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
⊢ False
Tactic:
have : p ≃ p := eqv_refl
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this : p ≃ p
⊢ False
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this : p ≃ p
⊢ False
Tactic:
have : TriSame := AA.TwoOfThree.oneAndTwo ‹p < p› ‹p ≃ p›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this✝ : p ≃ p
this : TriSame
⊢ False
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this✝ : p ≃ p
this : TriSame
⊢ False
Tactic:
have : ¬TriSame := (order_trichotomy p p).atMostOne
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this✝¹ : p ≃ p
this✝ : TriSame
this : ¬TriSame
⊢ False
Theorem: Lean4Axiomatic.Rational.lt_irrefl
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p : ℚ
x✝ : p < p
TriSame : Prop := AA.TwoOfThree (p < p) (p ≃ p) (p > p)
this✝¹ : p ≃ p
this✝ : TriSame
this : ¬TriSame
⊢ False
Tactic:
exact absurd ‹TriSame› ‹¬TriSame›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ q ↔ p < q ∨ p ≃ q
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q

case mpr
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p < q ∨ p ≃ q → p ≤ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q
Tactic:
case mp =>
  intro (_ : p ≤ q)
  show p < q ∨ p ≃ q
  have : AA.OneOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atLeastOne
  match this with
  | AA.OneOfThree.first (_ : p < q) =>
    have : p < q ∨ p ≃ q := Or.inl ‹p < q›
    exact this
  | AA.OneOfThree.second (_ : p ≃ q) =>
    have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
    exact this
  | AA.OneOfThree.third (_ : p > q) =>
    have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
    have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
    exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p < q ∨ p ≃ q → p ≤ q
Tactic:
case mpr =>
  intro (_ : p < q ∨ p ≃ q)
  show p ≤ q
  have : sgn (p - q) ≄ 1 := by
    intro (_ : sgn (p - q) ≃ 1)
    show False
    have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
    have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      (order_trichotomy p q).atMostOne
    match ‹p < q ∨ p ≃ q› with
    | Or.inl (_ : p < q) =>
      have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
        AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
      exact absurd two not_two
    | Or.inr (_ : p ≃ q) =>
      have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
        AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
      exact absurd two not_two
  have : p ≤ q := le_sgn.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ q → p < q ∨ p ≃ q
Tactic:
intro (_ : p ≤ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
⊢ p < q ∨ p ≃ q
Tactic:
have : AA.OneOfThree (p < q) (p ≃ q) (p > q) :=
  (order_trichotomy p q).atLeastOne
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
⊢ p < q ∨ p ≃ q
Tactic:
match this with
| AA.OneOfThree.first (_ : p < q) =>
  have : p < q ∨ p ≃ q := Or.inl ‹p < q›
  exact this
| AA.OneOfThree.second (_ : p ≃ q) =>
  have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
  exact this
| AA.OneOfThree.third (_ : p > q) =>
  have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
  have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
  exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
⊢ p < q ∨ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := Or.inl ‹p < q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
a✝ : p < q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := Or.inr ‹p ≃ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
b✝ : p ≃ q
this : p < q ∨ p ≃ q
⊢ p < q ∨ p ≃ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
⊢ p < q ∨ p ≃ q
Tactic:
have : sgn (p - q) ≃ 1 := gt_sgn.mp ‹p > q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this : sgn (p - q) ≃ 1
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this : sgn (p - q) ≃ 1
⊢ p < q ∨ p ≃ q
Tactic:
have : sgn (p - q) ≄ 1 := le_sgn.mp ‹p ≤ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝¹ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this✝ : sgn (p - q) ≃ 1
this : sgn (p - q) ≄ 1
⊢ p < q ∨ p ≃ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p ≤ q
this✝¹ : AA.OneOfThree (p < q) (p ≃ q) (p > q)
c✝ : p > q
this✝ : sgn (p - q) ≃ 1
this : sgn (p - q) ≄ 1
⊢ p < q ∨ p ≃ q
Tactic:
exact absurd ‹sgn (p - q) ≃ 1› ‹sgn (p - q) ≄ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p < q ∨ p ≃ q → p ≤ q
Tactic:
intro (_ : p < q ∨ p ≃ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
⊢ p ≤ q
Tactic:
have : sgn (p - q) ≄ 1 := by
  intro (_ : sgn (p - q) ≃ 1)
  show False
  have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
  have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    (order_trichotomy p q).atMostOne
  match ‹p < q ∨ p ≃ q› with
  | Or.inl (_ : p < q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
    exact absurd two not_two
  | Or.inr (_ : p ≃ q) =>
    have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
      AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
    exact absurd two not_two
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
this : sgn (p - q) ≄ 1
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
this : sgn (p - q) ≄ 1
⊢ p ≤ q
Tactic:
have : p ≤ q := le_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
this✝ : sgn (p - q) ≄ 1
this : p ≤ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
this✝ : sgn (p - q) ≄ 1
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝ : p < q ∨ p ≃ q
⊢ sgn (p - q) ≄ 1
Tactic:
intro (_ : sgn (p - q) ≃ 1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
⊢ False
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
⊢ False
Tactic:
have : p > q := gt_sgn.mpr ‹sgn (p - q) ≃ 1›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
⊢ False
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
⊢ False
Tactic:
have not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  (order_trichotomy p q).atMostOne
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
match ‹p < q ∨ p ≃ q› with
| Or.inl (_ : p < q) =>
  have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
  exact absurd two not_two
| Or.inr (_ : p ≃ q) =>
  have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
    AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
  exact absurd two not_two
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
⊢ False
Tactic:
have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p < q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
exact absurd two not_two
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
⊢ False
Tactic:
have two : AA.TwoOfThree (p < q) (p ≃ q) (p > q) :=
  AA.TwoOfThree.twoAndThree ‹p ≃ q› ‹p > q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Theorem: Lean4Axiomatic.Rational.le_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q : ℚ
x✝¹ : p < q ∨ p ≃ q
x✝ : sgn (p - q) ≃ 1
this : p > q
not_two : ¬AA.TwoOfThree (p < q) (p ≃ q) (p > q)
h✝ : p ≃ q
two : AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ False
Tactic:
exact absurd two not_two
Proof state after:
no goals