awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors R
inst_5 : DecidablePred fun (x : R) ↦ x = 0
x : ↥(posSubmonoid R)
⊢ (↑x : R) ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
a b : A
rw : ¬@vle.{u_2} B inst_1 _ ((algebraMap A B : (a : A) → B) b : B) ((algebraMap A B : (a : A) → B) a : B) ↔ a <ᵥ b
rw₁ : ¬@vle _ inst _ b a ↔ a <ᵥ b
rw₂ rw₃ : a <ᵥ b ↔ a <ᵥ b
⊢ vlt.{u_2} (R := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔ a <ᵥ b

Tactic:
rw [← not_vle, vle_iff_vle, not_vle]

Premises used: ValuativeExtension.vle_iff_vle, ValuativeRel.not_vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
x : ↥(posSubmonoid A)
a : A
ha : Membership.mem (γ := Submonoid A) (posSubmonoid A) a
⊢ Membership.mem (α := B) (γ := Submonoid B) (posSubmonoid B) ((algebraMap A B : (a : A) → B) a : B)

Tactic:
simpa only [posSubmonoid_def, ← (algebraMap A B).map_zero, vlt_iff_vlt] using ha

Premises used: Algebra.algebraMap, ValuativeExtension.vlt_iff_vlt, RingHom.map_zero, ValuativeRel.posSubmonoid_def
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
⊢ Eq.{u_2 + 1} (α := ↥(posSubmonoid B))
    (match (motive := ↥(posSubmonoid A) → ↥(posSubmonoid B)) 1 with
      | ⟨a, ha⟩ =>
        Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submonoid B) (posSubmonoid B) x)
          ((algebraMap A B : (a : A) → B) a) ⋯ :
      ↥(posSubmonoid B))
    (1 : ↥(posSubmonoid B))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
⊢ ∀ (x y : ↥(posSubmonoid A)),
    (match (motive := ↥(posSubmonoid A) → ↥(posSubmonoid B)) x * y with
      | ⟨a, ha⟩ =>
        Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submonoid B) (posSubmonoid B) x)
          ((algebraMap A B : (a : A) → B) a) ⋯) =
      HMul.hMul (α := ↥(posSubmonoid B)) (β := ↥(posSubmonoid B))
        (match (motive := ↥(posSubmonoid A) → ↥(posSubmonoid B)) x with
          | ⟨a, ha⟩ =>
            Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submonoid B) (posSubmonoid B) x)
              ((algebraMap A B : (a : A) → B) a) ⋯ :
          ↥(posSubmonoid B))
        (match (motive := ↥(posSubmonoid A) → ↥(posSubmonoid B)) y with
          | ⟨a, ha⟩ =>
            Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Submonoid B) (posSubmonoid B) x)
              ((algebraMap A B : (a : A) → B) a) ⋯ :
          ↥(posSubmonoid B))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
Γ : Type u_3
inst_6 : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst_7 : w.Compatible
vle_iff_le :
  ∀ (x y : A),
    @vle _ inst _ x y ↔
      LE.le.{u_3} (α := Γ) ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) x : Γ)
        ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) y : Γ)
⊢ Valuation.Compatible.{u_1, u_3} (R := A) (Valuation.comap (algebraMap A B) w)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
Γ : Type u_3
inst_6 : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst_7 : w.Compatible
⊢ ∀ (x y : A),
    @vle _ inst _ x y ↔
      LE.le.{u_3} (α := Γ) ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) x : Γ)
        ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) y : Γ)

Tactic:
simp [← vle_iff_vle (A := A) (B := B), Valuation.Compatible.vle_iff_le (v := w)]

