Theorem: Lean4Axiomatic.Rational.le_antisymm (Lean4Axiomatic/Rational/Order.lean)

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 → q ≤ p → p ≃ q
Tactic:
intro (_ : p ≤ q) (_ : q ≤ p)
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
x✝ : q ≤ p
⊢ p ≃ q

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
x✝ : q ≤ p
⊢ p ≃ q
Tactic:
have : p < q ∨ p ≃ q := le_cases.mp ‹p ≤ q›
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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
⊢ p ≃ q

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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
⊢ p ≃ q
Tactic:
match this with
| Or.inl (_ : p < q) =>
  have : q < p ∨ q ≃ p := le_cases.mp ‹q ≤ p›
  match this with
  | Or.inl (_ : q < p) =>
    let Tri := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
    have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
    have : ¬Tri := (order_trichotomy p q).atMostOne
    exact absurd ‹Tri› ‹¬Tri›
  | Or.inr (_ : q ≃ p) =>
    exact eqv_symm ‹q ≃ p›
| Or.inr (_ : p ≃ q) =>
  exact ‹p ≃ q›
State after:
no goals

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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
h✝ : p < q
⊢ p ≃ q
Tactic:
have : q < p ∨ q ≃ p := le_cases.mp ‹q ≤ p›
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : q < p ∨ q ≃ p
⊢ p ≃ q

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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝ : p < q
this : q < p ∨ q ≃ p
⊢ p ≃ q
Tactic:
match this with
| Or.inl (_ : q < p) =>
  let Tri := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
  have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
  have : ¬Tri := (order_trichotomy p q).atMostOne
  exact absurd ‹Tri› ‹¬Tri›
| Or.inr (_ : q ≃ p) =>
  exact eqv_symm ‹q ≃ p›
State after:
no goals

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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
⊢ p ≃ q
Tactic:
let Tri := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ p ≃ q

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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
⊢ p ≃ q
Tactic:
have : Tri := AA.TwoOfThree.oneAndThree ‹p < q› ‹p > q›
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
x✝ : q ≤ p
this✝¹ : p < q ∨ p ≃ q
h✝¹ : p < q
this✝ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this : Tri
⊢ p ≃ q

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
x✝ : q ≤ p
this✝¹ : p < q ∨ p ≃ q
h✝¹ : p < q
this✝ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this : Tri
⊢ p ≃ q
Tactic:
have : ¬Tri := (order_trichotomy p q).atMostOne
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
x✝ : q ≤ p
this✝² : p < q ∨ p ≃ q
h✝¹ : p < q
this✝¹ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this✝ : Tri
this : ¬Tri
⊢ p ≃ q

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
x✝ : q ≤ p
this✝² : p < q ∨ p ≃ q
h✝¹ : p < q
this✝¹ : q < p ∨ q ≃ p
h✝ : q < p
Tri : Prop := AA.TwoOfThree (p < q) (p ≃ q) (p > q)
this✝ : Tri
this : ¬Tri
⊢ p ≃ q
Tactic:
exact absurd ‹Tri› ‹¬Tri›
State after:
no goals

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
x✝ : q ≤ p
this✝ : p < q ∨ p ≃ q
h✝¹ : p < q
this : q < p ∨ q ≃ p
h✝ : q ≃ p
⊢ p ≃ q
Tactic:
exact eqv_symm ‹q ≃ p›
State after:
no goals

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
x✝ : q ≤ p
this : p < q ∨ p ≃ q
h✝ : p ≃ q
⊢ p ≃ q
Tactic:
exact ‹p ≃ q›
State after:
no goals