awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered.{u_1} (ValueGroupWithZero R)
pos : False
pos₁ :
  Set.Subsingleton (α := MonoidWithZeroHom.ValueGroup₀ v)
    (Set.range (ι := ValueGroupWithZero R)
      (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
        (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v))
pos₂ :
  DenselyOrdered
    (↑(Set.range (ι := ValueGroupWithZero R)
          (⇑(MulEquiv.toMonoidWithZeroHom (OrderMonoidIso.toMulEquiv (ValueGroupWithZero.orderMonoidIso v))) :
            (a : ValueGroupWithZero R) → MonoidWithZeroHom.ValueGroup₀ v)) :
      Type)
⊢ IsDiscrete R

Tactic:
classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range

Premises used: ValuativeRel.ValueGroupWithZero.embed_strictMono, MonoidWithZeroHom.range_nontrivial, StrictMono.denselyOrdered_range, WithZero.denselyOrdered_set_iff_subsingleton, ValuativeRel.ValueGroupWithZero.orderMonoidIso, Set.Nontrivial.not_subsingleton, OrderMonoidIso.toMulEquiv, MulEquiv.toMonoidWithZeroHom
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
rw [isNontrivial_iff_nontrivial_units] at h

Premises used: ValuativeRel.isNontrivial_iff_nontrivial_units
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
h₁ : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
⊢ ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)

Tactic:
rw [isNontrivial_iff_nontrivial_units] at h

Premises used: ValuativeRel.isNontrivial_iff_nontrivial_units
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : ¬DenselyOrdered.{u_1} (ValueGroupWithZero R)
⊢ Nonempty.{u_1 + 1} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H

Premises used: LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : Nonempty.{u_1 + 1} (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)

Tactic:
rw [nonempty_orderIso_withZeroMul_int_iff] at H

Premises used: ValuativeRel.nonempty_orderIso_withZeroMul_int_iff
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
H.left

Premises used: And.left
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
H : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean.{u_1} (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
exact H.left

Premises used: And.left
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ ¬Nontrivial.{u_1} (ValueGroupWithZero R)ˣ

Tactic:
rw [isNontrivial_iff_nontrivial_units] at h

Premises used: ValuativeRel.isNontrivial_iff_nontrivial_units
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : ¬Nontrivial.{u_1} (ValueGroupWithZero R)ˣ
⊢ Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R

Tactic:
⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩

Premises used: ValuativeRel.IsDiscrete.mk, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
neg : ∀ (y : ValueGroupWithZero R) (hy : y < 1), y ≤ 0
⊢ IsDiscrete R

Tactic:
refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : y < 1
neg : ∀ (hy : 0 < y), 1 ≤ y
⊢ y ≤ 0

Tactic:
contrapose! hy
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
⊢ 1 = Units.mk0 y ⋯

Tactic:
have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this_1 : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
this : 1 = Units.mk0 y ⋯
⊢ 1 ≤ y

Tactic:
Units.val_le_val.mpr this.le

Premises used: Iff.mpr, Units.val_le_val, Eq.le
-- Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst_2 : v.Compatible
this_1 : IsRankLeOne R
h : Subsingleton.{u_1 + 1} (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
this : 1 = Units.mk0 y ⋯
⊢ 1 ≤ y

Tactic:
exact Units.val_le_val.mpr this.le

Premises used: Iff.mpr, Units.val_le_val, Eq.le
-- 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
inst_5 : vR.HasExtension vA
x y : R
⊢ LE.le.{u_4} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA)
      ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) y : A) : ΓA) ↔
    LE.le.{u_3} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) ((vR : (a : R) → ΓR) y : ΓR)

Tactic:
val_isEquiv_comap.symm x y

Premises used: Valuation.HasExtension.val_isEquiv_comap, Valuation.IsEquiv.symm
-- 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
inst_5 : vR.HasExtension vA
x y : R
⊢ LT.lt.{u_4} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA)
      ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) y : A) : ΓA) ↔
    LT.lt.{u_3} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) ((vR : (a : R) → ΓR) y : ΓR)

Tactic:
simpa only [not_le] using ((val_map_le_iff vR vA _ _).not)

Premises used: not_le, Valuation.HasExtension.val_map_le_iff, Iff.not
-- 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
inst_5 : vR.HasExtension vA
x y : R
⊢ Eq.{u_4 + 1} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA)
      ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) y : A) : ΓA) ↔
    Eq.{u_3 + 1} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) ((vR : (a : R) → ΓR) y : ΓR)