Premises used: ValuativeExtension.vle_iff_vle, Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
r : A
s : ↥(posSubmonoid A)
⊢ Eq.{u_2 + 1} (α := ValueGroupWithZero B)
    (((mapValueGroupWithZero A B : MonoidWithZeroHom.{u_1, u_2} (ValueGroupWithZero A) (ValueGroupWithZero B)) :
          (a : ValueGroupWithZero A) → ValueGroupWithZero B)
        (ValueGroupWithZero.mk r s) :
      ValueGroupWithZero B)
    (ValueGroupWithZero.mk ((algebraMap A B : (a : A) → B) r)
        (((mapPosSubmonoid A B : MonoidHom.{u_1, u_2} ↥(posSubmonoid A) ↥(posSubmonoid B)) :
            (a : ↥(posSubmonoid A)) → ↥(posSubmonoid B))
          s) :
      ValueGroupWithZero B)

Tactic:
simp [mapValueGroupWithZero, mk_eq_div (R := B)]

Premises used: ValuativeRel.ValueGroupWithZero.mk_eq_div, ValuativeExtension.mapValueGroupWithZero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
a : A
⊢ Eq.{u_2 + 1} (α := ValueGroupWithZero B)
    (((mapValueGroupWithZero A B : MonoidWithZeroHom.{u_1, u_2} (ValueGroupWithZero A) (ValueGroupWithZero B)) :
          (a : ValueGroupWithZero A) → ValueGroupWithZero B)
        ((valuation A : (a : A) → ValueGroupWithZero A) a) :
      ValueGroupWithZero B)
    ((valuation B : (a : B) → ValueGroupWithZero B) ((algebraMap A B : (a : A) → B) a) : ValueGroupWithZero B)

Tactic:
simp [valuation]

Premises used: ValuativeRel.valuation
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
⊢ StrictMono.{u_1, u_2} (α := ValueGroupWithZero A) (β := ValueGroupWithZero B)
    (⇑(mapValueGroupWithZero A B) : (a : ValueGroupWithZero A) → ValueGroupWithZero B)

Tactic:
embedding_strictMono.comp (embed_strictMono _)

Premises used: Set.Mem, ValuativeRel.ValueGroupWithZero.embed_strictMono, setOf, StrictMono.comp, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
inst_6 : IsRankLeOne B
obtain :
  ∀ (f : ValueGroupWithZero B →*₀ NNReal)
    (hf : StrictMono (α := ValueGroupWithZero B) (β := NNReal) (⇑f : (a : ValueGroupWithZero B) → NNReal)),
    IsRankLeOne A
⊢ IsRankLeOne A

Tactic:
obtain ⟨⟨f, hf⟩⟩ := IsRankLeOne.nonempty (R := B)

Premises used: ValuativeRel.IsRankLeOne.nonempty
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
inst_6 : IsRankLeOne B
f : ValueGroupWithZero B →*₀ NNReal
hf : StrictMono (α := ValueGroupWithZero B) (β := NNReal) (⇑f : (a : ValueGroupWithZero B) → NNReal)
⊢ IsRankLeOne A

Tactic:
⟨⟨f.comp (mapValueGroupWithZero _ _), hf.comp mapValueGroupWithZero_strictMono⟩⟩

Premises used: ValuativeExtension.mapValueGroupWithZero_strictMono, ValuativeExtension.mapValueGroupWithZero, Nonempty.intro, ValuativeRel.RankLeOneStruct.mk, MonoidWithZeroHom.comp, ValuativeRel.IsRankLeOne.mk, StrictMono.comp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
inst_6 : IsRankLeOne B
f : ValueGroupWithZero B →*₀ NNReal
hf : StrictMono (α := ValueGroupWithZero B) (β := NNReal) (⇑f : (a : ValueGroupWithZero B) → NNReal)
⊢ IsRankLeOne A

Tactic:
exact ⟨⟨f.comp (mapValueGroupWithZero _ _), hf.comp mapValueGroupWithZero_strictMono⟩⟩
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsRankLeOne R
obtain :
  ∀ (f : ValueGroupWithZero R →*₀ NNReal)
    (hf : StrictMono (α := ValueGroupWithZero R) (β := NNReal) (⇑f : (a : ValueGroupWithZero R) → NNReal)),
    MulArchimedean.{u_1} (ValueGroupWithZero R)
