awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h :
  ∀
    (h :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            a :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
h₁ :
  ∀ (h : ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h₁ :
  ∀ (b : A)
    (h :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap A K : (a : A) → K) b) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    ∃ (x : A),
      Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
        Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a

Tactic:
obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le

Premises used: Eq.le, IsDiscreteValuationRing.exists_lift_of_le_one, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap A K : (a : A) → K) b) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ b ∉ asIdeal (maximalIdeal A)

Tactic:
rw [valuation_eq_one_iff_notMem] at h

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h : b ∉ asIdeal (maximalIdeal A)
⊢ IsUnit b

Tactic:
simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h

Premises used: Classical.not_not, mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, IsDiscreteValuationRing.maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h : IsUnit b
w : A
left : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) b
right : Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) b : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)

Tactic:
use b, h
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h : ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
h₁ :
  ∀ (x : A) (h : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x),
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap A K : (a : A) → K) x) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨x, h, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : A
h : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap A K : (a : A) → K) x) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simpa [IsDiscreteValuationRing.maximalIdeal] using h

Premises used: IsDiscreteValuationRing.maximalIdeal
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
pos : ∀ (hx : x = 0), ∃ (u : Aˣ), u • x = y
neg : ∀ (hx : ¬x = 0), ∃ (u : Aˣ), u • x = y
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : x = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))

Tactic:
rw [eq_comm] at h

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : x = 0
h₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
⊢ x = 0

Tactic:
rw [eq_comm] at h

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
hx : x = 0
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
pos : ∀ (hy : y = 0), ∃ (u : Aˣ), u • x = y
neg : ∀ (hy : ¬y = 0), ∃ (u : Aˣ), u • x = y
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : y = 0
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
⊢ Membership.mem (γ := Submonoid K)
    (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) (y / x)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
⊢ Membership.mem (γ := Submonoid K)
    (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) (y / x)

Tactic:
have : (y / x) ∈ MonoidHom.mker (((maximalIdeal A).valuation K)) := by simp_all
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
this :
  Membership.mem (γ := Submonoid K)
    (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) (y / x)
⊢ Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) (y / x)

Tactic:
rw [mker_valuation_eq_isUnitSubmonoid] at this

Premises used: IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
this : Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) (y / x)
neg :
  ∀ (u : A) (h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x), ∃ (u : Aˣ), u • x = y
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
obtain ⟨u, h⟩ := this
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h_1 :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x
h₁ : IsUnit.unit ⋯ • x = y
⊢ ∃ (u : Aˣ), u • x = y

Tactic:
use IsUnit.unit h.1

Premises used: And.left, IsUnit.unit
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h_1 :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x
h₁ : y / x * x = y
⊢ IsUnit.unit ⋯ • x = y

Tactic:
simp only [Units.smul_def, Algebra.smul_def, IsUnit.unit_spec, h.2]

Premises used: And.right, Units.smul_def, Algebra.smul_def, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h_1 :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
u : A
h : u ∈ (↑(IsUnit.submonoid A) : Set A) ∧ (algebraMap A K : (a : A) → K) u = y / x
⊢ y / x * x = y

Tactic:
field_simp
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
h :
  ∀ (x : K),
    Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
      Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
⊢ Eq (α := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
    (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h :
  ∀ (h : Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x),
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
h₁ :
  ∀
    (h :
      Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x),
    Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x ↔
    Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x
h₁ :
  ∀ (w : A),
    Membership.mem (γ := Subring A) ⊤ w →
      ∀
        (h :
          Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
            (((algebraMap A K : A →+* K) : (a : A) → K) w : K)),
        Membership.mem (α := K) (γ := Subring K)
          (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
          (((algebraMap A K : A →+* K) : (a : A) → K) w : K)
⊢ Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x

Tactic:
obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h

Premises used: Subring.mem_map, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
w : A
left : Membership.mem (γ := Subring A) ⊤ w
h :
  Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
    (((algebraMap A K : A →+* K) : (a : A) → K) w : K)
⊢ Membership.mem (α := K) (γ := Subring K)
    (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
    (((algebraMap A K : A →+* K) : (a : A) → K) w : K)

Tactic:
apply valuation_le_one

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_le_one
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
h : Membership.mem (γ := Subring K) (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A)))) x
h₁ :
  ∀ (y : A)
    (h :
      Membership.mem (α := K) (γ := Subring K)
        (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
        ((algebraMap A K : (a : A) → K) y : K)),
    Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤)
      ((algebraMap A K : (a : A) → K) y : K)
⊢ Membership.mem (γ := Subring K) (Subring.map.{u_1, u_2} (R := A) (algebraMap A K) ⊤) x

Tactic:
obtain ⟨y, rfl⟩ := exists_lift_of_le_one h

Premises used: IsDiscreteValuationRing.exists_lift_of_le_one, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
y : A
h :
  Membership.mem (α := K) (γ := Subring K)
    (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
    ((algebraMap A K : (a : A) → K) y : K)
⊢ ∃ (x : A),
    Membership.mem (γ := Subring A) ⊤ x ∧
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)

Tactic:
⟨y, mem_top _, rfl⟩

Premises used: Subring.mem_top, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
y : A
h :
  Membership.mem (α := K) (γ := Subring K)
    (ValuationSubring.toSubring (valuationSubring (valuation K (maximalIdeal A))))
    ((algebraMap A K : (a : A) → K) y : K)
⊢ ∃ (x : A),
    Membership.mem (γ := Subring A) ⊤ x ∧
      Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)

Tactic:
exact ⟨y, mem_top _, rfl⟩