awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.PrimeMultiplicity
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R
hp : Prime p
r : R
⊢ (multiplicity_addValuation hp : (a : R) → ℕ∞) r = emultiplicity p r

Tactic:
rfl

Premises used: dite, rfl, emultiplicity
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
q : R ⧸ J
a b : R
h : (Submodule.quotientRel J : R → R → Prop) a b
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (b + -(-a + b)) : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v

Tactic:
ext fun _ => rfl

Premises used: Valuation.ext, rfl
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation.{u_1, u_2} (R ⧸ J) Γ₀
rw : Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) J ≤ v.supp
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
rw [comap_supp, ← Ideal.map_le_iff_le_comap]

Premises used: Valuation.comap_supp, Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation.{u_1, u_2} (R ⧸ J) Γ₀
⊢ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) J ≤ v.supp

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation.{u_1, u_2} (R ⧸ J) Γ₀
r : R ⧸ J
x : R
⊢ Eq.{u_2 + 1} (α := Γ₀)
    (((comap (Ideal.Quotient.mk J) v).onQuot ⋯ : (a : R ⧸ J) → Γ₀)
        (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x) :
      Γ₀)
    ((v : (a : R ⧸ J) → Γ₀) (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x) : Γ₀)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
a : (v.onQuot hJ).supp ≤ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp
a₁ : Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp
⊢ (v.onQuot hJ).supp = Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x_1 : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x ∈ (v.onQuot hJ).supp
a :
  Membership.mem (γ := Set (R ⧸ J)) ((⇑(Ideal.Quotient.mk J) : (a : R) → R ⧸ J) '' (↑v.supp : Set R))
    (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)
⊢ Membership.mem (γ := Submodule (R ⧸ J) (R ⧸ J)) (Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp)
    (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x_1 : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x ∈ (v.onQuot hJ).supp
⊢ Membership.mem (γ := Set (R ⧸ J)) ((⇑(Ideal.Quotient.mk J) : (a : R) → R ⧸ J) '' (↑v.supp : Set R))
    (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x_1 : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x ∈ (v.onQuot hJ).supp
⊢ Membership.mem (γ := Set (R ⧸ J)) ((⇑(Ideal.Quotient.mk J) : (a : R) → R ⧸ J) '' (↑v.supp : Set R))
    (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
a : v.supp ≤ Ideal.comap (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) (v.onQuot hJ).supp
⊢ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Tactic:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
hx : x ∈ v.supp
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) (v.onQuot hJ).supp) x

Tactic:
hx

Premises used: Quotient.liftOn', Set.Mem, setOf, Valuation.onQuotVal, Set.preimage
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
hx : x ∈ v.supp
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) (v.onQuot hJ).supp) x

Tactic:
exact hx
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
rw : Eq (α := Ideal (R ⧸ v.supp)) (Ideal.map (F := R →+* R ⧸ v.supp) (Ideal.Quotient.mk v.supp) v.supp) 0
⊢ (v.onQuot ⋯).supp = 0

Tactic:
rw [supp_quot]

Premises used: Valuation.supp_quot
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq (α := Ideal (R ⧸ v.supp)) (Ideal.map (F := R →+* R ⧸ v.supp) (Ideal.Quotient.mk v.supp) v.supp) 0

Tactic:
Ideal.map_quotient_self _

Premises used: Ideal.map_quotient_self
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq (α := Ideal (R ⧸ v.supp)) (Ideal.map (F := R →+* R ⧸ v.supp) (Ideal.Quotient.mk v.supp) v.supp) 0

Tactic:
exact Ideal.map_quotient_self _

Premises used: Ideal.map_quotient_self
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v

Tactic:
Valuation.onQuot_comap_eq v hJ

Premises used: AddValuation.onQuot, AddValuation.comap, AddValuation, Valuation.onQuot_comap_eq
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
S : Type u_3
inst_2 : CommRing S
f : S →+* R
⊢ (comap f v).supp = Ideal.comap f v.supp

Tactic:
Valuation.comap_supp v f

Premises used: AddValuation.supp, AddValuation.comap, Valuation.comap_supp
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
J : Ideal R
v : AddValuation.{u_1, u_2} (R ⧸ J) Γ₀
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
Valuation.self_le_supp_comap J v

