awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
h₁ :
  Eq (α := R → K)
    (Function.comp (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.val (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x))
      (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range))
    (⇑(g.comp f) : (a : R) → K)
⊢ Eq (α := R → K)
    (Function.comp (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.val (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x))
      (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range))
    (⇑(algebraMap R K) : (a : R) → K)

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
⊢ Eq (α := R → K)
    (Function.comp (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.val (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x))
      (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range))
    (⇑(g.comp f) : (a : R) → K)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)

Tactic:
exact .of_comp (f := Subtype.val) (by convert! (IsFractionRing.injective R K); rw [← h]; rfl)
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
obtain :
  ∀ (y : R) (hy : Eq.{u_3 + 1} (α := K) (((algebraMap R K : R →+* K) : (a : R) → K) y : K) ((g : (a : S) → K) x : K)),
    ∃ (a : R),
      Eq.{u_3 + 1} (α := ↥(RingHom.range.{u_2, u_3} (R := S) g))
        ((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) a : ↥(RingHom.range.{u_2, u_3} (R := S) g))
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
            ((g : (a : S) → K) x) ⋯ :
          ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ ∃ (a : R),
    Eq.{u_3 + 1} (α := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      ((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) a : ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
          ((g : (a : S) → K) x) ⋯ :
        ↥(RingHom.range.{u_2, u_3} (R := S) g))

Tactic:
obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : Eq.{u_3 + 1} (α := K) (((algebraMap R K : R →+* K) : (a : R) → K) y : K) ((g : (a : S) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K) ((↑((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) y) : K) : K)
    ((↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
            ((g : (a : S) → K) x) ⋯) :
        K) :
      K)

Tactic:
simpa [← h] using hy
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : Eq.{u_3 + 1} (α := K) (((algebraMap R K : R →+* K) : (a : R) → K) y : K) ((g : (a : S) → K) x : K)
⊢ ∃ (a : R),
    Eq.{u_3 + 1} (α := ↥(RingHom.range.{u_2, u_3} (R := S) g))
      ((RingHom.comp g.rangeRestrict f : (a : R) → ↥g.range) a : ↥(RingHom.range.{u_2, u_3} (R := S) g))
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
          ((g : (a : S) → K) x) ⋯ :
        ↥(RingHom.range.{u_2, u_3} (R := S) g))

Tactic:
exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
refine_2 : LocalSubring.range g ≤ V.toLocalSubring
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (⇑(RingHom.comp g.rangeRestrict f) : (a : R) → ↥g.range)

Tactic:
suffices LocalSubring.range g ≤ V.toLocalSubring by
      rintro ⟨_, x, rfl⟩
      obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
      exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
refine_2 : V.toLocalSubring ≤ LocalSubring.range g
⊢ LocalSubring.range g ≤ V.toLocalSubring

Tactic:
apply V.isMax_toLocalSubring

Premises used: ValuationSubring.isMax_toLocalSubring
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
x : K
h_1 : Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K)) x
a : R
ha : ((algebraMap R K : R →+* K) : (a : R) → K) a = x
⊢ (g : (a : S) → K) ((f : (a : R) → S) a : S) = x

Tactic:
simp [← ha, ← h]
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
⊢ LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)

Tactic:
have H : (algebraMap R K).range ≤ g.range := fun x ⟨a, ha⟩ ↦ ⟨f a, by simp [← ha, ← h]⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
⊢ V.toLocalSubring ≤ LocalSubring.range g

Tactic:
⟨H, ⟨?_⟩⟩

Premises used: IsLocalHom.mk, Exists.intro
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
refine_2 :
  ∀ (a : ↥V.toLocalSubring.toSubring),
    IsUnit (M := ↥(LocalSubring.range g).toSubring)
        ((Subring.inclusion H : (a : ↥V.toLocalSubring.toSubring) → ↥(LocalSubring.range g).toSubring) a :
          ↥(LocalSubring.range g).toSubring) →
      IsUnit a
⊢ V.toLocalSubring ≤ LocalSubring.range g

Tactic:
refine ⟨H, ⟨?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
refine_2 : IsUnit a
⊢ IsUnit.{u_3} (M := ↥V.toLocalSubring.toSubring)
    (Subtype.mk (p := fun (x : K) ↦ x ∈ V.toLocalSubring.toSubring) (((algebraMap R K : R →+* K) : (a : R) → K) a) ⋯ :
      ↥V.toLocalSubring.toSubring)

Tactic:
suffices IsUnit a from this.map (algebraMap R K).rangeRestrict
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
refine_2 : IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S)
⊢ IsUnit a

Tactic:
apply IsUnit.of_map f

Premises used: IsUnit.of_map
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
refine_2 :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    ((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a) : ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S)

Tactic:
apply (IsLocalHom.of_surjective g.rangeRestrict g.rangeRestrict_surjective).1

Premises used: IsLocalHom.map_nonunit
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))

