awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
neg : IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ∀ (ha : (v : (a : hat K) → Γ₀) a = γ), ∃ (a : K), (v : (a : K) → Γ₀) a = γ}

Tactic:
simp only [H, imp_false]

Premises used: imp_false
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
neg :
  ∀ (H : ¬∃ (x : K), Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)),
    IsClosed.{u_1} (X := hat K) {a : hat K | ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) a : Γ₀) (0 : Γ₀)}
neg₁ : ∀ (hγ : γ ≠ 0), IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}

Tactic:
rcases eq_or_ne γ 0 with rfl | hγ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
H : ¬∃ (x : K), Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬Eq.{u_2 + 1} (α := Γ₀) ((v : (a : hat K) → Γ₀) a : Γ₀) (0 : Γ₀)}

Tactic:
simp at H
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
neg :
  ∀ (r : hat K) (hr : (v : (a : hat K) → Γ₀) r = γ),
    IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}

Tactic:
obtain ⟨r, hr⟩ := h γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
erw : ¬γ = 0
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)

Tactic:
erw [ne_eq, ← embedding_strictMono.injective.eq_iff, embedding_restrict₀ r, hr,
              map_zero]

Premises used: Function.Injective.eq_iff, map_zero, ne_eq, StrictMono.injective, MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
⊢ ¬γ = 0

Tactic:
hγ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
⊢ ¬γ = 0

Tactic:
exact hγ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
⊢ Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)

