awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
inst_5 : Nontrivial R
inst_6 : IsDomain S
⊢ MulRingNormClass (AbsoluteValue R S) R S

Tactic:
{ AbsoluteValue.subadditiveHomClass,
    AbsoluteValue.monoidWithZeroHomClass with
    map_neg_eq_map := fun f => f.map_neg
    eq_zero_of_map_eq_zero := fun f _ => f.eq_zero.1 }

Premises used: MulRingNormClass.mk, AbsoluteValue.eq_zero, AbsoluteValue.monoidWithZeroHomClass, Iff.mp, AbsoluteValue.subadditiveHomClass
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
x : ℤ
inl :
  ∀ (w : ℕ),
    Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (↑w : ℤ)) : R) : S) ((abv : (a : R) → S) (↑(↑w : ℤ) : R) : S)
inr :
  ∀ (w : ℕ),
    Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (-(↑w : ℤ))) : R) : S)
      ((abv : (a : R) → S) (↑(-(↑w : ℤ)) : R) : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑x.natAbs : R) : S) ((abv : (a : R) → S) (↑x : R) : S)

Tactic:
obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
w : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (↑w : ℤ)) : R) : S) ((abv : (a : R) → S) (↑(↑w : ℤ) : R) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
w : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (-(↑w : ℤ))) : R) : S)
    ((abv : (a : R) → S) (↑(-(↑w : ℤ)) : R) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
⊢ (∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)) ↔
    ∀ (n : ℤ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)

Tactic:
⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩

Premises used: Int.cast_natCast, congrArg, cast, Nat.cast, congr, Iff.intro, Eq, DFunLike.coe
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
refine :
  ∀ (h : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)) (z : ℤ),
    Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑z : R) : S) ((g : (a : R) → S) (↑z : R) : S)
⊢ (∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)) ↔
    ∀ (n : ℤ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)

Tactic:
refine ⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
inr :
  ∀ (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)

Tactic:
obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
n : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑(↑n : ℤ) : R) : S) ((g : (a : R) → S) (↑(↑n : ℤ) : R) : S)

Tactic:
simp [h n]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
n : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑(-(↑n : ℤ)) : R) : S) ((g : (a : R) → S) (↑(-(↑n : ℤ)) : R) : S)

Tactic:
simp [h n]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
rw : HSub.hSub (α := S) (β := S) ((abv : (a : R) → S) b : S) ((abv : (a : R) → S) a : S) ≤ (abv : (a : R) → S) (b - a)
⊢ HSub.hSub (α := S) (β := S) ((abv : (a : R) → S) b : S) ((abv : (a : R) → S) a : S) ≤ (abv : (a : R) → S) (a - b)

Tactic:
rw [abv.map_sub]

Premises used: AbsoluteValue.map_sub
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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) (b - a)

Tactic:
apply abv.le_sub

Premises used: AbsoluteValue.le_sub
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
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)
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
y : R
⊢ (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:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
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)
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x ≠ 0
⊢ (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:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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) = HMul.hMul (α := S) (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
inr : ∀ (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)

Tactic:
rcases eq_or_ne x 0 with hx | hx

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x = 0
⊢ LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x ≠ 0
⊢ LE.le.{u_6} (α := S) 0 (if x = 0 then 0 else 1)

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
inr : ∀ (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

Tactic:
rcases eq_or_ne x 0 with hx | hx

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x = 0
⊢ Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x ≠ 0
⊢ Eq.{u_6 + 1} (α := S) (if x = 0 then 0 else 1) 0 ↔ x = 0

Tactic:
simp [hx]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
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)
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
y : R
⊢ (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:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
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)
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x ≠ 0
⊢ (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:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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 : LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2
⊢ (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:
simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]

Premises used: one_add_one_eq_two, reduceIte
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
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

Tactic:
rcases eq_or_ne (x + y) 0 with hxy | hxy

Premises used: HAdd.hAdd, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hxy : x + y = 0
⊢ LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2

Tactic:
simp [hxy, one_le_two]

Premises used: one_le_two
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hxy : x + y ≠ 0
⊢ LE.le.{u_6} (α := S) (if x + y = 0 then 0 else 1) 2

Tactic:
simp [hxy, one_le_two]

Premises used: one_le_two
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
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
hx : x ≠ 0
⊢ Eq.{u_6 + 1} (α := S) ((AbsoluteValue.trivial : (a : R) → S) x : S) (1 : S)

Tactic:
if_neg hx

Premises used: if_neg, ite
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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

Tactic:
⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩

Premises used: False, Eq.rec, _private.0.AbsoluteValue.isNontrivial_iff_ne_trivial.match_1, AbsoluteValue.trivial_apply, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
refine : ∀ (H : v ≠ AbsoluteValue.trivial), v.IsNontrivial
⊢ v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial

Tactic:
refine ⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
contrapose! :
  ∀ (H : ∀ (x : R) (_ : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)), v = AbsoluteValue.trivial
⊢ ∃ (x : R), x ≠ 0 ∧ Ne.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)

Tactic:
contrapose! H
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
a : ∀ (x : R), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
⊢ v = AbsoluteValue.trivial

Tactic:
ext1 x
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
a₁ : ∀ (hx : x ≠ 0), Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
⊢ Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) 0 : S) ((AbsoluteValue.trivial : (a : R) → S) 0 : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
hx : x ≠ 0
⊢ Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) ((AbsoluteValue.trivial : (a : R) → S) x : S)

Tactic:
simp [H, hx]
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
v : AbsoluteValue R S
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)
⊢ (¬∃ (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)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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), 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:
rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
R : Type u_5
inst : Semiring R
S : Type u_6
inst_1 : Semiring S
inst_2 : PartialOrder S
v : AbsoluteValue R S
hv : ¬v.IsNontrivial
x : R
hx : x ≠ 0
⊢ Eq.{u_6 + 1} (α := S) ((v : (a : R) → S) x : S) (1 : S)

Tactic:
v.not_isNontrivial_iff.mp hv _ hx

Premises used: AbsoluteValue.not_isNontrivial_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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
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)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)

Tactic:
obtain ⟨x, hx₀, hx₁⟩ := h
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
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)
⊢ ∃ (x : R), LT.lt.{u_4} (α := S) (1 : S) ((v : (a : R) → S) x : S)

Tactic:
rcases hx₁.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)

Tactic:
⟨x⁻¹, ?_⟩

Premises used: Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
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)
inl : 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:
refine ⟨x⁻¹, ?_⟩