awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
inst : CommRing R
ΓR : Type u_6
inst_1 : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero ΓS
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
vS : Valuation S ΓS
inst_6 : vR.HasExtension vS
r : ↥vR.integer
hr :
  Eq.{u_10 + 1} (α := ΓS)
    ((vS : (a : S) → ΓS)
        ((algebraMap (↥vS.integer) S : (a : ↥vS.integer) → S)
            ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer) :
          S) :
      ΓS)
    (1 : ΓS)
⊢ Eq.{u_6 + 1} (α := ΓR) ((vR : (a : R) → ΓR) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R) : ΓR)
    (1 : ΓR)

Tactic:
(val_map_eq_one_iff vR vS _).mp hr

Premises used: Valuation.HasExtension.val_map_eq_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
inst : CommRing R
ΓR : Type u_6
inst_1 : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst_2 : CommRing S
inst_3 : LinearOrderedCommGroupWithZero ΓS
inst_4 : Algebra R S
inst_5 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
vS : Valuation S ΓS
inst_6 : vR.HasExtension vS
r : ↥vR.integer
hr :
  Eq.{u_10 + 1} (α := ΓS)
    ((vS : (a : S) → ΓS)
        ((algebraMap (↥vS.integer) S : (a : ↥vS.integer) → S)
            ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer) :
          S) :
      ΓS)
    (1 : ΓS)
⊢ Eq.{u_6 + 1} (α := ΓR) ((vR : (a : R) → ΓR) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R) : ΓR)
    (1 : ΓR)

Tactic:
exact (val_map_eq_one_iff vR vS _).mp hr

