awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inr₁ : ∀ (hy : y = 0),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy y 0 with (hy | hy | hy)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₁ :
  ∀ (hy : y = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inr₂ : ∀ (hy : 0 < y),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy y 0 with (hy | hy | hy)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inr : ∀ (hy : y < 0),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy y 0 with (hy | hy | hy)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inr₁ : ∀ (hy : y = 0),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy y 0 with (hy | hy | hy)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₁ :
  ∀ (hy : y = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inr₂ : ∀ (hy : 0 < y),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy y 0 with (hy | hy | hy)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x
have inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x
have inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) |0| = 0
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) |0| = 0
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x
have inr₁ : ∀ (hx : 0 < x), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x
have inl : ∀ (hx : x < 0), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x
have inr : HMul.hMul (α := α) |0| (↑((sign : (a : α) → SignType) 0) : α) = 0
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
inr : HMul.hMul (α := α) |0| (↑((sign : (a : α) → SignType) 0) : α) = 0
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x
have inr₁ : ∀ (hx : 0 < x), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|
have inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|
have inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) 0 = |0|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) 0 = |0|
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|
have inr₁ : ∀ (hx : 0 < x), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|
have inl : ∀ (hx : x < 0), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|
have inr : HMul.hMul (α := α) 0 (↑((sign : (a : α) → SignType) 0) : α) = |0|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
inr : HMul.hMul (α := α) 0 (↑((sign : (a : α) → SignType) 0) : α) = |0|
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|
have inr₁ : ∀ (hx : 0 < x), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = t
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = t
have zero : ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = zero), (sign : (a : α) → SignType) (∑ i ∈ s, f i) = zero
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = t
zero :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.zero),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.zero
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = t
have neg : ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = neg), (sign : (a : α) → SignType) (∑ i ∈ s, f i) = neg
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = t
zero :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.zero),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.zero
neg :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.neg),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.neg
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = t
have pos : ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = pos), (sign : (a : α) → SignType) (∑ i ∈ s, f i) = pos
Tactic: cases t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = zero
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = zero
have zero : ∀ (h : ∀ i ∈ s, f i = 0), Eq.{u + 1} (α := α) (∑ i ∈ s, f i) 0
Tactic: simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = neg
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = neg
have neg : ∀ (h : ∀ i ∈ s, f i < 0), LT.lt.{u} (α := α) (∑ i ∈ s, f i) 0
Tactic: simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = pos
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = pos
have pos : ∀ (h : ∀ i ∈ s, 0 < f i), LT.lt.{u} (α := α) 0 (∑ i ∈ s, f i)
Tactic: simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ (β : Type u) (t : Finset β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
have refine_1 : card.{u} (α := (_ : ↥s) × ℕ) (Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs) =
  ∑ a ∈ s, (f a).natAbs
Tactic: refine
    ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
      fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
refine_1 :
  card.{u} (α := (_ : ↥s) × ℕ) (Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs) =
    ∑ a ∈ s, (f a).natAbs
⊢ ∃ (β : Type u) (t : Finset β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
have refine_2 : ∀ a ∈ s,
  (∑ b ∈ Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs,
      if (fun (a : (_ : ↥s) × ℕ) ↦ (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) b = a then
        (↑((fun (a : (_ : ↥s) × ℕ) ↦
                ((sign : (a : ℤ) → SignType) (f (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) : SignType))
              b) :
          ℤ)
      else 0) =
    f a
Tactic: refine
    ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
      fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
⊢ ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a
have obtain : ∀ (β : Type u) (w : Fintype β) (sgn : β → SignType) (g : β → α) (hg : ∀ (b : β), g b ∈ s)
  (hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs) (hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a),
  ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a
Tactic: obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
⊢ ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a
have i : ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
  Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0
Tactic: refine
    ⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
      Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)),
        ?_, by simp [hβ, h], fun a ha => by simp [hf _ ha]⟩
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ a = -1 ∨ a = 0 ∨ a = 1
have zero : zero = -1 ∨ zero = 0 ∨ zero = 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero = -1 ∨ SignType.zero = 0 ∨ SignType.zero = 1
⊢ a = -1 ∨ a = 0 ∨ a = 1
have neg : neg = -1 ∨ neg = 0 ∨ neg = 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero = -1 ∨ SignType.zero = 0 ∨ SignType.zero = 1
neg : SignType.neg = -1 ∨ SignType.neg = 0 ∨ SignType.neg = 1
⊢ a = -1 ∨ a = 0 ∨ a = 1
have pos : pos = -1 ∨ pos = 0 ∨ pos = 1
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
⊢ Decidable (a ≤ b)
have zero : Decidable (zero ≤ b)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
zero : Decidable (SignType.zero ≤ b)
⊢ Decidable (a ≤ b)
have neg : Decidable (neg ≤ b)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
zero : Decidable (SignType.zero ≤ b)
neg : Decidable (SignType.neg ≤ b)
⊢ Decidable (a ≤ b)
have pos : Decidable (pos ≤ b)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ Decidable (zero ≤ b)
have zero : Decidable (zero ≤ zero)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
zero : Decidable (SignType.zero ≤ SignType.zero)
⊢ Decidable (SignType.zero ≤ b)
have zero₁ : Decidable (SignType.zero ≤ neg)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
zero : Decidable (SignType.zero ≤ SignType.zero)
zero₁ : Decidable (SignType.zero ≤ neg)
⊢ Decidable (SignType.zero ≤ b)
have zero₂ : Decidable (SignType.zero ≤ pos)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ Decidable (neg ≤ b)
have neg : Decidable (neg ≤ zero)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
neg : Decidable (SignType.neg ≤ zero)
⊢ Decidable (SignType.neg ≤ b)
have neg₁ : Decidable (SignType.neg ≤ SignType.neg)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
neg : Decidable (SignType.neg ≤ zero)
neg₁ : Decidable (SignType.neg ≤ SignType.neg)
⊢ Decidable (SignType.neg ≤ b)
have neg₂ : Decidable (SignType.neg ≤ pos)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ Decidable (pos ≤ b)
have pos : Decidable (pos ≤ zero)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
pos : Decidable (SignType.pos ≤ zero)
⊢ Decidable (SignType.pos ≤ b)
have pos₁ : Decidable (SignType.pos ≤ neg)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
pos : Decidable (SignType.pos ≤ zero)
pos₁ : Decidable (SignType.pos ≤ neg)
⊢ Decidable (SignType.pos ≤ b)
have pos₂ : Decidable (SignType.pos ≤ SignType.pos)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ 1 * a = a
have zero : 1 * zero = zero
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : 1 * SignType.zero = SignType.zero
⊢ 1 * a = a
have neg : 1 * neg = neg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : 1 * SignType.zero = SignType.zero
neg : 1 * SignType.neg = SignType.neg
⊢ 1 * a = a
have pos : 1 * pos = pos
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ a * 1 = a
have zero : zero * 1 = zero
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero * 1 = SignType.zero
⊢ a * 1 = a
have neg : neg * 1 = neg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero * 1 = SignType.zero
neg : SignType.neg * 1 = SignType.neg
⊢ a * 1 = a
have pos : pos * 1 = pos
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ 0 * a = 0
have zero : 0 * zero = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : 0 * SignType.zero = 0
⊢ 0 * a = 0
have neg : 0 * neg = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : 0 * SignType.zero = 0
neg : 0 * SignType.neg = 0
⊢ 0 * a = 0
have pos : 0 * pos = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ a * 0 = 0
have zero : zero * 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero * 0 = 0
⊢ a * 0 = 0
have neg : neg * 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero * 0 = 0
neg : SignType.neg * 0 = 0
⊢ a * 0 = 0
have pos : pos * 0 = 0
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
ha : a ≠ 0
⊢ a * id a = 1
have zero : ∀ (ha : zero ≠ 0), zero * id zero = 1
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
ha : a ≠ 0
zero : ∀ (ha : SignType.zero ≠ 0), SignType.zero * id SignType.zero = 1
⊢ a * id a = 1
have neg : ∀ (ha : neg ≠ 0), neg * id neg = 1
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
ha : a ≠ 0
zero : ∀ (ha : SignType.zero ≠ 0), SignType.zero * id SignType.zero = 1
neg : ∀ (ha : SignType.neg ≠ 0), SignType.neg * id SignType.neg = 1
⊢ a * id a = 1
have pos : ∀ (ha : pos ≠ 0), pos * id pos = 1
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ a ≤ a
have zero : zero ≤ zero
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero ≤ SignType.zero
⊢ a ≤ a
have neg : neg ≤ neg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero : SignType.zero ≤ SignType.zero
neg : SignType.neg ≤ SignType.neg
⊢ a ≤ a
have pos : pos ≤ pos
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
⊢ (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        a) =
    a
have zero : (fun (a : Fin 3) ↦
      (match (motive := Fin 3 → SignType) a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1 :
        SignType))
    ((fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      zero) =
  zero
Tactic: cases a
Cleared hypotheses: a