Tactic:
have hr' : restrict₀ valuedCompletion.v r ≠ 0 := by
            erw [ne_eq, ← embedding_strictMono.injective.eq_iff, embedding_restrict₀ r, hr,
              map_zero]
            exact hγ
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
⊢ IsClosed.{u_1} (X := hat K)
    (univ \
      {x : hat K |
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          (((restrict₀ v :
                  MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                (a : hat K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})

Tactic:
isClosed_univ.sdiff (isOpen_sphere (hat K) hr')

Premises used: isClosed_univ, Valued.isOpen_sphere, IsClosed.sdiff, UniformSpace.Completion
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
h₁ :
  Eq.{u_1 + 1} (α := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
    (univ \
      {x : hat K |
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          (((restrict₀ v :
                  MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                (a : hat K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
⊢ IsClosed.{u_1} (X := hat K) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}

Tactic:
convert! isClosed_univ.sdiff (isOpen_sphere (hat K) hr') using 1

Premises used: isClosed_univ, Valued.isOpen_sphere, IsClosed.sdiff, UniformSpace.Completion
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
h₁ :
  ∀ (x : hat K),
    Membership.mem (γ := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ} x ↔
      Membership.mem (γ := Set (hat K))
        (univ \
          {x : hat K |
            Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
              ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
                ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
              (((restrict₀ v :
                      MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                    (a : hat K) → ValueGroup₀ v)
                  r :
                ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
        x
⊢ Eq.{u_1 + 1} (α := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ}
    (univ \
      {x : hat K |
        Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
            ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
          (((restrict₀ v :
                  MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                (a : hat K) → ValueGroup₀ v)
              r :
            ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
H : ¬∃ (x : K), (v : (a : K) → Γ₀) x = γ
hγ : γ ≠ 0
r : hat K
hr : (v : (a : hat K) → Γ₀) r = γ
hr' :
  Ne.{u_2 + 1} (α := ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (((restrict₀ v : MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
          (a : hat K) → ValueGroup₀ v)
        r :
      ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
    (0 : ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)
x : hat K
⊢ Membership.mem (γ := Set (hat K)) {a : hat K | ¬(v : (a : hat K) → Γ₀) a = γ} x ↔
    Membership.mem (γ := Set (hat K))
      (univ \
        {x : hat K |
          Eq.{u_2 + 1} (α := ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
            ((Valuation.restrict v : (a : hat K) → ValueGroup₀ (↑v : hat K →*₀ Γ₀)) x :
              ValueGroup₀ (F := MonoidWithZeroHom.{u_1, u_2} (hat K) Γ₀) (↑v : hat K →*₀ Γ₀))
            (((restrict₀ v :
                    MonoidWithZeroHom.{u_1, u_2} (hat K) (ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)) :
                  (a : hat K) → ValueGroup₀ v)
                r :
              ValueGroup₀ (F := Valuation.{u_1, u_2} (hat K) Γ₀) v)})
      x

Tactic:
simp only [← hr, mem_setOf_eq, mem_diff, mem_univ, true_and, ← v.restrict_def,
            v.restrict_inj]

Premises used: Valued.v, Set.mem_setOf_eq, Valuation.restrict_inj, Valuation.restrict_def, Set.mem_diff, Set.mem_univ, true_and
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
a : K
ha : (v : (a : hat K) → Γ₀) (↑a : hat K) = γ
⊢ (v : (a : K) → Γ₀) a = γ

Tactic:
simpa using ha
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := hat K) (β := Γ₀) (⇑v : (a : hat K) → Γ₀)
γ : Γ₀
a : K
ha : (v : (a : hat K) → Γ₀) (↑a : hat K) = γ
⊢ ∃ (a : K), (v : (a : K) → Γ₀) a = γ

Tactic:
exact ⟨_, by simpa using ha⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
a : K
ha : (v : (a : K) → Γ₀) a = γ
⊢ (v : (a : hat K) → Γ₀) (↑a : hat K) = γ

Tactic:
simp [ha]
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := K) (β := Γ₀) (⇑v : (a : K) → Γ₀)
γ : Γ₀
a : K
ha : (v : (a : K) → Γ₀) a = γ
⊢ ∃ (a : hat K), (v : (a : hat K) → Γ₀) a = γ

Tactic:
exact ⟨a, by simp [ha]⟩
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Algebra R K
inst_4 : UniformContinuousConstSMul R K
inst_5 : FaithfulSMul R K
rw : Function.Injective.{u_3 + 1, u_1 + 1} (α := R) (β := hat K) (⇑(algebraMap R (hat K)) : (a : R) → hat K)
⊢ FaithfulSMul.{u_3, u_1} R (hat K)

Tactic:
rw [faithfulSMul_iff_algebraMap_injective R (hat K)]

Premises used: faithfulSMul_iff_algebraMap_injective, UniformSpace.Completion
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Algebra R K
inst_4 : UniformContinuousConstSMul R K
inst_5 : FaithfulSMul R K
⊢ Function.Injective.{u_3 + 1, u_1 + 1} (α := R) (β := hat K) (⇑(algebraMap R (hat K)) : (a : R) → hat K)

Tactic:
(FaithfulSMul.algebraMap_injective K (hat K)).comp (FaithfulSMul.algebraMap_injective R K)

Premises used: Function.Injective.comp, FaithfulSMul.algebraMap_injective, UniformSpace.Completion
-- Module: Mathlib.Topology.Algebra.Valued.ValuedField
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Algebra R K
inst_4 : UniformContinuousConstSMul R K
inst_5 : FaithfulSMul R K
⊢ Function.Injective.{u_3 + 1, u_1 + 1} (α := R) (β := hat K) (⇑(algebraMap R (hat K)) : (a : R) → hat K)

Tactic:
exact (FaithfulSMul.algebraMap_injective K (hat K)).comp (FaithfulSMul.algebraMap_injective R K)

Premises used: Function.Injective.comp, FaithfulSMul.algebraMap_injective, UniformSpace.Completion
-- 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
⊢ (toVal v x).ofVal = 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 Γ₀
x : WithVal v
⊢ toVal v x.ofVal = 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 Γ₀
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := WithVal v) ofVal

Tactic:
Function.RightInverse.surjective <| ofVal_toVal _

Premises used: WithVal.ofVal_toVal, Function.RightInverse.surjective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Function.Surjective (toVal v)

Tactic:
Function.RightInverse.surjective <| toVal_ofVal _

Premises used: WithVal.toVal_ofVal, Function.RightInverse.surjective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := WithVal v) ofVal

Tactic:
Function.LeftInverse.injective <| toVal_ofVal _

Premises used: Function.LeftInverse.injective, WithVal.toVal_ofVal
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Function.Injective (toVal v)

Tactic:
Function.LeftInverse.injective <| ofVal_toVal _

Premises used: Function.LeftInverse.injective, WithVal.ofVal_toVal
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := WithVal v) ofVal

Tactic:
⟨ofVal_injective v, ofVal_surjective v⟩

Premises used: WithVal.ofVal_injective, WithVal.ofVal_surjective, And.intro, Function.Bijective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ Function.Bijective (toVal v)

Tactic:
⟨toVal_injective v, toVal_surjective v⟩

Premises used: WithVal.toVal_surjective, And.intro, Function.Bijective, WithVal.toVal_injective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ toVal v 0 = 0

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 Γ₀
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) 0) 0

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 Γ₀
⊢ toVal v 1 = 1

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 Γ₀
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) 1) 1

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 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring R
v : Valuation R Γ₀
x : R
n : ℕ
⊢ toVal v (x ^ n) = toVal v x ^ n

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 : WithVal v
n : ℕ
⊢ (x ^ n).ofVal = x.ofVal ^ n

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
r : R
⊢ toVal v (s • r) = s • toVal 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 Γ₀
S : Type u_3
inst_2 : SMul S R
s : S
x : WithVal v
⊢ (s • x).ofVal = 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 Γ₀
n : ℕ
⊢ toVal v (↑n : R) = (↑n : 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 : Ring R
v : Valuation R Γ₀
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) (↑n : WithVal v)) (↑n : 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 Γ₀
z : ℤ
⊢ toVal v (↑z : R) = (↑z : 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 : Ring R
v : Valuation R Γ₀
z : ℤ
⊢ Eq.{u_1 + 1} (α := R) (ofVal.{u_1, u_2} (Γ₀ := Γ₀) (v := v) (↑z : WithVal v)) (↑z : 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 Γ₀
a b : WithVal v
⊢ a ≤ b ↔ LE.le.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) a.ofVal : Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
a b : WithVal v
⊢ a < b ↔ LT.lt.{u_2} (α := Γ₀) ((v : (a : R) → Γ₀) a.ofVal : Γ₀) ((v : (a : R) → Γ₀) b.ofVal : Γ₀)

Tactic:
.rfl

Premises used: Iff.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
⊢ toVal v x = 0 ↔ x = 0

Tactic:
(toVal_injective v).eq_iff

Premises used: Function.Injective.eq_iff, WithVal.toVal_injective
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
x : WithVal v
⊢ x.ofVal = 0 ↔ x = 0

Tactic:
(ofVal_injective v).eq_iff

Premises used: WithVal.ofVal_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Algebra.Valued.WithVal
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
inst_1 : Ring R
v : Valuation R Γ₀
⊢ map v v (RingHom.id R) = RingHom.id (WithVal v)

Tactic:
rfl

Premises used: WithVal.map, rfl