-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
lemma isNontrivial_iff_ne_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R]
    [Nontrivial S] (v : AbsoluteValue R S) :
    v.IsNontrivial ↔ v ≠ .trivial

Proof state:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ v.IsNontrivial

Tactic:
simp only [IsNontrivial]

Result:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Proof state:
case a
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
x : R
⊢ v x = AbsoluteValue.trivial x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case a.inl
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
⊢ v 0 = AbsoluteValue.trivial 0

case a.inr
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
x : R
hx : x ≠ 0
⊢ v x = AbsoluteValue.trivial x

Proof state:
case a.inl
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
⊢ v 0 = AbsoluteValue.trivial 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
⊢ v = AbsoluteValue.trivial

Tactic:
ext1 x

Result:
case a
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
x : R
⊢ v x = AbsoluteValue.trivial x

Proof state:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
⊢ v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial

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

Result:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ v.IsNontrivial

Proof state:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ ∃ x, x ≠ 0 ∧ v x ≠ 1

Tactic:
contrapose! H

Result:
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
⊢ v = AbsoluteValue.trivial

Proof state:
case a.inr
R : Type u_5
inst✝⁴ : Semiring R
S : Type u_6
inst✝³ : OrderedSemiring S
inst✝² : DecidablePred fun x => x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : ∀ (x : R), x ≠ 0 → v x = 1
x : R
hx : x ≠ 0
⊢ v x = AbsoluteValue.trivial x

Tactic:
simp [H, hx]

Result:
no goals