awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
⊢ ∀ (a : ↥(MonoidHom.mrange v)),
    Membership.mem (γ := Set ↥(MonoidHom.mrange v)) {x : ↥(MonoidHom.mrange v) | x ≤ 1} a →
      ∀ (b : ↥(MonoidHom.mrange v)),
        Membership.mem (γ := Set ↥(MonoidHom.mrange v)) {x : ↥(MonoidHom.mrange v) | x ≤ 1} b →
          a > b →
            ((fun (x1 x2 : Γ₀) ↦ x1 > x2) on
                Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
              a b

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
refine_1 :
  ∀
    (h :
      Set.WellFoundedOn
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        fun (x1 x2 : Γ₀) ↦ x1 > x2),
    Set.MapsTo.{u_2, u_2} (α := ↥(MonoidHom.mrange v))
      (Subtype.val (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
refine_2 :
  (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) →
    Γ₀ → ↥(MonoidHom.mrange v)
refine_3 :
  ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2),
    Set.MapsTo (β := ↥(MonoidHom.mrange v))
      (fun (x : Γ₀) ↦
        if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
          Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
        else 1)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
refine_4 :
  ∀ (h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) (a : Γ₀),
    Membership.mem (γ := Set Γ₀)
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        a →
      ∀ (b : Γ₀),
        Membership.mem (γ := Set Γ₀)
            (Set.range.{u_2, u_3 + 1} (ι := O)
              (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀)
                (⇑(algebraMap O F) : (a : O) → F)))
            b →
          a > b →
            ((fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) on fun (x : Γ₀) ↦
                if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
                  Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
                else 1)
              a b
⊢ (Set.WellFoundedOn
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      fun (x1 x2 : Γ₀) ↦ x1 > x2) ↔
    Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2

Tactic:
refine ⟨fun h ↦ (h.mapsTo Subtype.val ?_).mono' (by simp), fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
x : F
refine_1 :
  LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀) →
    ∃ (y : O),
      Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) x : Γ₀)
⊢ Membership.mem.{u_2, u_2} (α := ↥(MonoidHom.mrange v)) (γ := Set ↥(MonoidHom.mrange v))
      {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      (Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) ((v : (a : F) → Γ₀) x)
          ⋯ :
        ↥(MonoidHom.mrange v)) →
    Membership.mem.{u_2, u_2} (α := Γ₀) (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      ((↑(Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x)
              ((v : (a : F) → Γ₀) x) ⋯) :
          Γ₀) :
        Γ₀)

Tactic:
simp only [← Subtype.coe_le_coe, OneMemClass.coe_one, Set.mem_setOf_eq, Set.mem_range,
      Function.comp_apply]

Premises used: Set.mem_range, OneMemClass.coe_one, Subtype.coe_le_coe, Set.mem_setOf_eq, Function.comp_apply
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
x : F
hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
refine_1 :
  ∀ (y : O) (hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) (1 : Γ₀)),
    ∃ (y_1 : O),
      Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y_1 : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
⊢ ∃ (y : O),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ((v : (a : F) → Γ₀) x : Γ₀)

Tactic:
obtain ⟨y, rfl⟩ := hv.exists_of_le_one hx

Premises used: Valuation.Integers.exists_of_le_one, rfl
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
y : O
hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) (1 : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h :
  Set.WellFoundedOn
    (Set.range.{u_2, u_3 + 1} (ι := O)
      (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
    fun (x1 x2 : Γ₀) ↦ x1 > x2
y : O
hx : LE.le.{u_2} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) (1 : Γ₀)
⊢ ∃ (y_1 : O),
    Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y_1 : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)

Tactic:
exact ⟨y, by simp⟩
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
⊢ Γ₀ → ↥(MonoidHom.mrange v)

Tactic:
exact fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1

Premises used: Membership.mem, dite, MonoidHom.mrange, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
x : Γ₀
refine_3 :
  ∀ (x_1 : O) (h : (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x_1 : F) = x),
    LE.le.{u_2} (α := ↥(MonoidHom.mrange v))
      (if h : ∃ (x_2 : F), (v : (a : F) → Γ₀) x_2 = x then
        Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x ⋯
      else 1)
      1
⊢ Membership.mem (γ := Set Γ₀)
      (Set.range.{u_2, u_3 + 1} (ι := O)
        (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
      x →
    Membership.mem (γ := Set ↥(MonoidHom.mrange v)) {x : ↥(MonoidHom.mrange v) | x ≤ 1}
      ((fun (x : Γ₀) ↦
          (if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
              Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
            else 1 :
            ↥(MonoidHom.mrange v)))
        x)

Tactic:
simp only [Set.mem_range, Function.comp_apply, MonoidHom.mem_mrange, Set.mem_setOf_eq,
      forall_exists_index]

Premises used: Set.mem_range, forall_exists_index, Set.mem_setOf_eq, Function.comp_apply, MonoidHom.mem_mrange
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
x : O
⊢ LE.le.{u_2} (α := ↥(MonoidHom.mrange v))
    (if h :
        ∃ (x_1 : F),
          Eq.{u_2 + 1} (α := Γ₀) ((v : (a : F) → Γ₀) x_1 : Γ₀)
            ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) then
      Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F)) ⋯
    else 1)
    1

Tactic:
simp [← Subtype.coe_le_coe, hv.map_le_one]

