awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
inst_4 : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)
z : ℤ
inl : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑(↑n : ℤ) : R) : S) ((g : (a : R) → S) (↑(↑n : ℤ) : R) : S)
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑z : R) : S) ((g : (a : R) → S) (↑z : R) : S)
have inr : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑(-(↑n : ℤ)) : R) : S) ((g : (a : R) → S) (↑(-(↑n : ℤ)) : R) : S)
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Ring R
inst_1 : CommRing S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ HSub.hSub (α := S) (β := S) ((abv : (a : R) → S) b : S) ((abv : (a : R) → S) a : S) ≤ (abv : (a : R) → S) (a - b)
have rw : HSub.hSub (α := S) (β := S) ((abv : (a : R) → S) b : S) ((abv : (a : R) → S) a : S) ≤ (abv : (a : R) → S) (b - a)
Tactic: rw [abv.map_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inl : (if 0 * y = 0 then 0 else 1) = HMul.hMul (α := S) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
inl :
  (if 0 * y = 0 then 0 else 1) =
    HMul.hMul (α := S) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr : ∀ (hx : x ≠ 0), (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr : (if x * 0 = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1)
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
inr :
  (if x * 0 = 0 then 0 else 1) =
    HMul.hMul (α := S) (if x = 0 then 0 else 1) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1)
⊢ (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr₁ : ∀ (hy : y ≠ 0), (if x * y = 0 then 0 else 1) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x : R
⊢ LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)
have inl : ∀ (hx : x = 0), LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x : R
inl : ∀ (hx : x = 0), LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)
⊢ LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)
have inr : ∀ (hx : x ≠ 0), LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x : R
⊢ Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0
have inl : ∀ (hx : x = 0), Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0
Tactic: rcases eq_or_ne x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x : R
inl : ∀ (hx : x = 0), Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0
⊢ Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0
have inr : ∀ (hx : x ≠ 0), Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0
Tactic: rcases eq_or_ne x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inl : (if 0 + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
inl :
  (if 0 + y = 0 then 0 else 1) ≤
    HAdd.hAdd (α := S) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1) (if y = 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr : ∀ (hx : x ≠ 0), (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr : (if x + 0 = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1)
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
inr :
  (if x + 0 = 0 then 0 else 1) ≤
    HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if Eq.{u_5 + 1} (α := R) 0 0 then 0 else 1)
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr₁ : ∀ (hy : y ≠ 0), (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (if x + y = 0 then 0 else 1) ≤ HAdd.hAdd (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
have inr : LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
Tactic: simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
have inr : ∀ (hxy : x + y = 0), LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
Tactic: rcases eq_or_ne (x + y) 0 with hxy | hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
inst : Semiring R
inst_1 : DecidablePred fun (x : R) ↦ x = 0
inst_2 : NoZeroDivisors R
S : Type u_6
inst_3 : Semiring S
inst_4 : PartialOrder S
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
x y : R
hx : x ≠ 0
hy : y ≠ 0
inr : ∀ (hxy : x + y = 0), LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
⊢ LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
have inr₁ : ∀ (hxy : x + y ≠ 0), LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
Tactic: rcases eq_or_ne (x + y) 0 with hxy | hxy
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial S
v : AbsoluteValue R S
⊢ v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial
have refine : ∀ (H : v ≠ AbsoluteValue.trivial), v.IsNontrivial
Tactic: refine ⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
have contrapose! : ∀ (H : ∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)), v = AbsoluteValue.trivial
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ v = AbsoluteValue.trivial
have a : ∀ (x : R), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
x : R
⊢ Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
have a : Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) 0 : S) ((AbsoluteValue.trivial : (a : R) → S) 0 : S)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
inst_4 : DecidablePred fun (x : R) ↦ x = 0
inst_5 : NoZeroDivisors R
inst_6 : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
x : R
a : Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) 0 : S) ((AbsoluteValue.trivial : (a : R) → S) 0 : S)
⊢ Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
have a₁ : ∀ (hx : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
v : AbsoluteValue R S
⊢ (¬∃ (x : R), x ≠ 0 ∧ Ne.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)) ↔
    ∀ (x : R), x ≠ 0 → Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
have push : (∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)) ↔
  ∀ (x : R), x ≠ 0 → Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
have obtain : ∀ (x : R) (hx₀ : x ≠ 0) (hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)),
  ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
Tactic: obtain ⟨x, hx₀, hx₁⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
have inl : ∀ (h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)),
  ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
Tactic: rcases hx₁.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
inl :
  ∀ (h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)),
    ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
have inr : ∀ (h : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)),
  ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
Tactic: rcases hx₁.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)
have inl : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x⁻¹ : S)
Tactic: refine ⟨x⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : Ne.{u_4 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)
h : LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
⊢ LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x⁻¹ : S)
have inl : LT.lt.{u_4} (α := S) (1 : S) (((v : (a : R) → S) x)⁻¹ : S)
Tactic: rw [map_inv₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
have obtain : ∀ (y : R) (hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)),
  ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
