awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
T : Type u_5
inst_4 : Ring T
u : Valuation T Γ₀
f : S →+* T
g : R →+* S
⊢ map v u (f.comp g) = (map w u f).comp (map v w g)

Tactic:
rfl

Premises used: MulEquiv.toMonoidHom, RingEquiv.toRingHom, WithVal.map, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R →+* S
x : WithVal v
⊢ (map v w f : (a : WithVal v) → WithVal w) x = toVal w ((f : (a : R) → S) x.ofVal)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x : WithVal v
⊢ (map w v f.symm.toRingHom : (a : WithVal w) → WithVal v)
      ((↑(↑(map v w f.toRingHom) : WithVal v →* WithVal w) : OneHom (WithVal v) (WithVal w)).toFun x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x : WithVal w
⊢ (↑(↑(map v w f.toRingHom) : WithVal v →* WithVal w) : OneHom (WithVal v) (WithVal w)).toFun
      ((map w v f.symm.toRingHom : (a : WithVal w) → WithVal v) x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ congr v v (RingEquiv.refl R) = RingEquiv.refl (WithVal v)

Tactic:
rfl

Premises used: RingEquiv.refl, Equiv.refl, WithVal.congr, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
⊢ (congr v w f).symm = congr w v f.symm

Tactic:
rfl

Premises used: Equiv.symm, WithVal.congr, RingEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
T : Type u_5
inst_4 : Ring T
u : Valuation T Γ₀
f : R ≃+* S
g : S ≃+* T
⊢ congr v u (f.trans g) = (congr v w f).trans (congr w u g)

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.trans, WithVal.congr, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x : WithVal v
⊢ (congr v w f : (a : WithVal v) → WithVal w) x = toVal w ((f : (a : R) → S) x.ofVal)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x : WithVal w
⊢ ((congr v w f).symm : (a : WithVal w) → WithVal v) x = toVal v ((f.symm : (a : S) → R) x.ofVal)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
x : R
⊢ Eq.{u_2 + 1} (α := Γ₀) ((valuation v : (a : WithVal v) → Γ₀) (toVal v x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
r : WithVal v
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) r.ofVal : Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
r : WithVal v
⊢ Eq.{u_2 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((equiv v : (a : WithVal v) → R) r : R) : Γ₀)
    ((Valued.v : (a : WithVal v) → Γ₀) r : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
r : R
⊢ Eq.{u_2 + 1} (α := Γ₀) ((Valued.v : (a : WithVal v) → Γ₀) (toVal v r) : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
Λ₀ : Type u_4
inst_3 : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
inst_4 : CharZero R
⊢ Eq (α := WithVal v) (((equiv v).symm.toAddMonoidHom : (a : R) → WithVal v) 1 : WithVal v) (1 : WithVal v)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : CommRing R
v : Valuation R Γ₀
⊢ (valuation v).Compatible

Tactic:
.ofValuation (valuation v)

Premises used: Valuation.Compatible.ofValuation, WithVal.valuation
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul R S
x : WithVal v
s : S
⊢ x • s = x.ofVal • s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul S R
s : S
x : WithVal v
⊢ s • x = toVal v (s • x.ofVal)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul S R
inst_3 : FaithfulSMul S R
m₁ m₂ : S
h : ∀ (a : WithVal v), m₁ • a = m₂ • a
⊢ ∀ (a : WithVal v), m₁ • a.ofVal = m₂ • a.ofVal

Tactic:
simp only [smul_right_def, toVal.injEq] at h

Premises used: WithVal.toVal.injEq, WithVal.smul_right_def
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul S R
inst_3 : FaithfulSMul S R
m₁ m₂ : S
h : ∀ (a : WithVal v), m₁ • a.ofVal = m₂ • a.ofVal
⊢ m₁ = m₂

Tactic:
FaithfulSMul.eq_of_smul_eq_smul fun r ↦ h (toVal v r)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, WithVal.toVal
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : SMul S R
inst_3 : FaithfulSMul S R
m₁ m₂ : S
h : ∀ (a : WithVal v), m₁ • a.ofVal = m₂ • a.ofVal
⊢ m₁ = m₂

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul fun r ↦ h (toVal v r)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, WithVal.toVal
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v_1 : Valuation R Γ₀
S : Type u_3
P : Type u_4
inst_2 : SMul S P
inst_3 : SMul R S
inst_4 : SMul R P
inst_5 : IsScalarTower R S P
v : Valuation R Γ₀
⊢ ∀ (x : WithVal v) (y : S) (z : P), (x • y) • z = x • y • z

Tactic:
simp [smul_left_def]

Premises used: WithVal.smul_left_def
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v_1 : Valuation R Γ₀
S : Type u_3
P : Type u_4
inst_2 : Ring S
inst_3 : SMul P S
inst_4 : SMul R S
inst_5 : SMul P R
inst_6 : IsScalarTower P R S
v : Valuation S Γ₀
⊢ IsScalarTower.{u_4, u_1, u_3} P R (WithVal v)

Tactic:
(equiv v).isScalarTower P R

Premises used: RingEquiv.toEquiv, WithVal.equiv, Equiv.isScalarTower
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v_1 : Valuation R Γ₀
S : Type u_3
P : Type u_4
inst_2 : Ring S
inst_3 : SMul P R
inst_4 : SMul S R
inst_5 : SMul P S
inst_6 : IsScalarTower P S R
v : Valuation S Γ₀
⊢ ∀ (x : P) (y : WithVal v) (z : R), (x • y) • z = x • y • z

Tactic:
simp [smul_right_def, smul_left_def, - toVal_smul]

Premises used: WithVal.toVal_smul, WithVal.smul_right_def, WithVal.smul_left_def
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
S : Type u_3
inst_2 : AddCommMonoid S
inst_3 : Module R S
inst_4 : Module.Finite R S
⊢ Module.Finite.{u_1, u_3} (WithVal v) S

Tactic:
.of_restrictScalars_finite R (WithVal v) S

Premises used: Module.Finite.of_restrictScalars_finite, WithVal
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
S : Type u_3
inst_2 : Ring S
inst_3 : Module R S
v : Valuation S Γ₀
x : WithVal v
⊢ (linearEquiv R v : (a : WithVal v) → S) x = x.ofVal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
S : Type u_3
inst_2 : Ring S
inst_3 : Module R S
v : Valuation S Γ₀
x : S
⊢ (LinearEquiv.symm (linearEquiv R v) : (a : S) → WithVal v) x = toVal v x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v_1 : Valuation R Γ₀
S : Type u_3
inst_2 : Ring S
inst_3 : Module R S
v : Valuation S Γ₀
inst_4 : Module.Finite R S
⊢ Module.Finite.{u_1, u_3} R (WithVal v)

Tactic:
.equiv (linearEquiv R v).symm

Premises used: LinearEquiv.symm, WithVal.linearEquiv, Module.Finite.equiv
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommRing R
v : Valuation R Γ₀
inst_2 : Semiring S
inst_3 : Algebra R S
s : WithVal v
⊢ Eq.{u_3 + 1} (α := S) ((algebraMap (WithVal v) S : (a : WithVal v) → S) s : S)
    ((algebraMap R S : (a : R) → S) s.ofVal : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S_1 : Type u_3
inst_1 : CommRing R
v : Valuation R Γ₀
inst_2 : Semiring S_1
inst_3 : Algebra R S_1
S : Type u_4
inst_4 : CommSemiring S
inst_5 : Algebra R S
i : IsFractionRing R S
⊢ IsFractionRing.{u_1, u_4} (WithVal v) S

Tactic:
.of_ringEquiv_left (equiv v) (fun _ ↦ rfl)

Premises used: IsFractionRing.of_ringEquiv_left, WithVal.equiv, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommRing R
v : Valuation R Γ₀
inst_2 : Semiring S
inst_3 : Algebra R S
h : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := WithVal v) (β := S) (⇑(algebraMap (WithVal v) S) : (a : WithVal v) → S)

Tactic:
h.comp (ofVal_injective v)

Premises used: WithVal.ofVal_injective, Function.Injective.comp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommSemiring R
inst_2 : Ring S
inst_3 : Algebra R S
v : Valuation S Γ₀
r : R
⊢ (algebraMap R (WithVal v) : (a : R) → WithVal v) r = toVal v ((algebraMap R S : (a : R) → S) r)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommSemiring R
inst_2 : Ring S
inst_3 : Algebra R S
v : Valuation S Γ₀
h : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := WithVal v) (⇑(algebraMap R (WithVal v)) : (a : R) → WithVal v)

Tactic:
(toVal_injective v).comp h

Premises used: Function.Injective.comp, WithVal.toVal_injective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommSemiring R
inst_2 : Ring S
inst_3 : Algebra R S
v : Valuation S Γ₀
x : WithVal v
⊢ (algEquiv R v : (a : WithVal v) → S) x = x.ofVal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S : Type u_3
inst_1 : CommSemiring R
inst_2 : Ring S
inst_3 : Algebra R S
v : Valuation S Γ₀
x : S
⊢ (AlgEquiv.symm (algEquiv R v) : (a : S) → WithVal v) x = toVal v x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
S_1 : Type u_3
inst_1 : CommSemiring R
inst_2 : Ring S_1
inst_3 : Algebra R S_1
v_1 : Valuation S_1 Γ₀
S : Type u_4
inst_4 : CommRing S
inst_5 : Algebra R S
M : Submonoid R
inst_6 : IsLocalization M S
v : Valuation S Γ₀
rwa rwa₁ rwa₂ rwa₃ : IsLocalization M S
⊢ IsLocalization.{u_1, u_4} M (WithVal v)

Tactic:
rwa [← IsLocalization.isLocalization_iff_of_algEquiv M (algEquiv R v).symm]

Premises used: AlgEquiv.symm, IsLocalization.isLocalization_iff_of_algEquiv, WithVal.algEquiv
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x y : R
⊢ toVal v (x / y) = toVal v x / toVal v y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x y : WithVal v
⊢ (x / y).ofVal = x.ofVal / y.ofVal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x : R
⊢ toVal v x⁻¹ = (toVal v x)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x : WithVal v
⊢ x⁻¹.ofVal = x.ofVal⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x : R
z : ℤ
⊢ toVal v (x ^ z) = toVal v x ^ z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
x : WithVal v
z : ℤ
⊢ (x ^ z).ofVal = x.ofVal ^ z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
q : ℚ≥0
⊢ toVal v (↑q : R) = (↑q : WithVal v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) (↑q : WithVal v)) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
q : ℚ
⊢ toVal v (↑q : R) = (↑q : WithVal v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Field R
v : Valuation R Γ₀
q : ℚ
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) (↑q : WithVal v)) (↑q : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
Γ'₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation R Γ₀
w : Valuation R Γ'₀
⊢ (congr v w (RingEquiv.refl R)).symm = congr w v (RingEquiv.refl R)

Tactic:
rfl

Premises used: Equiv.symm, WithVal.congr, RingEquiv.symm, rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
Γ'₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation R Γ₀
w : Valuation R Γ'₀
x : WithVal v
⊢ Eq (α := WithVal w) ((congr v w (RingEquiv.refl R) : (a : WithVal v) → WithVal w) x : WithVal w)
    (((equiv w).symm : (a : R) → WithVal w) ((equiv v : (a : WithVal v) → R) x : R) : WithVal w)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
Γ'₀ : Type u_3
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation R Γ₀
w : Valuation R Γ'₀
x : WithVal w
⊢ Eq (α := WithVal v) (((congr v w (RingEquiv.refl R)).symm : (a : WithVal w) → WithVal v) x : WithVal v)
    (((equiv v).symm : (a : R) → WithVal v) ((equiv w : (a : WithVal w) → R) x : R) : WithVal v)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
simp :
  Eq.{u_2 + 1} (α := Subgroup Γ₀ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) (⇑Valued.v : (a : WithVal v) → Γ₀)))
    (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) ((⇑v : (a : R) → Γ₀) ∘ ofVal)))