Tactic:
ha
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
h₁ :
  Eq.{u_3 + 1} (α := K) ((↑((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a)) : K) : K)
    ((algebraMap R K : (a : R) → K) a : K)
⊢ IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    ((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a) : ↥(RingHom.range.{u_2, u_3} (R := S) g))

Tactic:
convert! ha
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : IsDomain R
inst_4 : ValuationRing R
inst_5 : IsLocalRing S
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst_8 : IsLocalHom (R := R) (S := S) f
V : ValuationSubring K := { toSubring := RingHom.range.{u_1, u_3} (R := R) (algebraMap R K), mem_or_inv_mem' := ⋯ }
H :
  LE.le.{u_3} (α := Subring K) (RingHom.range.{u_1, u_3} (R := R) (algebraMap R K))
    (RingHom.range.{u_2, u_3} (R := S) g)
a : R
ha :
  IsUnit.{u_3} (M := ↥(RingHom.range.{u_2, u_3} (R := S) g))
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) (RingHom.range.{u_2, u_3} (R := S) g) x)
        ((algebraMap R K : (a : R) → K) a) ⋯ :
      ↥(RingHom.range.{u_2, u_3} (R := S) g))
⊢ Eq.{u_3 + 1} (α := K) ((↑((g.rangeRestrict : (a : S) → ↥g.range) ((f : (a : R) → S) a)) : K) : K)
    ((algebraMap R K : (a : R) → K) a : K)

Tactic:
simp [← h]
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
obtain :
  ∀ (B : ValuationSubring K) (hB : LocalSubring.range f ≤ B.toLocalSubring),
    ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
      IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)
⊢ ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)

Tactic:
obtain ⟨B, hB⟩ := (LocalSubring.range f).exists_le_valuationSubring

Premises used: LocalSubring.exists_le_valuationSubring, LocalSubring.range
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)

Tactic:
⟨B, fun x ↦ hB.1 ⟨x, rfl⟩, ?_⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
refine : IsLocalHom (R := R) (S := ↥B.toSubring) (F := RingHom.{u_1, u_3} R ↥B.toSubring) (f.codRestrict B.toSubring ⋯)
⊢ ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)

Tactic:
refine ⟨B, fun x ↦ hB.1 ⟨x, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ IsLocalHom (R := R) (S := ↥B.toSubring) (F := RingHom.{u_1, u_3} R ↥B.toSubring) (f.codRestrict B.toSubring ⋯)

Tactic:
@RingHom.isLocalHom_comp _ _ _ _ _ _ _ _ hB.2 (.of_surjective _ f.rangeRestrict_surjective)

Premises used: Set.Mem, RingHom.isLocalHom_comp, RingHom.codRestrict
-- Module: Mathlib.RingTheory.Valuation.LocalSubring
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ IsLocalHom (R := R) (S := ↥B.toSubring) (F := RingHom.{u_1, u_3} R ↥B.toSubring) (f.codRestrict B.toSubring ⋯)

Tactic:
exact @RingHom.isLocalHom_comp _ _ _ _ _ _ _ _ hB.2 (.of_surjective _ f.rangeRestrict_surjective)

Premises used: RingHom.isLocalHom_comp
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₂ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) 0 (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₃ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (0 - x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
rw₄ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (-x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
rw₅ rw₆ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]

Premises used: Polynomial.coeff_X_zero, Polynomial.coeff_sub, Valuation.map_neg, Polynomial.coeff_C_zero, minpoly.eq_X_sub_C, zero_sub
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
⊢ Algebra.IsAlgebraic K L

Tactic:
have h_alg : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
⊢ IsIntegral K x

Tactic:
have hx₀ : IsIntegral K x := (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
⊢ 0 < finrank K L / natDegree (minpoly K x)

Tactic:
have hdeg := Nat.div_pos (natDegree_le x) (natDegree_pos hx₀)
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / natDegree (minpoly K x)
rw : ¬coeff (minpoly K x) 0 = 0
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (coeff (minpoly K x) 0) : Γ₀) (finrank K L / natDegree (minpoly K x)) ≠ 0

Tactic:
rw [ne_eq, pow_eq_zero_iff hdeg.ne.symm, Valuation.zero_iff]

Premises used: pow_eq_zero_iff, Valuation.zero_iff, Ne.symm, ne_eq, LT.lt.ne
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / natDegree (minpoly K x)
⊢ ¬coeff (minpoly K x) 0 = 0

Tactic:
coeff_zero_ne_zero hx₀ hx.ne_zero

Premises used: minpoly.coeff_zero_ne_zero, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.Valuation.Minpoly
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / natDegree (minpoly K x)
⊢ ¬coeff (minpoly K x) 0 = 0

Tactic:
exact coeff_zero_ne_zero hx₀ hx.ne_zero

Premises used: minpoly.coeff_zero_ne_zero, IsUnit.ne_zero