⊢ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
obtain ⟨⟨f, hf⟩⟩ := IsRankLeOne.nonempty (R := R)

Premises used: ValuativeRel.IsRankLeOne.nonempty
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsRankLeOne R
f : ValueGroupWithZero R →*₀ NNReal
hf : StrictMono (α := ValueGroupWithZero R) (β := NNReal) (⇑f : (a : ValueGroupWithZero R) → NNReal)
⊢ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
.comap f.toMonoidHom hf

Premises used: MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsRankLeOne R
f : ValueGroupWithZero R →*₀ NNReal
hf : StrictMono (α := ValueGroupWithZero R) (β := NNReal) (⇑f : (a : ValueGroupWithZero R) → NNReal)
⊢ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
exact .comap f.toMonoidHom hf
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
pos : x_1 = 0 → x = 0 → x = 0 ∨ x_1 = 0
neg : x_1 = 0 → ¬x = 0 → x = 0 ∨ True
pos₁ : ¬x_1 = 0 → x = 0 → True ∨ x_1 = 0
neg₁ : ¬x_1 = 0 → ¬x = 0 → True ∨ True
⊢ (if x_1 = 0 then x = 0 else True) ∨ if x = 0 then x_1 = 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
h : x_1 = 0
h_1 : x = 0
⊢ x = 0 ∨ x_1 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
h : x_1 = 0
h_1 : ¬x = 0
⊢ x = 0 ∨ True

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
h : ¬x_1 = 0
h_1 : x = 0
⊢ True ∨ x_1 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
h : ¬x_1 = 0
h_1 : ¬x = 0
⊢ True ∨ True

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
z y x : R
h : if y = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
pos : z = 0 → x = 0
⊢ if z = 0 then x = 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
z y x : R
h : if y = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
h_2 : z = 0
⊢ x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : if z = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
pos : z = 0 → x + y = 0
⊢ if z = 0 then x + y = 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : if z = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
h_2 : z = 0
⊢ x + y = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y : R
h : if y = 0 then x = 0 else True
x_1 : R
pos : y * x_1 = 0 → y = 0 → x = 0 → x * x_1 = 0
neg : y * x_1 = 0 → ¬y = 0 → True → x * x_1 = 0
⊢ if y * x_1 = 0 then x * x_1 = 0 else True

Tactic:
split_ifs at *
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y x_1 : R
h : y * x_1 = 0
h_1 : y = 0
h_2 : x = 0
⊢ x * x_1 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y x_1 : R
h : y * x_1 = 0
h_1 : ¬y = 0
h_2 : True
⊢ x * x_1 = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
pos : y * z = 0 → y = 0 → x * z = 0 → x = 0
neg : y * z = 0 → ¬y = 0 → x * z = 0 → True
pos₁ : ¬y * z = 0 → y = 0 → True → x = 0
neg₁ : ¬y * z = 0 → ¬y = 0 → True → True
⊢ (if y * z = 0 then x * z = 0 else True) → if y = 0 then x = 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
h_1 : y * z = 0
h_2 : y = 0
⊢ x * z = 0 → x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
h_1 : y * z = 0
h_2 : ¬y = 0
⊢ x * z = 0 → True

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
h_1 : ¬y * z = 0
h_2 : y = 0
⊢ True → x = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
h_1 : ¬y * z = 0
h_2 : ¬y = 0
⊢ True → True

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
pos : Eq (α := R) 0 0 → ¬Eq (α := R) 1 0
neg : ¬Eq (α := R) 0 0 → ¬True
⊢ ¬if Eq (α := R) 0 0 then Eq (α := R) 1 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : Eq (α := R) 0 0
⊢ ¬Eq (α := R) 1 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ¬Eq (α := R) 0 0
⊢ ¬True

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
vle : ∀ (x x_1 : R), @ValuativeRel.vle _ inst _ x x_1 ↔ @ValuativeRel.vle _ inst _ x x_1
⊢ h = trivialRel

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
vle : LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ if x_1 = 0 then x = 0 else True
⊢ @ValuativeRel.vle _ inst _ x x_1 ↔ if x_1 = 0 then x = 0 else True