Tactic: obtain ⟨y, hy⟩ := h.exists_abv_gt_one
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
have hy₀ : y ≠ 0
Tactic: have hy₀ := v.ne_zero_iff.mp <| (zero_lt_one.trans hy).ne'
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
⊢ ∃ (x : R), x ≠ 0 ∧ LT.lt.{u_4} (α := S) ((v : (a : R) → S) x : S) (1 : S)
have refine : LT.lt.{u_4} (α := S) ((v : (a : R) → S) y⁻¹ : S) (1 : S)
Tactic: refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) y : S)
hy₀ : y ≠ 0
⊢ LT.lt.{u_4} (α := S) ((v : (a : R) → S) y⁻¹ : S) (1 : S)
have rw : LT.lt.{u_4} (α := S) (((v : (a : R) → S) y)⁻¹ : S) (1 : S)
Tactic: rw [map_inv₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Euclidean (goal)
Goal:
x y : ℤ
⊢ |x| < |y| ↔ x.natAbs < y.natAbs
have rw : (↑x.natAbs : ℤ) < |y| ↔ x.natAbs < y.natAbs
Tactic: rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Euclidean (goal)
Goal:
x y : ℤ
rw : (↑x.natAbs : ℤ) < |y| ↔ x.natAbs < y.natAbs
⊢ |x| < |y| ↔ x.natAbs < y.natAbs
have rw₁ : LT.lt (α := ℤ) (↑x.natAbs : ℤ) (↑y.natAbs : ℤ) ↔ x.natAbs < y.natAbs
Tactic: rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Euclidean (goal)
Goal:
x y : ℤ
rw : (↑x.natAbs : ℤ) < |y| ↔ x.natAbs < y.natAbs
rw₁ : LT.lt (α := ℤ) (↑x.natAbs : ℤ) (↑y.natAbs : ℤ) ↔ x.natAbs < y.natAbs
⊢ |x| < |y| ↔ x.natAbs < y.natAbs
have rw₂ : x.natAbs < y.natAbs ↔ x.natAbs < y.natAbs
Tactic: rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
h : Eq.{u_2 + 1} (α := α) ⊤ 0
⊢ False
have obtain : ∀ (a : α) (ha : a ≠ 0), False
Tactic: obtain ⟨a, ha⟩ := exists_ne (0 : α)
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (hypothesis)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
h : Eq.{u_2 + 1} (α := α) ⊤ 0
a : α
ha : a ≠ 0
⊢ False
have ha₁ : 0 + a ≠ 0
Tactic: rw [← zero_add a] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
have rw : ¬a + b = ⊤ ↔ ¬a = ⊤ ∧ ¬b = ⊤
Tactic: rw [← not_iff_not, not_or]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
⊢ - -a = a
have inl : Eq.{u_2 + 1} (α := α) (- -⊤) ⊤
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
inl : Eq.{u_2 + 1} (α := α) (- -⊤) ⊤
⊢ - -a = a
have inr : ∀ (ha : a ≠ ⊤), - -a = a
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
⊢ - -a = a
have inr : - -a + -a = 0
Tactic: apply left_neg_eq_right_neg (a := -a)
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b c a : α
ha : a ≠ ⊤
inr : - -a + -a = 0
⊢ - -a = a
have inr₁ : -a + a = 0
Tactic: apply left_neg_eq_right_neg (a := -a)
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
⊢ -(a + b) = -b + -a
have inl : -(⊤ + b) = -b + -⊤
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
inl : -(⊤ + b) = -b + -⊤
⊢ -(a + b) = -b + -a
have inr : ∀ (ha : a ≠ ⊤), -(a + b) = -b + -a
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
ha : a ≠ ⊤
⊢ -(a + b) = -b + -a
have inr : -(a + ⊤) = -⊤ + -a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
ha : a ≠ ⊤
inr : -(a + ⊤) = -⊤ + -a
⊢ -(a + b) = -b + -a
have inr₁ : ∀ (hb : b ≠ ⊤), -(a + b) = -b + -a
Tactic: obtain rfl | hb := eq_or_ne b ⊤
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a_1 b_1 c a b : α
h : a + b = 0
⊢ -a = b
have ha : a ≠ ⊤
Tactic: have ha : a ≠ ⊤ := by rintro rfl; simp at h
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 → a ≠ ⊤
have contrapose : a = ⊤ → ¬a + -a = 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - a = 0 ↔ a ≠ ⊤
have rw : a + -a = 0 ↔ a ≠ ⊤
Tactic: rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.AddGroupWithTop (goal)
Goal:
α : Type u_2
inst : LinearOrderedAddCommGroupWithTop α
a : α
rw : a + -a = 0 ↔ a ≠ ⊤
⊢ a - a = 0 ↔ a ≠ ⊤
have rw₁ : a ≠ ⊤ ↔ a ≠ ⊤
Tactic: rw [sub_eq_add_neg, add_neg_cancel_iff_ne_top]