Tactic:
(IsEquiv.eq_iff val_isEquiv_comap).symm

Premises used: Valuation.HasExtension.val_isEquiv_comap, Valuation.IsEquiv.eq_iff, Iff.symm
-- 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
inst_5 : vR.HasExtension vA
x : R
⊢ LE.le.{u_4} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA) (1 : ΓA) ↔
    LE.le.{u_3} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) (1 : ΓR)

Tactic:
simpa only [map_one] using val_map_le_iff vR vA x 1

Premises used: Valuation.HasExtension.val_map_le_iff, map_one, OfNat.ofNat
-- 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
inst_5 : vR.HasExtension vA
x : R
⊢ LT.lt.{u_4} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA) (1 : ΓA) ↔
    LT.lt.{u_3} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) (1 : ΓR)

Tactic:
simpa only [map_one, not_le] using (val_map_le_iff vR vA 1 x).not

Premises used: not_le, Valuation.HasExtension.val_map_le_iff, Iff.not, map_one, OfNat.ofNat
-- 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
inst_5 : vR.HasExtension vA
x : R
⊢ Eq.{u_4 + 1} (α := ΓA) ((vA : (a : A) → ΓA) ((algebraMap R A : (a : R) → A) x : A) : ΓA) (1 : ΓA) ↔
    Eq.{u_3 + 1} (α := ΓR) ((vR : (a : R) → ΓR) x : ΓR) (1 : ΓR)

Tactic:
simpa only [le_antisymm_iff, map_one] using
    and_congr (val_map_le_iff vR vA x 1) (val_map_le_iff vR vA 1 x)

Premises used: Valuation.HasExtension.val_map_le_iff, le_antisymm_iff, map_one, OfNat.ofNat, and_congr
-- 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
⊢ vR.IsEquiv (comap (algebraMap R R) vR)

Tactic:
simp only [Algebra.algebraMap_self, comap_id, IsEquiv.refl]

Premises used: Algebra.algebraMap_self, Valuation.comap_id, Valuation.IsEquiv.refl
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
rw :
  ∀ {x : K},
    LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
      LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
⊢ vK.IsEquiv (comap (algebraMap K A) vA)

Tactic:
rw [isEquiv_iff_val_le_one]

Premises used: Valuation.isEquiv_iff_val_le_one
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
simp_rw : x ∈ vK.integer ↔ Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₁ :
  Membership.mem (γ := Subring K) (Subring.comap (algebraMap K A) vA.integer) x ↔
    Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₂ :
  Membership.mem (α := A) vA.integer (((algebraMap K A : K →+* A) : (a : K) → A) x : A) ↔
    Membership.mem (γ := Subring K) (integer (comap (algebraMap K A) vA)) x
simp_rw₃ :
  LE.le.{u_7} (α := ΓA) ((vA : (a : A) → ΓA) (((algebraMap K A : K →+* A) : (a : K) → A) x : A) : ΓA) (1 : ΓA) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)
⊢ LE.le.{u_8} (α := ΓK) ((vK : (a : K) → ΓK) x : ΓK) (1 : ΓK) ↔
    LE.le.{u_7} (α := ΓA) ((comap (algebraMap K A) vA : (a : K) → ΓA) x : ΓA) (1 : ΓA)

Tactic:
simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]

Premises used: Valuation.comap_apply, Subring.mem_comap, Valuation.mem_integer_iff
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
⊢ ∀ x ∈ vR.integer, Membership.mem (α := A) vA.integer ((algebraMap R A : (a : R) → A) x : A)

Tactic:
simp [Valuation.mem_integer_iff, val_map_le_one_iff vR vA]

