internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ (if true = true then p else q) ≤ p
Tactic:
show p ≤ p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ p
Tactic:
exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ (if false = true then p else q) ≤ p
Tactic:
show q ≤ p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ p
Tactic:
have : ¬(p < q) := ofBoolUsing_eq_false eq
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this : ¬p < q
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this : ¬p < q
⊢ q ≤ p
Tactic:
have : sgn (p - q) ≄ -1 := mt lt_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this✝ : ¬p < q
this : sgn (p - q) ≄ -1
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this✝ : ¬p < q
this : sgn (p - q) ≄ -1
⊢ q ≤ p
Tactic:
have : q ≤ p := ge_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this✝¹ : ¬p < q
this✝ : sgn (p - q) ≄ -1
this : q ≤ p
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
this✝¹ : ¬p < q
this✝ : sgn (p - q) ≄ -1
this : q ≤ p
⊢ q ≤ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ Ordered.min p q ≤ q
Tactic:
show (if decide (p < q) then p else q) ≤ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ q
Tactic:
match eq : decide (p < q) with
| true =>
  show (if true then p else q) ≤ q
  show p ≤ q
  have : p < q := ofBoolUsing_eq_true eq
  have : p ≤ q := le_cases.mpr (Or.inl this)
  exact this
| false =>
  show (if false then p else q) ≤ q
  show q ≤ q
  exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ (if true = true then p else q) ≤ q
Tactic:
show p ≤ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ q
Tactic:
have : p < q := ofBoolUsing_eq_true eq
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this : p < q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this : p < q
⊢ p ≤ q
Tactic:
have : p ≤ q := le_cases.mpr (Or.inl this)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this✝ : p < q
this : p ≤ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this✝ : p < q
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ (if false = true then p else q) ≤ q
Tactic:
show q ≤ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ q
Tactic:
exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
Tactic:
show
  (if decide (p > q) then p else q) ≃ p ∨
  (if decide (p > q) then p else q) ≃ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p > q) = true then p else q) ≃ p ∨ (if decide (p > q) = true then p else q) ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p > q) = true then p else q) ≃ p ∨ (if decide (p > q) = true then p else q) ≃ q
Tactic:
match decide (p > q) with
| true =>
  apply Or.inl
  show (if true then p else q) ≃ p
  show p ≃ p
  exact eqv_refl
| false =>
  apply Or.inr
  show (if false then p else q) ≃ q
  show q ≃ q
  exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p ∨ (if true = true then p else q) ≃ q
Tactic:
apply Or.inl
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p
Tactic:
show p ≃ p
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ p
Tactic:
exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ p ∨ (if false = true then p else q) ≃ q
Tactic:
apply Or.inr
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ q
Tactic:
show q ≃ q
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≃ q
Tactic:
exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ Ordered.max p q
Tactic:
show p ≤ (if decide (p > q) then p else q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ if decide (p > q) = true then p else q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≤ if decide (p > q) = true then p else q
Tactic:
match eq : decide (p > q) with
| true =>
  show p ≤ (if true then p else q)
  show p ≤ p
  exact le_refl
| false =>
  show p ≤ (if false then p else q)
  show p ≤ q
  have : ¬(p > q) := ofBoolUsing_eq_false eq
  have : sgn (p - q) ≄ 1 := mt gt_sgn.mpr this
  have : p ≤ q := le_sgn.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ p ≤ if true = true then p else q
Tactic:
show p ≤ p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ p ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ p ≤ p
Tactic:
exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ p ≤ if false = true then p else q
Tactic:
show p ≤ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ p ≤ q
Tactic:
have : ¬(p > q) := ofBoolUsing_eq_false eq
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this : ¬p > q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this : ¬p > q
⊢ p ≤ q
Tactic:
have : sgn (p - q) ≄ 1 := mt gt_sgn.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this✝ : ¬p > q
this : sgn (p - q) ≄ 1
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this✝ : ¬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✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this✝¹ : ¬p > q
this✝ : sgn (p - q) ≄ 1
this : p ≤ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
this✝¹ : ¬p > q
this✝ : sgn (p - q) ≄ 1
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≤ Ordered.max p q
Tactic:
show q ≤ (if decide (p > q) then p else q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≤ if decide (p > q) = true then p else q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≤ if decide (p > q) = true then p else q
Tactic:
match eq : decide (p > q) with
| true =>
  show q ≤ (if true then p else q)
  show q ≤ p
  have : p > q := ofBoolUsing_eq_true eq
  have : q ≤ p := le_cases.mpr (Or.inl ‹q < p›)
  exact this
| false =>
  show q ≤ (if false then p else q)
  show q ≤ q
  exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ q ≤ if true = true then p else q
Tactic:
show q ≤ p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
⊢ q ≤ p
Tactic:
have : p > q := ofBoolUsing_eq_true eq
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
this : p > q
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
this : p > q
⊢ q ≤ p
Tactic:
have : q ≤ p := le_cases.mpr (Or.inl ‹q < p›)
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
this✝ : p > q
this : q ≤ p
⊢ q ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = true
this✝ : p > q
this : q ≤ p
⊢ q ≤ p
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ q ≤ if false = true then p else q
Tactic:
show q ≤ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ q ≤ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.max_leR
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p > q) = false
⊢ q ≤ q
Tactic:
exact le_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let motive (z : ℤ) : Prop := ∃ (n m : ℕ), z ≃ n - m
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let msubst {x₁ x₂ : ℤ} : x₁ ≃ x₂ → motive x₁ → motive x₂ := by
  intro (_ : x₁ ≃ x₂) (_ : motive x₁)
  show motive x₂
  have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : x₁ ≃ n - m)) :=
    ‹motive x₁›
  have : x₂ ≃ n - m := calc
    _ = x₂    := rfl
    _ ≃ x₁    := Rel.symm ‹x₁ ≃ x₂›
    _ ≃ n - m := ‹x₁ ≃ n - m›
  have : ∃ (n m : ℕ), x₂ ≃ n - m := Exists.intro n (Exists.intro m this)
  have : motive x₂ := this
  exact this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m