Premises used: Valuation.HasExtension.val_map_eq_one_iff, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
rw : LE.le.{u_7} (α := Γ₀) ((vK : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ Membership.mem (α := L) L₀ ((algebraMap K L : (a : K) → L) (↑x : K) : L)

Tactic:
rw [mem_valuationSubring_iff, ← _root_.map_one vL, ← _root_.map_one (algebraMap K L),
    val_map_le_iff (vR := vK), _root_.map_one]

Premises used: Valuation.HasExtension.val_map_le_iff, Algebra.algebraMap, Valuation.mem_valuationSubring_iff, map_one
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ LE.le.{u_7} (α := Γ₀) ((vK : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)

Tactic:
x.2

Premises used: Set.Mem, setOf, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ LE.le.{u_7} (α := Γ₀) ((vK : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ Eq.{u_6 + 1} (α := L) ((↑((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x) : L) : L)
    ((algebraMap K L : (a : K) → L) (↑x : K) : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR
inst_3 : LinearOrderedCommMonoidWithZero ΓA
inst_4 : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : LinearOrderedCommGroupWithZero Γ₀
inst_9 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_10 : vK.HasExtension vL
⊢ IsScalarTower (↥K₀) K L

Tactic:
inferInstanceAs (IsScalarTower vK.integer K L)

Premises used: _private.0.Valuation.HasExtension.instIsScalarTower_valuationSubring._proof_1
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR
inst_3 : LinearOrderedCommMonoidWithZero ΓA
inst_4 : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : LinearOrderedCommGroupWithZero Γ₀
inst_9 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_10 : vK.HasExtension vL
⊢ IsScalarTower.{u_5, u_6, u_6} (↥K₀) (↥L₀) L

Tactic:
instIsScalarTowerInteger

Premises used: Set.Mem, setOf, Valuation.integer, Valuation.valuationSubring, Valuation.HasExtension.instIsScalarTowerInteger
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR
inst_3 : LinearOrderedCommMonoidWithZero ΓA
inst_4 : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : LinearOrderedCommGroupWithZero Γ₀
inst_9 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_10 : vK.HasExtension vL
⊢ IsLocalHom (R := ↥K₀) (S := ↥L₀) (F := RingHom.{u_5, u_6} ↥K₀ ↥L₀) (algebraMap ↥K₀ ↥L₀)

Tactic:
instIsLocalHomValuationInteger

Premises used: Set.Mem, setOf, Valuation.HasExtension.instIsLocalHomValuationInteger, Valuation.integer, Valuation.valuationSubring
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ Membership.mem.{u_6, u_6} (α := ↥L₀) (γ := Ideal ↥L₀) (maximalIdeal ↥L₀)
      ((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x : ↥L₀) ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x

Tactic:
simp [mem_maximalIdeal, map_mem_nonunits_iff, _root_.mem_nonunits_iff]

Premises used: mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
rw :
  Membership.mem.{u_6, u_6} (α := ↥L₀) (γ := Ideal ↥L₀) (maximalIdeal ↥L₀)
      ((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x : ↥L₀) ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
rw₁ rw₂ : Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x ↔ Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x
⊢ Membership.mem (γ := Ideal ↥K₀)
      (Ideal.comap (F := RingHom.{u_5, u_6} ↥K₀ ↥L₀) (algebraMap ↥K₀ ↥L₀) (maximalIdeal ↥L₀)) x ↔
    Membership.mem (γ := Ideal ↥K₀) (maximalIdeal ↥K₀) x

Tactic:
rw [Ideal.mem_comap, algebraMap_mem_maximalIdeal_iff]

Premises used: Ideal.mem_comap, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR
inst_3 : LinearOrderedCommMonoidWithZero ΓA
inst_4 : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : LinearOrderedCommGroupWithZero Γ₀
inst_9 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_10 : vK.HasExtension vL
⊢ Ideal.LiesOver.{u_5, u_6} (A := ↥K₀) (B := ↥L₀) (maximalIdeal ↥L₀) (maximalIdeal ↥K₀)

Tactic:
⟨(maximalIdeal_comap_algebraMap_eq_maximalIdeal _ _).symm⟩

Premises used: Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, Ideal.LiesOver.mk, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
K : Type u_5
L : Type u_6
Γ₀ : Type u_7
Γ₁ : Type u_8
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : LinearOrderedCommGroupWithZero Γ₀
inst_4 : LinearOrderedCommGroupWithZero Γ₁
vK : Valuation K Γ₀
vL : Valuation L Γ₁
inst_5 : vK.HasExtension vL
x : ↥K₀
⊢ Eq (α := ResidueField ↥L₀)
    ((algebraMap (ResidueField ↥K₀) (ResidueField ↥L₀) : (a : ResidueField ↥K₀) → ResidueField ↥L₀)
        ((residue ↥K₀ : (a : ↥K₀) → ResidueField ↥K₀) x) :
      ResidueField ↥L₀)
    ((residue ↥L₀ : (a : ↥L₀) → ResidueField ↥L₀) ((algebraMap ↥K₀ ↥L₀ : (a : ↥K₀) → ↥L₀) x) : ResidueField ↥L₀)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y : R
hx : Membership.mem (γ := Set R) {x : R | LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)} x
hy : Membership.mem (γ := Set R) {x : R | LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)} y
⊢ Membership.mem (γ := Set R) {x : R | LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)} (x * y)

Tactic:
simp only [Set.mem_setOf_eq, map_mul, mul_le_one' hx hy]

Premises used: Set.mem_setOf_eq, map_mul, mul_le_one'
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ Membership.mem (γ := Set R) {x : R | LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)} 0

Tactic:
simp only [Set.mem_setOf_eq, map_zero, zero_le']

Premises used: map_zero, Set.mem_setOf_eq, zero_le'
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
hx : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Membership.mem (γ := Set R) {x : R | LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀)} (-x)

Tactic:
simpa only [Set.mem_setOf_eq, map_neg]

Premises used: Set.mem_setOf_eq, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
r : R
⊢ r ∈ v.integer ↔ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) (1 : Γ₀)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ v.Integers ↥v.integer

Tactic:
{ hom_inj := Subtype.coe_injective
    map_le_one := fun r => r.2
    exists_of_le_one := fun r hr => ⟨⟨r, hr⟩, rfl⟩ }

Premises used: Subtype.coe_injective, Subtype.mk, Exists.intro, Valuation.Integers.mk, rfl, Subtype.property
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Oˣ
hu : (↑u : O) = x
grw : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) 1 : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
grw₃ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) ((↑u : O) * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₄ :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * (↑u⁻¹ : O)) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₅ :
  (v : (a : R) → Γ₀)
      (HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) x : R)
        ((algebraMap O R : (a : O) → R) (↑u⁻¹ : O) : R)) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₆ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (↑u⁻¹ : O) : R) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₇ grw₈ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)

Tactic:
grw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul, H (u⁻¹ : Units O)]

Premises used: Units.val, Algebra.algebraMap, RingHom.map_one, Units.mul_inv, Valuation.map_mul, Valuation.map_one, Inv.inv, RingHom.map_mul, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit x
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)

Tactic:
one_of_isUnit' hx hv.map_le_one