Premises used: Set.Mem, setOf, Valuation.self_le_supp_comap
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
J : Ideal R
v : AddValuation.{u_1, u_2} (R ⧸ J) Γ₀
⊢ (comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v

Tactic:
Valuation.comap_onQuot_eq J v

Premises used: AddValuation.onQuot, AddValuation.comap, Valuation.comap_onQuot_eq, AddValuation
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp = Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp

Tactic:
Valuation.supp_quot v hJ

Premises used: AddValuation.onQuot, AddValuation.supp, Valuation.supp_quot
-- Module: Mathlib.RingTheory.Valuation.Quotient
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ supp (Valuation.onQuot v ⋯) = 0

Tactic:
Valuation.supp_quot_supp v

Premises used: Valuation.supp_quot_supp, AddValuation.supp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
mp : Nonempty.{u_2 + 1} v.RankOne → MulArchimedean.{u_2} (ValueGroup₀ v)
mpr : MulArchimedean.{u_2} (ValueGroup₀ v) → Nonempty.{u_2 + 1} v.RankOne
⊢ Nonempty.{u_2 + 1} v.RankOne ↔ MulArchimedean.{u_2} (ValueGroup₀ v)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : Nonempty.{u_2 + 1} v.RankOne
mp : ∀ (hv : v.RankOne), MulArchimedean.{u_2} (ValueGroup₀ v)
⊢ MulArchimedean.{u_2} (ValueGroup₀ v)

Tactic:
obtain hv := Nonempty.some h

Premises used: Nonempty.some
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : Nonempty.{u_2 + 1} v.RankOne
hv : v.RankOne
⊢ MulArchimedean.{u_2} (ValueGroup₀ v)

Tactic:
MulArchimedean.comap hv.hom'.toMonoidHom hv.strictMono'

Premises used: MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom, Valuation.RankLeOne.strictMono', Valuation.RankLeOne.hom'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : Nonempty.{u_2 + 1} v.RankOne
hv : v.RankOne
⊢ MulArchimedean.{u_2} (ValueGroup₀ v)

Tactic:
exact MulArchimedean.comap hv.hom'.toMonoidHom hv.strictMono'

Premises used: MulArchimedean.comap, MonoidWithZeroHom.toMonoidHom, Valuation.RankLeOne.strictMono', Valuation.RankLeOne.hom'
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
mpr :
  ∀ (f : Additive (ValueGroup₀ v)ˣ →+o ℝ)
    (hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)),
    Nonempty.{u_2 + 1} v.RankOne
⊢ Nonempty.{u_2 + 1} v.RankOne

Tactic:
obtain ⟨f, hf⟩ :=
      Archimedean.exists_orderAddMonoidHom_real_injective (Additive (ValueGroup₀ v)ˣ)

Premises used: Additive, Units, MonoidWithZeroHom.ValueGroup₀, Archimedean.exists_orderAddMonoidHom_real_injective
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
simp :
  StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ)
    (Function.comp (β := ℝ) (⇑ofAdd : (a : ℝ) → Multiplicative ℝ)
      (Function.comp (β := Additive (ValueGroup₀ v)ˣ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
        (⇑Additive.ofMul : (a : (ValueGroup₀ v)ˣ) → Additive (ValueGroup₀ v)ˣ)))
⊢ StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)

Tactic:
simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]

Premises used: AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
⊢ StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ)
    (Function.comp (β := ℝ) (⇑ofAdd : (a : ℝ) → Multiplicative ℝ)
      (Function.comp (β := Additive (ValueGroup₀ v)ˣ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
        (⇑Additive.ofMul : (a : (ValueGroup₀ v)ˣ) → Additive (ValueGroup₀ v)ˣ)))

Tactic:
StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)

Premises used: OrderAddMonoidHom.monotone', strictMono_id, Monotone.strictMono_of_injective, StrictMono.comp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
⊢ StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ)
    (Function.comp (β := ℝ) (⇑ofAdd : (a : ℝ) → Multiplicative ℝ)
      (Function.comp (β := Additive (ValueGroup₀ v)ˣ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
        (⇑Additive.ofMul : (a : (ValueGroup₀ v)ˣ) → Additive (ValueGroup₀ v)ˣ)))

Tactic:
exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)

Premises used: OrderAddMonoidHom.monotone', strictMono_id, Monotone.strictMono_of_injective, StrictMono.comp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
⊢ StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)

Tactic:
have he : StrictMono e := by
      simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
      -- toAdd_strictMono is already in an applied form, do defeq abuse instead
      exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x : Multiplicative ℝ
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log

Tactic:
positivity
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x : Multiplicative ℝ
rw : ¬(↑(NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) : ℝ) = (↑0 : ℝ)
⊢ NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯ ≠ 0

Tactic:
rw [ne_eq, Subtype.ext_iff]

Premises used: ne_eq, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x : Multiplicative ℝ
⊢ ¬HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log = 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
⊢ Eq (α := ℝ≥0ˣ) (Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) (β := ℝ) 2 (log (↑1 : WithZero (Multiplicative ℝ)))) ⋯) ⋯) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x x_1 : Multiplicative ℝ
rw :
  (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑(x * x_1) : WithZero (Multiplicative ℝ)).log) ⋯) ⋯) : ℝ≥0) : ℝ) =
    (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ *
              Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x_1 : WithZero (Multiplicative ℝ)).log) ⋯) ⋯) :
          ℝ≥0) :
      ℝ)
⊢ Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑(x * x_1) : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ =
    Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ *
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x_1 : WithZero (Multiplicative ℝ)).log) ⋯) ⋯

Tactic:
rw [Units.ext_iff, Subtype.ext_iff]

Premises used: Units.ext_iff, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x x_1 : Multiplicative ℝ
⊢ (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑(x * x_1) : WithZero (Multiplicative ℝ)).log) ⋯) ⋯) : ℝ≥0) : ℝ) =
    (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ *
              Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x_1 : WithZero (Multiplicative ℝ)).log) ⋯) ⋯) :
          ℝ≥0) :
      ℝ)

Tactic:
simp [log_mul, Real.rpow_add]

Premises used: WithZero.log_mul, Real.rpow_add
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)

Tactic:
map'_strictMono ?_

Premises used: WithZero.map'_strictMono
-- Module: Mathlib.RingTheory.Valuation.RankOne
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
refine : StrictMono (α := (ValueGroup₀ v)ˣ) (β := ℝ≥0ˣ) (⇑(rf.comp e) : (a : (ValueGroup₀ v)ˣ) → ℝ≥0ˣ)
⊢ StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)

Tactic:
refine map'_strictMono ?_

Premises used: WithZero.map'_strictMono