internlm/Lean-Github huggingface dataset:
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))
Tactic:
unfold mergeNodes
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le
    (Heap.heap
      (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
      else
        if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
        else
          let merged := combine le h₁ h₂;
          let r := merged.rank;
          if (r != hRank t₁) = true then
            if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
          else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le
    (Heap.heap
      (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
      else
        if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
        else
          let merged := combine le h₁ h₂;
          let r := merged.rank;
          if (r != hRank t₁) = true then
            if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
          else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
split
Proof state after:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : h₁.rank < h₂.rank
⊢ IsMinHeap le (Heap.heap (h₁ :: mergeNodes le t₁ (h₂ :: t₂)))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Theorem: project.IsMinHeap_merge
Proof state before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : h₁.rank < h₂.rank
⊢ IsMinHeap le (Heap.heap (h₁ :: mergeNodes le t₁ (h₂ :: t₂)))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
. constructor
  . cases hxs
    assumption
  . cases hxs
    apply IsMinHeap_merge <;> assumption
Proof state after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Theorem: project.IsMinHeap_merge
Proof state before:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
Tactic:
. split
  . constructor
    . cases hys
      assumption
    . cases hys
      apply IsMinHeap_merge <;> assumption
  . dsimp
    split
    . split
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
      . apply IsMinHeap_merge
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hxs
            assumption
        . cases hys
          assumption
    . split
      . apply IsMinHeap_merge
        . cases hxs
          assumption
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hys
            assumption
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption 
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
Proof state after:
no goals
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
_x✝ : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))
a✝¹ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        _x✝ →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hx hy : List (HeapNodeAux α (Heap α))
a✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := hx, snd := hy } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
x✝ :
  ∀ (y : (_ : List (HeapNodeAux α (Heap α))) ×' List (HeapNodeAux α (Heap α))),
    (invImage (fun a ↦ PSigma.casesOn a fun hx snd ↦ List.length hx + List.length snd) instWellFoundedRelation).1 y
        { fst := h₁ :: t₁, snd := h₂ :: t₂ } →
      IsMinHeap le (Heap.heap y.1) → IsMinHeap le (Heap.heap y.2) → IsMinHeap le (Heap.heap (mergeNodes le y.1 y.2))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝³ : ¬h₁.rank < h₂.rank
h✝² : ¬h₂.rank < h₁.rank
h✝¹ : ¬((combine le h₁ h₂).rank != hRank t₁) = true
h✝ : ¬((combine le h₁ h₂).rank != hRank t₂) = true
⊢ List.length t₁ + List.length t₂ < Nat.succ (List.length t₁) + Nat.succ (List.length t₂)
Tactic:
simp_arith [*]
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_subst
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
⊢ p₁ ≃ p₂ → abs p₁ ≃ abs p₂
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
x✝ : p₁ ≃ p₂
⊢ abs p₁ ≃ abs p₂
Theorem: Lean4Axiomatic.Rational.abs_subst
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
x✝ : p₁ ≃ p₂
⊢ abs p₁ ≃ abs p₂
Tactic:
calc
  abs p₁      ≃ _ := abs_sgn
  p₁ * sgn p₁ ≃ _ := mul_substL ‹p₁ ≃ p₂›
  p₂ * sgn p₁ ≃ _ := mul_substR (from_integer_subst (sgn_subst ‹p₁ ≃ p₂›))
  p₂ * sgn p₂ ≃ _ := eqv_symm abs_sgn
  abs p₂      ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≃ 0 ↔ p ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≃ 0 → p ≃ 0

case mpr
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ p ≃ 0 → abs p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≃ 0 → p ≃ 0
Tactic:
case mp =>
  intro (_ : abs p ≃ 0)
  show p ≃ 0
  have : p * sgn p ≃ 0 := AA.eqv_substL abs_sgn ‹abs p ≃ 0›
  have : p ≃ 0 ∨ (sgn p : ℚ) ≃ 0 := mul_split_zero.mp this
  match this with
  | Or.inl (_ : p ≃ 0) =>
    exact ‹p ≃ 0›
  | Or.inr (_ : (sgn p : ℚ) ≃ 0) =>
    have : sgn p ≃ 0 := from_integer_inject ‹(sgn p : ℚ) ≃ 0›
    have : p ≃ 0 := sgn_zero.mpr this
    exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ p ≃ 0 → abs p ≃ 0
Tactic:
case mpr =>
  intro (_ : p ≃ 0)
  show abs p ≃ 0
  calc
    abs p           ≃ _ := abs_sgn
    p * sgn p       ≃ _ := mul_substL ‹p ≃ 0›
    (0 : ℚ) * sgn p ≃ _ := mul_absorbL
    0               ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ abs p ≃ 0 → p ≃ 0
Tactic:
intro (_ : abs p ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
⊢ p ≃ 0
Tactic:
have : p * sgn p ≃ 0 := AA.eqv_substL abs_sgn ‹abs p ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this : p * from_integer (sgn p) ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this : p * from_integer (sgn p) ≃ 0
⊢ p ≃ 0
Tactic:
have : p ≃ 0 ∨ (sgn p : ℚ) ≃ 0 := mul_split_zero.mp this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝ : p * from_integer (sgn p) ≃ 0
this : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝ : p * from_integer (sgn p) ≃ 0
this : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
⊢ p ≃ 0
Tactic:
match this with
| Or.inl (_ : p ≃ 0) =>
  exact ‹p ≃ 0›
| Or.inr (_ : (sgn p : ℚ) ≃ 0) =>
  have : sgn p ≃ 0 := from_integer_inject ‹(sgn p : ℚ) ≃ 0›
  have : p ≃ 0 := sgn_zero.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝ : p * from_integer (sgn p) ≃ 0
this : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : p ≃ 0
⊢ p ≃ 0
Tactic:
exact ‹p ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝ : p * from_integer (sgn p) ≃ 0
this : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : from_integer (sgn p) ≃ 0
⊢ p ≃ 0
Tactic:
have : sgn p ≃ 0 := from_integer_inject ‹(sgn p : ℚ) ≃ 0›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝¹ : p * from_integer (sgn p) ≃ 0
this✝ : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : from_integer (sgn p) ≃ 0
this : sgn p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝¹ : p * from_integer (sgn p) ≃ 0
this✝ : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : from_integer (sgn p) ≃ 0
this : sgn p ≃ 0
⊢ p ≃ 0
Tactic:
have : p ≃ 0 := sgn_zero.mpr this
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝² : p * from_integer (sgn p) ≃ 0
this✝¹ : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : from_integer (sgn p) ≃ 0
this✝ : sgn p ≃ 0
this : p ≃ 0
⊢ p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : abs p ≃ 0
this✝² : p * from_integer (sgn p) ≃ 0
this✝¹ : p ≃ 0 ∨ from_integer (sgn p) ≃ 0
h✝ : from_integer (sgn p) ≃ 0
this✝ : sgn p ≃ 0
this : p ≃ 0
⊢ p ≃ 0
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ p ≃ 0 → abs p ≃ 0
Tactic:
intro (_ : p ≃ 0)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : p ≃ 0
⊢ abs p ≃ 0
Theorem: Lean4Axiomatic.Rational.abs_zero
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : p ≃ 0
⊢ abs p ≃ 0
Tactic:
calc
  abs p           ≃ _ := abs_sgn
  p * sgn p       ≃ _ := mul_substL ‹p ≃ 0›
  (0 : ℚ) * sgn p ≃ _ := mul_absorbL
  0               ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_positive
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ sgn p ≃ 1 → abs p ≃ p
Tactic:
intro (_ : sgn p ≃ 1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ 1
⊢ abs p ≃ p
Theorem: Lean4Axiomatic.Rational.abs_positive
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ 1
⊢ abs p ≃ p
Tactic:
calc
  _ ≃ abs p     := eqv_refl
  _ ≃ p * sgn p := abs_sgn
  _ ≃ p * 1     := mul_substR (from_integer_subst ‹sgn p ≃ 1›)
  _ ≃ p         := mul_identR
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.abs_negative
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
⊢ sgn p ≃ -1 → abs p ≃ -p
Tactic:
intro (_ : sgn p ≃ -1)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
⊢ abs p ≃ -p
Theorem: Lean4Axiomatic.Rational.abs_negative
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
⊢ abs p ≃ -p
Tactic:
have : (sgn p : ℚ) ≃ -1 := calc
  _ ≃ (sgn p : ℚ)    := eqv_refl
  _ ≃ ((-1 : ℤ) : ℚ) := from_integer_subst ‹sgn p ≃ -1›
  _ ≃ -((1 : ℤ) : ℚ) := neg_compat_from_integer
  _ ≃ -1             := eqv_refl
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p : ℚ
x✝ : sgn p ≃ -1
this : from_integer (sgn p) ≃ -1
⊢ abs p ≃ -p