⊢ Eq (α := Subgroup Γ₀ˣ) (valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) (valueGroup v)

Tactic:
simp [valueGroup, valueMonoid, ← (WithVal.ofVal_surjective v).range_comp]

Premises used: Function.Surjective.range_comp, WithVal.ofVal_surjective, MonoidWithZeroHom.valueGroup, MonoidWithZeroHom.valueMonoid
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Eq.{u_2 + 1} (α := Subgroup Γ₀ˣ)
    (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) (⇑Valued.v : (a : WithVal v) → Γ₀)))
    (Subgroup.closure (Units.val ⁻¹' Set.range.{u_2, u_3 + 1} (ι := WithVal v) ((⇑v : (a : R) → Γ₀) ∘ ofVal)))

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ (↑(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) : Set Γ₀ˣ) = (↑(valueGroup v) : Set Γ₀ˣ)

Tactic:
simp [valueGroup_eq v]

Premises used: WithVal.valueGroup_eq
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
⊢ ∀ (x y : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)),
    (Equiv.setCongr (s := (↑(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) : Set Γ₀ˣ)) (t :=
            (↑(valueGroup v) : Set Γ₀ˣ)) ⋯).toFun
        (x * y) =
      (Equiv.setCongr (s := (↑(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) : Set Γ₀ˣ)) (t :=
              (↑(valueGroup v) : Set Γ₀ˣ)) ⋯).toFun
          x *
        (Equiv.setCongr (s := (↑(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v) : Set Γ₀ˣ)) (t :=
              (↑(valueGroup v) : Set Γ₀ˣ)) ⋯).toFun
          y

Tactic:
simp [Equiv.setCongr, Equiv.subtypeEquivProp]

Premises used: Equiv.setCongr, Equiv.subtypeEquivProp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
x x_1 : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
h : x < x_1
⊢ LT.lt (α := ↥(valueGroup v))
    ((valueGroupEquiv v : (a : ↥(valueGroup Valued.v)) → ↥(valueGroup v)) x : ↥(valueGroup v))
    ((valueGroupEquiv v : (a : ↥(valueGroup Valued.v)) → ↥(valueGroup v)) x_1 : ↥(valueGroup v))

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
x x_1 : ↥(valueGroup v)
h : x < x_1
⊢ LT.lt (α := ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (((valueGroupEquiv v).symm : (a : ↥(valueGroup v)) → ↥(valueGroup Valued.v)) x :
      ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (((valueGroupEquiv v).symm : (a : ↥(valueGroup v)) → ↥(valueGroup Valued.v)) x_1 :
      ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
x : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
⊢ Eq (α := ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
    ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
          (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
        ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
              (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
            0 :
          WithZero ↥(valueGroup v)) :
      WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v))
    (0 : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
x : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
a : ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)
⊢ (WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
        (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          (↑a : WithZero ↥(valueGroup Valued.v)) :
        WithZero ↥(valueGroup v)) =
    (↑a : WithZero ↥(valueGroup Valued.v))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
x : ValueGroup₀ (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v
⊢ (WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
        (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
      ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
            (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
          x :
        WithZero ↥(valueGroup v)) =
    x

Tactic:
match x with
    | 0 => simp
    | .coe a => simp
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R_1 : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst_1 : Ring R
v : Valuation R Γ₀
y : ValueGroup₀ v
⊢ Eq (α := ValueGroup₀ v)
    ((WithZero.map' (↑(valueGroupEquiv v) : ↥(valueGroup Valued.v) →* ↥(valueGroup v)) :
          (a : WithZero ↥(valueGroup Valued.v)) → WithZero ↥(valueGroup v))
        ((WithZero.map' (↑(valueGroupEquiv v).symm : ↥(valueGroup v) →* ↥(valueGroup Valued.v)) :
              (a : WithZero ↥(valueGroup v)) → WithZero ↥(valueGroup Valued.v))
            0 :
          WithZero ↥(valueGroup (F := Valuation.{u_3, u_2} (WithVal v) Γ₀) Valued.v)) :
      WithZero ↥(valueGroup v))
    (0 : ValueGroup₀ v)

Tactic:
simp