Tactic:
rw [hv.vle_iff_le]

Premises used: Valuation.Compatible.vle_iff_le
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
pos : x_1 = 0 → (LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ x = 0)
neg : ¬x_1 = 0 → (LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ True)
⊢ LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ if x_1 = 0 then x = 0 else True

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
h_1 : x_1 = 0
⊢ LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ x = 0

Tactic:
simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

Premises used: Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
h_1 : ¬x_1 = 0
⊢ LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ True

Tactic:
simp_all [Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one]

Premises used: Valuation.one_apply_of_ne_zero, Valuation.one_apply_le_one
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
⊢ Eq (α := ValuativeRel R) trivialRel (ofValuation (Γ := Γ) 1)

Tactic:
(eq_trivialRel_of_compatible_one (Γ := Γ)).symm

Premises used: ValuativeRel.eq_trivialRel_of_compatible_one, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
convert_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
⊢ Eq (α := ValuativeRel R) trivialRel (ofValuation (Γ := Γ) 1)

Tactic:
convert! (eq_trivialRel_of_compatible_one (Γ := Γ)).symm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
⊢ Valuation.Compatible (R := R) (Γ := Γ) 1

Tactic:
Valuation.Compatible.ofValuation 1

Premises used: Valuation.Compatible.ofValuation, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
⊢ Valuation.Compatible (R := R) (Γ := Γ) 1

Tactic:
exact Valuation.Compatible.ofValuation 1

Premises used: Valuation.Compatible.ofValuation, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
allEq : ∀ (a b : (ValueGroupWithZero R)ˣ), a = b
⊢ Subsingleton (ValueGroupWithZero R)ˣ

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
⊢ Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1

Tactic:
have : (valuation R).IsEquiv (1 : Valuation R Γ) := isEquiv _ _
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
allEq :
  ∀ (r s : ↥(posSubmonoid R))
    (hr :
      HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
        (↑a : ValueGroupWithZero R)),
    a = b
⊢ a = b

Tactic:
obtain ⟨r, s, hr⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq a

Premises used: ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
r s : ↥(posSubmonoid R)
hr :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (↑a : ValueGroupWithZero R)
allEq :
  ∀ (t u : ↥(posSubmonoid R))
    (ht :
      HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑t : R) : ValueGroupWithZero R)
          ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R) =
        (↑b : ValueGroupWithZero R)),
    a = b
⊢ a = b

Tactic:
obtain ⟨t, u, ht⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq b

Premises used: ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
inst_4 : ValuativeRel R
inst_5 : Valuation.Compatible (R := R) (Γ := Γ) 1
a b : (ValueGroupWithZero R)ˣ
this : Valuation.IsEquiv (Γ₀ := ValueGroupWithZero R) (Γ'₀ := Γ) (valuation R) 1
r s : ↥(posSubmonoid R)
hr :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) =
    (↑a : ValueGroupWithZero R)
t u : ↥(posSubmonoid R)
ht :
  HDiv.hDiv (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑t : R) : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R) =
    (↑b : ValueGroupWithZero R)
allEq : Eq (α := Γ) ((1 : (a : R) → Γ) ((↑r : R) * (↑u : R)) : Γ) ((1 : (a : R) → Γ) ((↑t : R) * (↑s : R)) : Γ)
allEq₁ :
  Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
allEq₂ :
  Ne (α := ValueGroupWithZero R) ((valuation R : (a : R) → ValueGroupWithZero R) (↑u : R) : ValueGroupWithZero R)
    (0 : ValueGroupWithZero R)
⊢ a = b

Tactic:
rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff]

Premises used: Units.ext_iff, div_eq_div_iff, map_mul, Valuation.IsEquiv.eq_iff