awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
a :
  (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x * x_1)) ⋯) :
      K) =
    (↑(HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)
⊢ Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
      ((algebraMap A K : (a : A) → K) (x * x_1)) ⋯ =
    HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x_1) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x * x_1)) ⋯) :
      K) =
    (↑(HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)

Tactic:
(algebraMap A K).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x * x_1)) ⋯) :
      K) =
    (↑(HMul.hMul (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)

Tactic:
exact (algebraMap A K).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
a :
  Eq.{v + 1} (α := K)
    ((↑(Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) 0) ⋯) :
        K) :
      K)
    ((↑0 : K) : K)
⊢ Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
        ((algebraMap A K : (a : A) → K) 0) ⋯ :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (0 : ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
⊢ Eq.{v + 1} (α := K)
    ((↑(Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) 0) ⋯) :
        K) :
      K)
    ((↑0 : K) : K)

Tactic:
(algebraMap A K).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
⊢ Eq.{v + 1} (α := K)
    ((↑(Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) 0) ⋯) :
        K) :
      K)
    ((↑0 : K) : K)

Tactic:
exact (algebraMap A K).map_zero

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
a :
  (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x + x_1)) ⋯) :
      K) =
    (↑(HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)
⊢ Subtype.mk (p := fun (x : K) ↦
      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
      ((algebraMap A K : (a : A) → K) (x + x_1)) ⋯ =
    HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) x_1) ⋯ :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x + x_1)) ⋯) :
      K) =
    (↑(HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)

Tactic:
(algebraMap A K).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x x_1 : A
⊢ (↑(Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) (x + x_1)) ⋯) :
      K) =
    (↑(HAdd.hAdd (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) (β :=
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
          (Subtype.mk (p := fun (x : K) ↦
              Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
              ((algebraMap A K : (a : A) → K) x_1) ⋯ :
            ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))) :
      K)

Tactic:
exact (algebraMap A K).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
left :
  Function.Injective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)
right :
  Function.Surjective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)
⊢ Function.Bijective.{u + 1, v + 1} (α := A) (β := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    (⇑(have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
          {
            toFun := fun (a : A) ↦
              Subtype.mk (p := fun (x : K) ↦
                Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                ((algebraMap A K : (a : A) → K) a) ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
        this) :
      (a : A) → ↥(valuation A K).integer)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x y : A
h :
  Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        x :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
    ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        y :
      ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
⊢ Eq (α := K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            x :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            y :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)

Tactic:
apply_fun (algebraMap (valuation A K).integer K) at h

Premises used: Algebra.algebraMap, Membership.mem, ValuationRing.valuation, Subtype, Valuation.integer
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x y : A
h :
  Eq (α := K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            x :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            y :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)
⊢ x = y

Tactic:
IsFractionRing.injective _ _ h

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
x y : A
h :
  Eq (α := K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            x :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)
    ((algebraMap (↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) K : (a : ↥(valuation A K).integer) → K)
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            y :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))) :
      K)
⊢ x = y

Tactic:
exact IsFractionRing.injective _ _ h
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
val : K
ha : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) val
⊢ ∃ (a : A), (algebraMap A K : (a : A) → K) a = val

Tactic:
rw [mem_integer_iff] at ha

Premises used: ValuationRing.mem_integer_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
val : K
ha_1 : Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) val
ha : ∃ (a : A), (algebraMap A K : (a : A) → K) a = val
right :
  ∀ (a : A)
    (ha :
      Membership.mem (α := K) (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
        ((algebraMap A K : (a : A) → K) a : K)),
    ∃ (a_1 : A),
      Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
                {
                  toFun := fun (a : A) ↦
                    Subtype.mk (p := fun (x : K) ↦
                      Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                      ((algebraMap A K : (a : A) → K) a) ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
              this :
              (a : A) → ↥(valuation A K).integer)
            a_1 :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
        (Subtype.mk (p := fun (x : K) ↦
            Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
            ((algebraMap A K : (a : A) → K) a) ha :
          ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
⊢ ∃ (a : A),
    (have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
            {
              toFun := fun (a : A) ↦
                Subtype.mk (p := fun (x : K) ↦
                  Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                  ((algebraMap A K : (a : A) → K) a) ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
          this :
          (a : A) → ↥(valuation A K).integer)
        a =
      Subtype.mk (p := fun (x : K) ↦
        Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x) val ha_1

Tactic:
obtain ⟨a, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationRing
Goal:
A : Type u
inst : CommRing A
K : Type v
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : ValuationRing A
inst_5 : IsFractionRing A K
a : A
ha :
  Membership.mem (α := K) (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K))
    ((algebraMap A K : (a : A) → K) a : K)
⊢ ∃ (a_1 : A),
    Eq.{v + 1} (α := ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      ((have this : NonUnitalRingHom.{u, v} A ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) :=
              {
                toFun := fun (a : A) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
                    ((algebraMap A K : (a : A) → K) a) ⋯,
                map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ };
            this :
            (a : A) → ↥(valuation A K).integer)
          a_1 :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))
      (Subtype.mk (p := fun (x : K) ↦
          Membership.mem (γ := Subring K) (Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)) x)
          ((algebraMap A K : (a : A) → K) a) ha :
        ↥(Valuation.integer (Γ₀ := ValueGroup A K) (valuation A K)))

Tactic:
⟨a, rfl⟩

Premises used: Exists.intro, rfl