Premises used: Valuation.Integers.one_of_isUnit', Valuation.Integers.map_le_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
rw : HMul.hMul (α := Γ₀) (β := Γ₀) (1 : Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤ 1
rw₁ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) ≤
    (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R)
rw₂ :
  LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) x : R) (↑u⁻¹ : R)) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₃ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((↑u : R) * (↑u⁻¹ : R)) : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₄ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)
rw₅ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
rw₆ : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)
rw₇ rw₈ : LE.le.{v} (α := Γ₀) 1 1
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)

Tactic:
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]

Premises used: Units.mul_inv, Valuation.map_mul, Valuation.map_one, DFunLike.coe, one_mul
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r1 : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
rw₂ : HMul.hMul (β := R) (↑u : R) ((algebraMap O R : (a : O) → R) r2 : R) = 1
rw₃ : (↑u : R) * (↑u⁻¹ : R) = 1
rw₄ rw₅ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r1 * r2) : R) ((algebraMap O R : (a : O) → R) 1 : R)

Tactic:
rw [map_mul, map_one, hr1, hr2, Units.mul_inv]

Premises used: Units.mul_inv, map_mul, map_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit.{u} (M := R) ((algebraMap O R : (a : O) → R) x : R)
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
u : Rˣ
hu : (↑u : R) = (algebraMap O R : (a : O) → R) x
h1 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u : R) : Γ₀) (1 : Γ₀)
h2 : LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (↑u⁻¹ : R) : Γ₀) (1 : Γ₀)
r1 : O
hr1 : (algebraMap O R : (a : O) → R) r1 = (↑u : R)
r2 : O
hr2 : (algebraMap O R : (a : O) → R) r2 = (↑u⁻¹ : R)
rw :
  HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) =
    (algebraMap O R : (a : O) → R) 1
rw₁ : HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) r2 : R) ((algebraMap O R : (a : O) → R) r1 : R) = 1
rw₂ : HMul.hMul (α := R) ((algebraMap O R : (a : O) → R) r2 : R) (↑u : R) = 1
rw₃ : (↑u⁻¹ : R) * (↑u : R) = 1
rw₄ rw₅ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) (r2 * r1) : R) ((algebraMap O R : (a : O) → R) 1 : R)

Tactic:
rw [map_mul, map_one, hr1, hr2, Units.inv_mul]

Premises used: Units.inv_mul, map_mul, map_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x y : O
h : x ∣ y
obtain :
  ∀ (z : O),
    LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
      ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) y : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)

Tactic:
obtain ⟨z, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
x z : O
grw :
  (v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₁ :
  (v : (a : R) → Γ₀)
      (HMul.hMul (α := R) (β := R) ((algebraMap O R : (a : O) → R) x : R) ((algebraMap O R : (a : O) → R) z : R)) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)
      ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) z : R) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
grw₃ grw₄ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) (x * z) : R) : Γ₀)
    ((v : (a : R) → Γ₀) ((algebraMap O R : (a : O) → R) x : R) : Γ₀)

Tactic:
grw [← mul_one (v (algebraMap O R x)), map_mul, v.map_mul, hv.2 z]

Premises used: Algebra.algebraMap, Valuation.Integers.map_le_one, Valuation.map_mul, map_mul, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
mp : Nontrivial O → Nontrivial R
mpr : Nontrivial R → Nontrivial O
⊢ Nontrivial O ↔ Nontrivial R

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R

Tactic:
hv.hom_inj.nontrivial

Premises used: Function.Injective.nontrivial, Valuation.Integers.hom_inj
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial O
⊢ Nontrivial R

Tactic:
exact hv.hom_inj.nontrivial

Premises used: Function.Injective.nontrivial, Valuation.Integers.hom_inj
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 0 : Γ₀) (1 : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
mpr : ∀ (o0 : O) (ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)), Nontrivial O
⊢ Nontrivial O

Tactic:
obtain ⟨o0, ho0⟩ := hv.exists_of_le_one (r := 0) (by simp)

Premises used: Valuation.Integers.exists_of_le_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
mpr : ∀ (o1 : O) (ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o1 : R) (1 : R)), Nontrivial O
⊢ Nontrivial O

Tactic:
obtain ⟨o1, ho1⟩ := hv.exists_of_le_one (r := 1) (by simp)

Premises used: Valuation.Integers.exists_of_le_one
-- Module: Mathlib.RingTheory.Valuation.Integers
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
o1 : O
ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o1 : R) (1 : R)
⊢ Nontrivial O

Tactic:
⟨o0, o1, ?_⟩

Premises used: Nontrivial.mk, Exists.intro