awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
pos :
  (match (motive := SignType → Fin 3) SignType.pos * zero with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) zero with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.pos * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have pos₁ : (match (motive := SignType → Fin 3) SignType.pos * neg with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.pos with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) neg with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
pos :
  (match (motive := SignType → Fin 3) SignType.pos * zero with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) zero with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
pos₁ :
  (match (motive := SignType → Fin 3) SignType.pos * neg with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.pos * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have pos₂ : (match (motive := SignType → Fin 3) SignType.pos * SignType.pos with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.pos with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) SignType.pos with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
⊢ f (↑s : α) = (↑s : β)
have zero : f (↑zero : α) = (↑zero : β)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
zero : f (↑SignType.zero : α) = (↑SignType.zero : β)
⊢ f (↑s : α) = (↑s : β)
have neg : f (↑neg : α) = (↑neg : β)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
zero : f (↑SignType.zero : α) = (↑SignType.zero : β)
neg : f (↑SignType.neg : α) = (↑SignType.neg : β)
⊢ f (↑s : α) = (↑s : β)
have pos : f (↑pos : α) = (↑pos : β)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (↑s : α) : β) ((↑s : β) : β)
have h₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
Tactic: apply map_cast'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
h₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (↑s : α) : β) ((↑s : β) : β)
have h₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: apply map_cast'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
h₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
h₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (↑s : α) : β) ((↑s : β) : β)
have h₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (-1) : β) (-1 : β)
Tactic: apply map_cast'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
s : SignType
⊢ Eq.{u_2 + 1} (α := α) (↑(-s) : α) (-(↑s : α))
have zero : Eq.{u_2 + 1} (α := α) (↑(-zero) : α) (-(↑zero : α))
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
s : SignType
zero : Eq.{u_2 + 1} (α := α) (↑(-SignType.zero) : α) (-(↑SignType.zero : α))
⊢ Eq.{u_2 + 1} (α := α) (↑(-s) : α) (-(↑s : α))
have neg : Eq.{u_2 + 1} (α := α) (↑(-neg) : α) (-(↑neg : α))
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
s : SignType
zero : Eq.{u_2 + 1} (α := α) (↑(-SignType.zero) : α) (-(↑SignType.zero : α))
neg : Eq.{u_2 + 1} (α := α) (↑(-SignType.neg) : α) (-(↑SignType.neg : α))
⊢ Eq.{u_2 + 1} (α := α) (↑(-s) : α) (-(↑s : α))
have pos : Eq.{u_2 + 1} (α := α) (↑(-pos) : α) (-(↑pos : α))
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have neg₁ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : ¬b < 0), LE.le (α := SignType) (-1) 0
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
neg₁ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : ¬b < 0), LE.le (α := SignType) (-1) 0
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos₄ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : 0 < b), LE.le (α := SignType) 0 1
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
neg₁ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : ¬b < 0), LE.le (α := SignType) (-1) 0
pos₄ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : 0 < b), LE.le (α := SignType) 0 1
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have pos₅ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 0 (-1)
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
neg₁ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : ¬b < 0), LE.le (α := SignType) (-1) 0
pos₄ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : 0 < b), LE.le (α := SignType) 0 1
pos₅ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 0 (-1)
⊢ LE.le (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (if 0 < b then 1 else if b < 0 then -1 else 0)
have neg₂ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 0 0
Tactic: split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : 0 < a
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
have rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 1
Tactic: rwa [sign_apply, if_pos]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : 0 < a
rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 1
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
have rwa₁ : Eq (α := SignType) 1 1
Tactic: rwa [sign_apply, if_pos]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : a < 0
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
have rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
Tactic: rwa [sign_apply, if_neg <| asymm ha, if_pos]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : a < 0
rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
have rwa₁ : Eq (α := SignType) (if a < 0 then -1 else 0) (-1)
Tactic: rwa [sign_apply, if_neg <| asymm ha, if_pos]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : a < 0
rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
rwa₁ : Eq (α := SignType) (if a < 0 then -1 else 0) (-1)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
have rwa₂ : Eq (α := SignType) (-1) (-1)
Tactic: rwa [sign_apply, if_neg <| asymm ha, if_pos]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType) ↔ 0 < a
have refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)), 0 < a
Tactic: refine ⟨fun h => ?_, fun h => sign_pos h⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
⊢ 0 < a
have by_contra : ∀ (hn : ¬0 < a), False
Tactic: by_contra hn
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hn : ¬0 < a
⊢ False
have h₁ : Eq (α := SignType) (if a < 0 then -1 else 0) 1
Tactic: rw [sign_apply, if_neg hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType) ↔ a < 0
have refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)), a < 0
Tactic: refine ⟨fun h => ?_, fun h => sign_neg h⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
⊢ a < 0
have h₁ : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
Tactic: rw [sign_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
⊢ a < 0
have h₁ : ¬0 < a
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
h₁ : ¬0 < a
h₂ : a < 0
⊢ a < 0
have h₃ : Eq (α := SignType) (-1) (-1)
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a = 0
have refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)), a = 0
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
⊢ a = 0
have h₁ : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
Tactic: rw [sign_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
⊢ a = 0
have h_1 : ¬0 < a
Tactic: split_ifs at h with h_1 h_2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
h_1 : ¬0 < a
⊢ a = 0
have h_2 : ¬a < 0
Tactic: split_ifs at h with h_1 h_2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (hypothesis)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0
have h₁ : Eq (α := SignType) 0 0
Tactic: split_ifs at h with h_1 h_2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
have inl : ∀ (h : 0 < a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
Tactic: rcases lt_trichotomy 0 a with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
have inr : ∀ (h : 0 = a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
Tactic: rcases lt_trichotomy 0 a with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
inr : ∀ (h : 0 = a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
have inr₁ : ∀ (h : a < 0), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
Tactic: rcases lt_trichotomy 0 a with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
have inl : ∀ (h : 0 < a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
Tactic: rcases lt_trichotomy 0 a with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
have inr : ∀ (h : 0 = a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
Tactic: rcases lt_trichotomy 0 a with (h | h | h)
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
inr : ∀ (h : 0 = a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
have inr₁ : ∀ (h : a < 0), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
Tactic: rcases lt_trichotomy 0 a with (h | h | h)