awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inl : ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign a) with hsa | hsa | hsa
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
inl :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr : ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign a) with hsa | hsa | hsa
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
inl :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr₁ : ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign a) with hsa | hsa | hsa
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inl : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
inl :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inl₁ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
inl :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inl₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inl₂ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr₁ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr₂ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr₁ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
have inr₂ : ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
  Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
Tactic: rcases trichotomy (sign b) with hsb | hsb | hsb
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) (-a) : SignType) (-(sign : (a : α) → SignType) a : SignType)
have simp_rw : Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
Tactic: simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have pos : ∀ (h : a < 0) (h' : 0 < a), False
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddLeftStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have neg₁ : ∀ (h : ¬a < 0), ¬0 < a → Eq (α := SignType) 0 (-0)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) (-a) : SignType) (-(sign : (a : α) → SignType) a : SignType)
have simp_rw : Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
Tactic: simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have pos : ∀ (h : a < 0) (h' : 0 < a), False
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
α : Type u_1
inst : AddGroup α
inst_1 : Preorder α
inst_2 : DecidableLT α
inst_3 : AddRightStrictMono α
a : α
pos : ∀ (h : a < 0) (h' : 0 < a), False
neg : ∀ (h : a < 0) (h' : ¬0 < a), Eq (α := SignType) 1 (- -1)
pos₁ : ∀ (h : ¬a < 0), 0 < a → Eq (α := SignType) (-1) (-1)
⊢ Eq (α := SignType) (if a < 0 then 1 else if 0 < a then -1 else 0) (-if 0 < a then 1 else if a < 0 then -1 else 0)
have neg₁ : ∀ (h : ¬a < 0), ¬0 < a → Eq (α := SignType) 0 (-0)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
n : ℤ
⊢ n.sign = (↑((SignType.sign : (a : ℤ) → SignType) n) : ℤ)
have ofNat : (ofNat 0).sign = (↑((SignType.sign : (a : ℤ) → SignType) (ofNat 0)) : ℤ)
Tactic: obtain (n | _) | _ := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
n : ℤ
ofNat : (Int.ofNat 0).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat 0)) : ℤ)
⊢ n.sign = (↑((SignType.sign : (a : ℤ) → SignType) n) : ℤ)
have ofNat₁ : ∀ (n : ℕ), (Int.ofNat (n + 1)).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat (n + 1))) : ℤ)
Tactic: obtain (n | _) | _ := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
n : ℤ
ofNat : (Int.ofNat 0).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat 0)) : ℤ)
ofNat₁ : ∀ (n : ℕ), (Int.ofNat (n + 1)).sign = (↑((SignType.sign : (a : ℤ) → SignType) (Int.ofNat (n + 1))) : ℤ)
⊢ n.sign = (↑((SignType.sign : (a : ℤ) → SignType) n) : ℤ)
have negSucc : ∀ (a : ℕ), -[a+1].sign = (↑((SignType.sign : (a : ℤ) → SignType) -[a+1]) : ℤ)
Tactic: obtain (n | _) | _ := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
i : ℕ
⊢ (s.head :: s.tail) i = s i
have zero : (s.head :: s.tail) 0 = s 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
s : Stream' α
i : ℕ
zero : (s.head :: s.tail) 0 = s 0
⊢ (s.head :: s.tail) i = s i
have succ : ∀ (n : ℕ), (s.head :: s.tail) (n + 1) = s (n + 1)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (m + n)
have rw : (drop m s).get n = s.get (n + m)
Tactic: rw [Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (m + n) s
have a : ∀ (n_1 : ℕ), (drop n (drop m s)).get n_1 = (drop (m + n) s).get n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
i : ℕ
s : Stream' α
⊢ (drop i s).tail = drop (i + 1) s
have a : ∀ (n : ℕ), (drop i s).tail.get n = (drop (i + 1) s).get n
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y
have rw : (x :: s).get 0 = y
Tactic: rw [← get_zero_cons x s, h, get_zero_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
rw : (x :: s).get 0 = y
⊢ x = y
have rw₁ : (y :: t).get 0 = y
Tactic: rw [← get_zero_cons x s, h, get_zero_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
rw : (x :: s).get 0 = y
rw₁ : (y :: t).get 0 = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← get_zero_cons x s, h, get_zero_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ s.get n = t.get n
have rw : (x :: s).get n.succ = t.get n
Tactic: rw [← get_succ_cons n _ x, h, get_succ_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
rw : (x :: s).get n.succ = t.get n
⊢ s.get n = t.get n
have rw₁ : (y :: t).get n.succ = t.get n
Tactic: rw [← get_succ_cons n _ x, h, get_succ_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
rw : (x :: s).get n.succ = t.get n
rw₁ : (y :: t).get n.succ = t.get n
⊢ s.get n = t.get n
have rw₂ : t.get n = t.get n
Tactic: rw [← get_succ_cons n _ x, h, get_succ_cons]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
b : α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
⊢ (fun (b : α) ↦ a = b) ((b :: s).get n.succ)
have rw : (fun (b : α) ↦ a = b) ((b :: s).tail.get n)
Tactic: rw [get_succ, tail_cons, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a : α
s : Stream' α
b : α
h_1 : a ∈ s
n : ℕ
h : (fun (b : α) ↦ a = b) (s.get n)
rw : a = (b :: s).tail.get n
rw₁ : a = s.get n
⊢ a = (b :: s).get n.succ
have rw₂ : (fun (b : α) ↦ s.get n = b) (s.get n)
Tactic: rw [get_succ, tail_cons, h]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n : ℕ
h : (fun (b : α) ↦ a = b) ((b :: s).get n)
⊢ a = b ∨ a ∈ s
have zero : ∀ (h : a = (b :: s).get 0), a = b ∨ a ∈ s
Tactic: rcases n with - | n'
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n : ℕ
h : (fun (b : α) ↦ a = b) ((b :: s).get n)
zero : ∀ (h : a = (b :: s).get 0), a = b ∨ a ∈ s
⊢ a = b ∨ a ∈ s
have succ : ∀ (n' : ℕ) (h : a = (b :: s).get (n' + 1)), a = b ∨ a ∈ s
Tactic: rcases n with - | n'
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s
have zero : a = b
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s
have succ : a ∈ s
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Stream.Init (hypothesis)
Goal:
α : Type u
a b : α
s : Stream' α
h_1 : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a ∈ s
have h₁ : a = s.get n'
Tactic: rw [get_succ, tail_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = f s.head :: map f s.tail
have rw : (map f s).head :: (map f s).tail = f s.head :: map f s.tail
Tactic: rw [← Stream'.eta (map f s), tail_map, head_map]
-- Lean 4 proof step from Mathlib.Data.Stream.Init (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Stream' α
rw : (map f s).head :: (map f s).tail = f s.head :: map f s.tail
⊢ map f s = f s.head :: map f s.tail
have rw₁ : (map f s).head :: map f s.tail = f s.head :: map f s.tail
Tactic: rw [← Stream'.eta (map f s), tail_map, head_map]