Theorem: Lean4Axiomatic.Rational.min_comm (Lean4Axiomatic/Rational/MinMax.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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have opposite_eqv
    {r s x y : ℚ} : min r s ≃ x → min s r ≃ y → min r s ≤ y → min s r ≤ x →
    min r s ≃ min s r
    := by
  intro (_ : min r s ≃ x) (_ : min s r ≃ y)
  intro (_ : min r s ≤ y) (_ : min s r ≤ x)
  show min r s ≃ min s r
  have : x ≤ y := le_substL_eqv ‹min r s ≃ x› ‹min r s ≤ y›
  have : y ≤ x := le_substL_eqv ‹min s r ≃ y› ‹min s r ≤ x›
  have : x ≃ y := le_antisymm ‹x ≤ y› ‹y ≤ x›
  have : min r s ≃ min s r := calc
    _ ≃ min r s := eqv_refl
    _ ≃ x       := ‹min r s ≃ x›
    _ ≃ y       := ‹x ≃ y›
    _ ≃ min s r := eqv_symm ‹min s r ≃ y›
  exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have pq_cases : min p q ≃ p ∨ min p q ≃ q := min_cases
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have qp_cases : min q p ≃ q ∨ min q p ≃ p := min_cases
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
match pq_cases with
| Or.inl (_ : min p q ≃ p) =>
  match qp_cases with
  | Or.inl (_ : min q p ≃ q) =>
    have : min p q ≤ q := min_leR
    have : min q p ≤ p := min_leR
    have : min p q ≃ min q p :=
      opposite_eqv ‹min p q ≃ p› ‹min q p ≃ q› ‹min p q ≤ q› ‹min q p ≤ p›
    exact this
  | Or.inr (_ : min q p ≃ p) =>
    have : min p q ≃ min q p := calc
      _ ≃ min p q := eqv_refl
      _ ≃ p       := ‹min p q ≃ p›
      _ ≃ min q p := eqv_symm ‹min q p ≃ p›
    exact this
| Or.inr (_ : min p q ≃ q) =>
  match qp_cases with
  | Or.inl (_ : min q p ≃ q) =>
    have : min p q ≃ min q p := calc
      _ ≃ min p q := eqv_refl
      _ ≃ q       := ‹min p q ≃ q›
      _ ≃ min q p := eqv_symm ‹min q p ≃ q›
    exact this
  | Or.inr (_ : min q p ≃ p) =>
    have : min p q ≤ p := min_leL
    have : min q p ≤ q := min_leL
    have : min p q ≃ min q p :=
      opposite_eqv ‹min p q ≃ q› ‹min q p ≃ p› ‹min p q ≤ p› ‹min q p ≤ q›
    exact this
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
⊢ Ordered.min r s ≃ x →
    Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
Tactic:
intro (_ : min r s ≃ x) (_ : min s r ≃ y)
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝¹ : Ordered.min r s ≃ x
x✝ : Ordered.min s r ≃ y
⊢ Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝¹ : Ordered.min r s ≃ x
x✝ : Ordered.min s r ≃ y
⊢ Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
Tactic:
intro (_ : min r s ≤ y) (_ : min s r ≤ x)
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
⊢ Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
⊢ Ordered.min r s ≃ Ordered.min s r
Tactic:
have : x ≤ y := le_substL_eqv ‹min r s ≃ x› ‹min r s ≤ y›
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this : x ≤ y
⊢ Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this : x ≤ y
⊢ Ordered.min r s ≃ Ordered.min s r
Tactic:
have : y ≤ x := le_substL_eqv ‹min s r ≃ y› ‹min s r ≤ x›
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝ : x ≤ y
this : y ≤ x
⊢ Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝ : x ≤ y
this : y ≤ x
⊢ Ordered.min r s ≃ Ordered.min s r
Tactic:
have : x ≃ y := le_antisymm ‹x ≤ y› ‹y ≤ x›
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝¹ : x ≤ y
this✝ : y ≤ x
this : x ≃ y
⊢ Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝¹ : x ≤ y
this✝ : y ≤ x
this : x ≃ y
⊢ Ordered.min r s ≃ Ordered.min s r
Tactic:
have : min r s ≃ min s r := calc
  _ ≃ min r s := eqv_refl
  _ ≃ x       := ‹min r s ≃ x›
  _ ≃ y       := ‹x ≃ y›
  _ ≃ min s r := eqv_symm ‹min s r ≃ y›
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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝² : x ≤ y
this✝¹ : y ≤ x
this✝ : x ≃ y
this : Ordered.min r s ≃ Ordered.min s r
⊢ Ordered.min r s ≃ Ordered.min s r

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 ℚ
inst✝ : MinMax ℚ
p q r s x y : ℚ
x✝³ : Ordered.min r s ≃ x
x✝² : Ordered.min s r ≃ y
x✝¹ : Ordered.min r s ≤ y
x✝ : Ordered.min s r ≤ x
this✝² : x ≤ y
this✝¹ : y ≤ x
this✝ : x ≃ y
this : Ordered.min r s ≃ Ordered.min s r
⊢ Ordered.min r s ≃ Ordered.min s r
Tactic:
exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝ : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
match qp_cases with
| Or.inl (_ : min q p ≃ q) =>
  have : min p q ≤ q := min_leR
  have : min q p ≤ p := min_leR
  have : min p q ≃ min q p :=
    opposite_eqv ‹min p q ≃ p› ‹min q p ≃ q› ‹min p q ≤ q› ‹min q p ≤ p›
  exact this
| Or.inr (_ : min q p ≃ p) =>
  have : min p q ≃ min q p := calc
    _ ≃ min p q := eqv_refl
    _ ≃ p       := ‹min p q ≃ p›
    _ ≃ min q p := eqv_symm ‹min q p ≃ p›
  exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≤ q := min_leR
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min q p ≤ p := min_leR
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this✝ : Ordered.min p q ≤ q
this : Ordered.min q p ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this✝ : Ordered.min p q ≤ q
this : Ordered.min q p ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p :=
  opposite_eqv ‹min p q ≃ p› ‹min q p ≃ q› ‹min p q ≤ q› ‹min q p ≤ 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this✝¹ : Ordered.min p q ≤ q
this✝ : Ordered.min q p ≤ p
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ q
this✝¹ : Ordered.min p q ≤ q
this✝ : Ordered.min q p ≤ p
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p := calc
  _ ≃ min p q := eqv_refl
  _ ≃ p       := ‹min p q ≃ p›
  _ ≃ min q p := eqv_symm ‹min q p ≃ 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ p
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝ : Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
match qp_cases with
| Or.inl (_ : min q p ≃ q) =>
  have : min p q ≃ min q p := calc
    _ ≃ min p q := eqv_refl
    _ ≃ q       := ‹min p q ≃ q›
    _ ≃ min q p := eqv_symm ‹min q p ≃ q›
  exact this
| Or.inr (_ : min q p ≃ p) =>
  have : min p q ≤ p := min_leL
  have : min q p ≤ q := min_leL
  have : min p q ≃ min q p :=
    opposite_eqv ‹min p q ≃ q› ‹min q p ≃ p› ‹min p q ≤ p› ‹min q p ≤ q›
  exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p := calc
  _ ≃ min p q := eqv_refl
  _ ≃ q       := ‹min p q ≃ q›
  _ ≃ min q p := eqv_symm ‹min 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≤ p := min_leL
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this : Ordered.min p q ≤ p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min q p ≤ q := min_leL
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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝ : Ordered.min p q ≤ p
this : Ordered.min q p ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝ : Ordered.min p q ≤ p
this : Ordered.min q p ≤ q
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
have : min p q ≃ min q p :=
  opposite_eqv ‹min p q ≃ q› ‹min q p ≃ p› ‹min p q ≤ p› ‹min 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝¹ : Ordered.min p q ≤ p
this✝ : Ordered.min q p ≤ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p

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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
opposite_eqv :
  ∀ {r s x y : ℚ},
    Ordered.min r s ≃ x →
      Ordered.min s r ≃ y → Ordered.min r s ≤ y → Ordered.min s r ≤ x → Ordered.min r s ≃ Ordered.min s r
pq_cases : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
qp_cases : Ordered.min q p ≃ q ∨ Ordered.min q p ≃ p
h✝¹ : Ordered.min p q ≃ q
h✝ : Ordered.min q p ≃ p
this✝¹ : Ordered.min p q ≤ p
this✝ : Ordered.min q p ≤ q
this : Ordered.min p q ≃ Ordered.min q p
⊢ Ordered.min p q ≃ Ordered.min q p
Tactic:
exact this
State after:
no goals