Premises used: Valuation.Integers.map_le_one, Subtype.coe_le_coe
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : Set.WellFoundedOn {x : ↥(MonoidHom.mrange v) | x ≤ 1} fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2
⊢ ∀ (a : Γ₀),
    Membership.mem (γ := Set Γ₀)
        (Set.range.{u_2, u_3 + 1} (ι := O)
          (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F)))
        a →
      ∀ (b : Γ₀),
        Membership.mem (γ := Set Γ₀)
            (Set.range.{u_2, u_3 + 1} (ι := O)
              (Function.comp.{u_3 + 1, u_1 + 1, u_2 + 1} (β := F) (⇑v : (a : F) → Γ₀)
                (⇑(algebraMap O F) : (a : O) → F)))
            b →
          a > b →
            ((fun (x1 x2 : ↥(MonoidHom.mrange v)) ↦ x1 > x2) on fun (x : Γ₀) ↦
                if hx : Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x then
                  Subtype.mk (p := fun (x : Γ₀) ↦ Membership.mem (γ := Submonoid Γ₀) (MonoidHom.mrange v) x) x hx
                else 1)
              a b

Tactic:
simp [Function.onFun]

Premises used: Function.onFun
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)

Tactic:
⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩

Premises used: Valuation.Integers.not_denselyOrdered_of_isPrincipalIdealRing, Iff.intro
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
refine :
  ∀ (H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)),
    IsPrincipalIdealRing O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)

Tactic:
refine ⟨fun _ ↦ not_denselyOrdered_of_isPrincipalIdealRing hv, fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
inl : ∀ (hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ), IsPrincipalIdealRing O
inr : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ → IsPrincipalIdealRing O
⊢ IsPrincipalIdealRing O

Tactic:
rcases subsingleton_or_nontrivial (MonoidHom.mrange v)ˣ with hs | _

Premises used: Membership.mem, Units, Subtype, subsingleton_or_nontrivial, MonoidHom.mrange
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ
⊢ Function.Bijective.{u_3 + 1, u_1 + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)

Tactic:
have := bijective_algebraMap_of_subsingleton_units_mrange hv
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ
this : Function.Bijective.{u_3 + 1, u_1 + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)
⊢ IsPrincipalIdealRing O

Tactic:
.of_surjective _ (RingEquiv.ofBijective _ this).symm.surjective

Premises used: RingEquiv.surjective, RingEquiv.ofBijective, IsPrincipalIdealRing.of_surjective, RingEquiv.symm
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
hs : Subsingleton.{u_2 + 1} (↥(MonoidHom.mrange v))ˣ
this : Function.Bijective.{u_3 + 1, u_1 + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)
⊢ IsPrincipalIdealRing O

Tactic:
exact .of_surjective _ (RingEquiv.ofBijective _ this).symm.surjective
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
⊢ IsDomain O

Tactic:
have : IsDomain O := hv.hom_inj.isDomain
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this : IsDomain O
⊢ ValuationRing O

Tactic:
have : ValuationRing O := ValuationRing.of_integers v hv
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this : ValuationRing O
⊢ IsPrincipalIdealRing O ↔ WfDvdMonoid O

Tactic:
have := ((IsBezout.TFAE (R := O)).out 1 3)
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this_2 : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
inr : ¬DenselyOrdered.{u_2} ↥(MonoidHom.mrange v)
⊢ IsPrincipalIdealRing O

Tactic:
rw [this, hv.wfDvdMonoid_iff_wellFounded_gt_on_v, hv.wellFounded_gt_on_v_iff_discrete_mrange,
    LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]

Premises used: Valuation.Integers.wfDvdMonoid_iff_wellFounded_gt_on_v, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this_2 : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered.{u_2} ↥(MonoidHom.mrange v)

Tactic:
H

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
H : ¬DenselyOrdered.{u_2} (↑(Set.range.{u_2, u_1 + 1} (ι := F) (⇑v : (a : F) → Γ₀)) : Type u_2)
h : Nontrivial.{u_2} (↥(MonoidHom.mrange v))ˣ
this_1 : IsDomain O
this_2 : ValuationRing O
this : IsPrincipalIdealRing O ↔ WfDvdMonoid O
⊢ ¬DenselyOrdered.{u_2} ↥(MonoidHom.mrange v)

Tactic:
exact H
-- Module: Mathlib.RingTheory.Valuation.Archimedean
Goal:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : CommRing O
inst_3 : Algebra O F
v : Valuation F Γ₀
inst_4 : MulArchimedean.{u_2} ↥(MonoidHom.mrange v)
hv : v.Integers O
⊢ IsPrincipalIdealRing O ↔ ¬DenselyOrdered.{u_2} ↥(MonoidHom.mrange v)

Tactic:
isPrincipalIdealRing_iff_not_denselyOrdered hv

Premises used: Set.Mem, setOf, Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered, Set.range
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
f g : Valuation R Γ₀
h :
  Eq (α := (a : R) → Γ₀) ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) f)
    ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) g)
obtain :
  ∀ (toFun : R → Γ₀) (map_zero' : toFun 0 = 0)
    (map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun 1 = 1)
    (map_mul' :
      ∀ (x y : R),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun (x * y) =
          { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun x *
            { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun y)
    (map_add_le_max' :
      ∀ (x y : R),
        (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
                ZeroHom R Γ₀).toFun
            (x + y) ≤
          max
            ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
                  ZeroHom R Γ₀).toFun
              x)
            ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
                  ZeroHom R Γ₀).toFun
              y))
    (h :
      Eq (α := (a : R) → Γ₀)
        ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun)
          { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
            map_add_le_max' := map_add_le_max' })
        ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) g)),
    { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
        map_add_le_max' := map_add_le_max' : Valuation R Γ₀ } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f