awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderBot ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderBot (α ⊥)
x : Σₗ (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊥), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) ⊥ b
⊢ mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
have inr : ∀ (ha : ⊥ < a), mk (β := fun (i : ι) ↦ α i) ⊥ ⊥ ≤ mk (β := fun (i : ι) ↦ α i) a b
Tactic: obtain rfl | ha := eq_bot_or_bot_lt a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ (i : ι), α i
a : ι
b : α a
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
have inl : ∀ (b : α ⊤), mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
Tactic: obtain rfl | ha := eq_top_or_lt_top a
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : PartialOrder ι
inst_1 : OrderTop ι
inst_2 : (i : ι) → Preorder (α i)
inst_3 : OrderTop (α ⊤)
x : Σₗ (i : ι), α i
a : ι
b : α a
inl : ∀ (b : α ⊤), mk (β := fun (i : ι) ↦ α i) ⊤ b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
⊢ mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
have inr : ∀ (ha : a < ⊤), mk (β := fun (i : ι) ↦ α i) a b ≤ mk (β := fun (i : ι) ↦ α i) ⊤ ⊤
Tactic: obtain rfl | ha := eq_top_or_lt_top a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (k : ι) (hi : i < k) (hj : k < j),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨k, hi, hj⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
k : ι
hi : i < k
hj : k < j
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α k), ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c⟩ : Nonempty (α k) := inferInstance
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : DenselyOrdered ι
inst_2 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
inst_3 : (i : ι) → Preorder (α i)
inst_4 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α i) (ha : a < c),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c, ha⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
j : ι
b : α j
h : i < j
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
have left : ∀ (c : α j) (hb : c < b),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) j b
Tactic: obtain ⟨c, hb⟩ := exists_lt b
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), DenselyOrdered.{u_2} (α i)
inst_3 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
have right : ∀ (c : α i) (ha : a < c) (hb : c < b),
  ∃ (a_1 : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < a_1 ∧ a_1 < mk (β := fun (i : ι) ↦ α i) i b
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (j : ι) (h : i < j), ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨j, h⟩ := exists_gt i
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMaxOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : i < j
⊢ ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (b : α j), ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨b⟩ : Nonempty (α j) := inferInstance
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (j : ι) (h : j < i), ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨j, h⟩ := exists_lt i
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : NoMinOrder ι
inst_3 : ∀ (i : ι), Nonempty.{u_2 + 1} (α i)
i : ι
a : α i
j : ι
h : j < i
⊢ ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (b : α j), ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨b⟩ : Nonempty (α j) := inferInstance
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMaxOrder.{u_2} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
have obtain : ∀ (b : α i) (h : a < b), ∃ (b : Σₗ (i : ι), α i), mk (β := fun (i : ι) ↦ α i) i a < b
Tactic: obtain ⟨b, h⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Data.Sigma.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Preorder ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_2} (α i)
i : ι
a : α i
⊢ ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
have obtain : ∀ (b : α i) (h : b < a), ∃ (b : Σₗ (i : ι), α i), b < mk (β := fun (i : ι) ↦ α i) i a
Tactic: obtain ⟨b, h⟩ := exists_lt a
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
n : ℕ
hn : Odd n
⊢ s ^ n = s
have obtain : ∀ (k : ℕ), s ^ (2 * k + 1) = s
Tactic: obtain ⟨k, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
k : ℕ
⊢ s ^ (2 * k + 1) = s
have rw : (s * s) ^ k * s = s
Tactic: rw [pow_add, pow_one, pow_mul, sq]
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
k : ℕ
⊢ (s * s) ^ k * s = s
have zero : (zero * zero) ^ k * zero = zero
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
k : ℕ
zero : (SignType.zero * SignType.zero) ^ k * SignType.zero = SignType.zero
⊢ (s * s) ^ k * s = s
have neg : (neg * neg) ^ k * neg = neg
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
k : ℕ
zero : (SignType.zero * SignType.zero) ^ k * SignType.zero = SignType.zero
neg : (SignType.neg * SignType.neg) ^ k * SignType.neg = SignType.neg
⊢ (s * s) ^ k * s = s
have pos : (pos * pos) ^ k * pos = pos
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Odd z
⊢ s ^ z = s
have inl : HPow.hPow (α := SignType) 0 z = 0
Tactic: obtain rfl | hs := eq_or_ne s 0
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Odd z
inl : HPow.hPow (α := SignType) 0 z = 0
⊢ s ^ z = s
have inr : ∀ (hs : s ≠ 0), s ^ z = s
Tactic: obtain rfl | hs := eq_or_ne s 0
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
z : ℤ
hz : Odd z
⊢ HPow.hPow (α := SignType) 0 z = 0
have inl : z ≠ 0
Tactic: rw [zero_zpow]
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Odd z
hs : s ≠ 0
⊢ s ^ z = s
have inr : ∀ (k : ℤ), s ^ (2 * k + 1) = s
Tactic: obtain ⟨k, rfl⟩ := hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
⊢ s ^ (2 * k + 1) = s
have inr : (s * s) ^ k * s = s
Tactic: rw [zpow_add₀ hs, zpow_one, zpow_mul, zpow_two]
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s * s) ^ k * s = s
have inr : ∀ (hs : zero ≠ 0), (zero * zero) ^ k * zero = zero
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
inr : ∀ (hs : zero ≠ 0), (zero * zero) ^ k * zero = zero
⊢ (s * s) ^ k * s = s
have inr₁ : ∀ (hs : neg ≠ 0), (neg * neg) ^ k * neg = neg
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
hs : s ≠ 0
k : ℤ
inr : ∀ (hs : zero ≠ 0), (zero * zero) ^ k * zero = zero
inr₁ : ∀ (hs : neg ≠ 0), (neg * neg) ^ k * neg = neg
⊢ (s * s) ^ k * s = s
have inr₂ : ∀ (hs : pos ≠ 0), (pos * pos) ^ k * pos = pos
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
⊢ s ^ n = 1
have zero : ∀ (hs : zero ≠ 0), zero ^ n = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ n = 1
⊢ s ^ n = 1
have neg : ∀ (hs : neg ≠ 0), neg ^ n = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
n : ℕ
hn : Even n
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ n = 1
neg : ∀ (hs : SignType.neg ≠ 0), SignType.neg ^ n = 1
⊢ s ^ n = 1
have pos : ∀ (hs : pos ≠ 0), pos ^ n = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
⊢ s ^ z = 1
have zero : ∀ (hs : zero ≠ 0), zero ^ z = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ z = 1
⊢ s ^ z = 1
have neg : ∀ (hs : neg ≠ 0), neg ^ z = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
s : SignType
z : ℤ
hz : Even z
hs : s ≠ 0
zero : ∀ (hs : SignType.zero ≠ 0), SignType.zero ^ z = 1
neg : ∀ (hs : SignType.neg ≠ 0), SignType.neg ^ z = 1
⊢ s ^ z = 1
have pos : ∀ (hs : pos ≠ 0), pos ^ z = 1
Tactic: cases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
x y : SignType
⊢ (↑(x * y) : α) = HMul.hMul (α := α) (↑x : α) (↑y : α)
have zero : (↑(zero * y) : α) = HMul.hMul (α := α) (↑zero : α) (↑y : α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
x y : SignType
zero : (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)
⊢ (↑(x * y) : α) = HMul.hMul (α := α) (↑x : α) (↑y : α)
have neg : (↑(neg * y) : α) = HMul.hMul (α := α) (↑neg : α) (↑y : α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
x y : SignType
zero : (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)
neg : (↑(SignType.neg * y) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑y : α)
⊢ (↑(x * y) : α) = HMul.hMul (α := α) (↑x : α) (↑y : α)
have pos : (↑(pos * y) : α) = HMul.hMul (α := α) (↑pos : α) (↑y : α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
⊢ (↑(zero * y) : α) = HMul.hMul (α := α) (↑zero : α) (↑y : α)
have zero : (↑(zero * zero) : α) = HMul.hMul (α := α) (↑zero : α) (↑zero : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
zero : (↑(SignType.zero * SignType.zero) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑SignType.zero : α)
⊢ (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)
have zero₁ : (↑(SignType.zero * neg) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑neg : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
zero : (↑(SignType.zero * SignType.zero) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑SignType.zero : α)
zero₁ : (↑(SignType.zero * neg) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑neg : α)
⊢ (↑(SignType.zero * y) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑y : α)
have zero₂ : (↑(SignType.zero * pos) : α) = HMul.hMul (α := α) (↑SignType.zero : α) (↑pos : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
⊢ (↑(neg * y) : α) = HMul.hMul (α := α) (↑neg : α) (↑y : α)
have neg : (↑(neg * zero) : α) = HMul.hMul (α := α) (↑neg : α) (↑zero : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
neg : (↑(SignType.neg * zero) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑zero : α)
⊢ (↑(SignType.neg * y) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑y : α)
have neg₁ : (↑(SignType.neg * SignType.neg) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑SignType.neg : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
neg : (↑(SignType.neg * zero) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑zero : α)
neg₁ : (↑(SignType.neg * SignType.neg) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑SignType.neg : α)
⊢ (↑(SignType.neg * y) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑y : α)
have neg₂ : (↑(SignType.neg * pos) : α) = HMul.hMul (α := α) (↑SignType.neg : α) (↑pos : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
⊢ (↑(pos * y) : α) = HMul.hMul (α := α) (↑pos : α) (↑y : α)
have pos : (↑(pos * zero) : α) = HMul.hMul (α := α) (↑pos : α) (↑zero : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
pos : (↑(SignType.pos * zero) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑zero : α)
⊢ (↑(SignType.pos * y) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑y : α)
have pos₁ : (↑(SignType.pos * neg) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑neg : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
y : SignType
pos : (↑(SignType.pos * zero) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑zero : α)
pos₁ : (↑(SignType.pos * neg) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑neg : α)
⊢ (↑(SignType.pos * y) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑y : α)
have pos₂ : (↑(SignType.pos * SignType.pos) : α) = HMul.hMul (α := α) (↑SignType.pos : α) (↑SignType.pos : α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
have rw : (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}
Tactic: rw [← Fintype.coe_image_univ, univ_eq]
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
have classical : (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}
Tactic: classical rw [← Fintype.coe_image_univ, univ_eq]
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inl : ∀ (hx : x < 0),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy x 0 with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
inl :
  ∀ (hx : x < 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 : ∀ (hx : x = 0),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy x 0 with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.Data.Sign.Basic (goal)
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
inl :
  ∀ (hx : x < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr :
  ∀ (hx : x = 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₁ : ∀ (hx : 0 < x),
  (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
Tactic: rcases lt_trichotomy x 0 with (hx | hx | hx)
-- 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
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)
have inl : ∀ (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
inl :
  ∀ (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 inl₁ : ∀ (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
inl :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inl₁ :
  ∀ (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 inl₂ : ∀ (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 : x = 0
⊢ (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)