Premises used: Valuation.HasExtension.val_map_le_one_iff, Valuation.mem_integer_iff
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst_3 : LinearOrderedCommGroupWithZero ΓR
inst_4 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst_5 : vR.HasExtension vA
r : ↥vR.integer
a : ↥vA.integer
⊢ (↑(r • a) : A) = (↑r : R) • (↑a : A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst_3 : LinearOrderedCommGroupWithZero ΓR
inst_4 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst_5 : vR.HasExtension vA
r : R
hr : r ∈ vR.integer
a : A
ha : a ∈ vA.integer
⊢ Subtype.mk (p := fun (x : R) ↦ x ∈ vR.integer) r hr • Subtype.mk (p := fun (x : A) ↦ x ∈ vA.integer) a ha =
    Subtype.mk (p := fun (x : A) ↦ x ∈ vA.integer) (r • a) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst_3 : LinearOrderedCommGroupWithZero ΓR
inst_4 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst_5 : vR.HasExtension vA
r : ↥vR.integer
⊢ Eq.{u_2 + 1} (α := A) ((↑((algebraMap ↥vR.integer ↥vA.integer : (a : ↥vR.integer) → ↥vA.integer) r) : A) : A)
    ((algebraMap R A : (a : R) → A) (↑r : R) : A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
x : ↥vR.integer
y : ↥vA.integer
z : A
simp :
  HMul.hMul (α := ↥vA.integer) ((algebraMap ↥vR.integer ↥vA.integer : (a : ↥vR.integer) → ↥vA.integer) x : ↥vA.integer)
        y •
      z =
    HMul.hMul (α := A) ((algebraMap (↥vR.integer) A : (a : ↥vR.integer) → A) x : A) (y • z)
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
x : ↥vR.integer
y : ↥vA.integer
z : A
⊢ HMul.hMul (α := ↥vA.integer) ((algebraMap ↥vR.integer ↥vA.integer : (a : ↥vR.integer) → ↥vA.integer) x : ↥vA.integer)
        y •
      z =
    HMul.hMul (α := A) ((algebraMap (↥vR.integer) A : (a : ↥vR.integer) → A) x : A) (y • z)

Tactic:
mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
x : ↥vR.integer
y : ↥vA.integer
z : A
⊢ HMul.hMul (α := ↥vA.integer) ((algebraMap ↥vR.integer ↥vA.integer : (a : ↥vR.integer) → ↥vA.integer) x : ↥vA.integer)
        y •
      z =
    HMul.hMul (α := A) ((algebraMap (↥vR.integer) A : (a : ↥vR.integer) → A) x : A) (y • z)

Tactic:
exact mul_assoc _ _ _

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
R : Type u_1
A : Type u_2
ΓR_1 : Type u_3
ΓA_1 : Type u_4
inst : CommRing R
inst_1 : Ring A
inst_2 : LinearOrderedCommMonoidWithZero ΓR_1
inst_3 : LinearOrderedCommMonoidWithZero ΓA_1
inst_4 : Algebra R A
vR_1 : Valuation R ΓR_1
vA_1 : Valuation A ΓA_1
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst_7 : LinearOrderedCommGroupWithZero ΓR
inst_8 : LinearOrderedCommGroupWithZero ΓK
inst_9 : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_10 : vR.HasExtension vA
inst_11 : IsDomain R
inst_12 : IsTorsionFree R A
⊢ ∀ (r : ↥vR.integer) (m : ↥vA.integer), r • m = 0 → r = 0 ∨ m = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Extension
Goal:
A : Type u_2
inst : Ring A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst_3 : LinearOrderedCommGroupWithZero ΓK
inst_4 : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst_5 : vK.HasExtension vA
inst_6 : Nontrivial A
⊢ Function.Injective.{u_5 + 1, u_2 + 1} (α := ↥vK.integer) (β := ↥vA.integer)
    (⇑(algebraMap ↥vK.integer ↥vA.integer) : (a : ↥vK.integer) → ↥vA.integer)

Tactic:
FaithfulSMul.algebraMap_injective _ _

Premises used: FaithfulSMul.algebraMap_injective
-- 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 :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
hx : IsUnit (M := R) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R)
hvx :
  Eq.{u_6 + 1} (α := ΓR) ((vR : (a : R) → ΓR) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R) : ΓR)
    (1 : ΓR)
⊢ IsUnit r

Tactic:
apply (Valuation.integer.integers (v := vR)).isUnit_of_one

Premises used: Valuation.integer.integers, Valuation.Integers.isUnit_of_one
-- 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 :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
⊢ IsUnit (M := R) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R)

Tactic:
(isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))

Premises used: Algebra.algebraMap, isUnit_map_iff, Iff.mp, IsUnit.map
-- 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 :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
⊢ IsUnit (M := R) ((algebraMap (↥vR.integer) R : (a : ↥vR.integer) → R) r : R)

Tactic:
exact (isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))

Premises used: Algebra.algebraMap, isUnit_map_iff, Iff.mp, IsUnit.map
-- 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 :
  IsUnit.{u_9} (M := ↥vS.integer)
    ((algebraMap ↥vR.integer ↥vS.integer : (a : ↥vR.integer) → ↥vS.integer) r : ↥vS.integer)
⊢ 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)

Tactic:
apply (Valuation.integer.integers (v := vS)).one_of_isUnit at hr

Premises used: Valuation.integer.integers, Valuation.Integers.one_of_isUnit