awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) :=
  Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
convert_3 :
  (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Eq (α := HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A))
      ((π : (a : ↥A) → ↥A ⧸ IsLocalRing.maximalIdeal ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A))
      1
⊢ (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Eq.{u + 1} (α := IsLocalRing.ResidueField ↥A)
      (↑((Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A) :
              (a : (↥A)ˣ) → (IsLocalRing.ResidueField ↥A)ˣ)
            ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x)) :
        IsLocalRing.ResidueField ↥A)
      (↑1 : IsLocalRing.ResidueField ↥A)

Tactic:
convert_to _ ↔ π _ = 1

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) :=
  Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
convert_3 :
  (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    LT.lt (α := A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup)
          (↑(HSub.hSub (α := ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A) 1) : K) :
        A.ValueGroup)
      (1 : A.ValueGroup)
⊢ (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    Eq (α := HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A))
      ((π : (a : ↥A) → ↥A ⧸ IsLocalRing.maximalIdeal ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A))
      1

Tactic:
rw [← π.map_one, ← sub_eq_zero, ← π.map_sub, Ideal.Quotient.eq_zero_iff_mem, valuation_lt_one_iff]

Premises used: ValuationSubring.valuation_lt_one_iff, sub_eq_zero, RingHom.map_one, RingHom.map_sub, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* HasQuotient.Quotient ↥A (B := Ideal ↥A) (IsLocalRing.maximalIdeal ↥A) :=
  Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ (↑x : Kˣ) ∈ A.principalUnitGroup ↔
    LT.lt (α := A.ValueGroup)
      ((A.valuation : (a : K) → A.ValueGroup)
          (↑(HSub.hSub (α := ↥A) (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A) 1) : K) :
        A.ValueGroup)
      (1 : A.ValueGroup)

Tactic:
simp [mem_principalUnitGroup_iff]

Premises used: ValuationSubring.mem_principalUnitGroup_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x :
  ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
rw :
  Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
    (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
    ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ)
        ((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) :
      (↥A)ˣ)
⊢ (↑((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) : Kˣ) ∈ A.principalUnitGroup

Tactic:
rw [A.coe_mem_principalUnitGroup_iff]

Premises used: ValuationSubring.coe_mem_principalUnitGroup_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x :
  ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
⊢ Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
    (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
    ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ)
        ((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) :
      (↥A)ˣ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.principalUnitGroup
⊢ (fun
          (x :
            ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
                (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))) ↦
        Subtype.mk (p := fun (x : Kˣ) ↦ x ∈ A.principalUnitGroup)
          (↑((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) : Kˣ) ⋯)
      ((fun (x : ↥A.principalUnitGroup) ↦
          (Subtype.mk (p := fun (x : (↥A)ˣ) ↦
              Membership.mem (γ := Subgroup (↥A)ˣ)
                (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
                  (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
                x)
              ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ)
                (Subtype.mk (p := fun (x : Kˣ) ↦ x ∈ A.unitGroup) (↑x : Kˣ) ⋯))
              ⋯ :
            ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
                (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x :
  ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
⊢ (fun (x : ↥A.principalUnitGroup) ↦
        (Subtype.mk (p := fun (x : (↥A)ˣ) ↦
            Membership.mem (γ := Subgroup (↥A)ˣ)
              (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
                (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
              x)
            ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ)
              (Subtype.mk (p := fun (x : Kˣ) ↦ x ∈ A.unitGroup) (↑x : Kˣ) ⋯))
            ⋯ :
          ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
              (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))))
      ((fun
            (x :
              ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
                  (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))) ↦
          Subtype.mk (p := fun (x : Kˣ) ↦ x ∈ A.principalUnitGroup)
            (↑((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) : Kˣ) ⋯)
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : ↥A.principalUnitGroup
⊢ (↑(↑(↑((A.principalUnitGroupEquiv :
                    (a : ↥A.principalUnitGroup) →
                      ↥(Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)).ker)
                  a) :
              (↥A)ˣ) :
          ↥A) :
      K) =
    (↑(↑a : Kˣ) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a :
  ↥(MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)))
⊢ (↑(↑((A.principalUnitGroupEquiv.symm :
                (a : ↥(Units.map (↑(IsLocalRing.residue ↥A) : ↥A →* IsLocalRing.ResidueField ↥A)).ker) →
                  ↥A.principalUnitGroup)
              a) :
          Kˣ) :
      K) =
    (↑(↑(↑a : (↥A)ˣ) : ↥A) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ Eq.{u + 1} (α := IsLocalRing.ResidueField ↥A)
    (↑((A.unitGroupToResidueFieldUnits : (a : ↥A.unitGroup) → (IsLocalRing.ResidueField ↥A)ˣ) x) :
      IsLocalRing.ResidueField ↥A)
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A) : (a : ↥A) → ↥A ⧸ IsLocalRing.maximalIdeal ↥A)
      (↑((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x) : ↥A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
h :
  ∀ (x : ↥A.unitGroup),
    x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
⊢ A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup

Tactic:
ext
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Function.Surjective (α := ↥A.unitGroup) (β := (IsLocalRing.ResidueField ↥A)ˣ)
    (⇑A.unitGroupToResidueFieldUnits : (a : ↥A.unitGroup) → (IsLocalRing.ResidueField ↥A)ˣ)

Tactic:
IsLocalRing.surjective_units_map_of_local_ringHom _ Ideal.Quotient.mk_surjective
    (inferInstanceAs (IsLocalHom (IsLocalRing.residue A))) |>.comp (MulEquiv.surjective _)

Premises used: MulEquiv.surjective, Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField, IsLocalRing.surjective_units_map_of_local_ringHom, Function.Surjective.comp
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ MonoidHom.comp
      (↑A.unitsModPrincipalUnitsEquivResidueFieldUnits :
        ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup →* (IsLocalRing.ResidueField ↥A)ˣ)
      (QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) =
    A.unitGroupToResidueFieldUnits

Tactic:
rfl

Premises used: MonoidHom.mk', Quotient.liftOn', Quotient, Con.liftOn, ValuationSubring.unitGroupToResidueFieldUnits, rfl, Units.map
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ Eq (α := (IsLocalRing.ResidueField ↥A)ˣ)
    ((A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom :
          (a : ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup) → (IsLocalRing.ResidueField ↥A)ˣ)
        (↑x : ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup) :
      (IsLocalRing.ResidueField ↥A)ˣ)
    ((A.unitGroupToResidueFieldUnits : (a : ↥A.unitGroup) → (IsLocalRing.ResidueField ↥A)ˣ) x :
      (IsLocalRing.ResidueField ↥A)ˣ)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
x : K
h : (g⁻¹ • x)⁻¹ ∈ S
rwa rwa₁ rwa₂ rwa₃ : (g⁻¹ • x)⁻¹ ∈ S.toSubring
⊢ g⁻¹ • x⁻¹ ∈ S.toSubring

Tactic:
rwa [smul_inv'']

Premises used: smul_inv''
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
⊢ (↑(g • S) : Set K) = g • (↑S : Set K)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
⊢ (g • S).toSubring = g • S.toSubring

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
x : K
S : ValuationSubring K
⊢ x ∈ S → g • x ∈ g • S

Tactic:
(Set.smul_mem_smul_set : _ → _ ∈ g • (S : Set K))

Premises used: Set.Mem, setOf, Set.image, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
⊢ CovariantClass G (ValuationSubring K) HSMul.hSMul LE.le

Tactic:
⟨fun _ _ _ => Set.image_mono⟩

Premises used: CovariantClass.mk, Set.image_mono
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
x : K
S : ValuationSubring K
⊢ x ∈ g • S ↔ ∃ s ∈ S, g • s = x

Tactic:
(Set.mem_smul_set : x ∈ g • (S : Set K) ↔ _)

Premises used: Set.Mem, setOf, Set.mem_smul_set, Set.image
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
inst_3 : MulSemiringAction.{u_1, u} Gᵐᵒᵖ K
inst_4 : IsCentralScalar G K
⊢ IsCentralScalar.{u_1, u} G (ValuationSubring K)

Tactic:
⟨fun g S => toSubring_injective <| op_smul_eq_smul g S.toSubring⟩

Premises used: IsCentralScalar.mk, ValuationSubring.toSubring_injective, ValuationSubring.toSubring, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
x : K
⊢ g • x ∈ g • S ↔ x ∈ S

Tactic:
Set.smul_mem_smul_set_iff

Premises used: Set.Mem, setOf, Set.image, Set.smul_mem_smul_set_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
x : K
⊢ x ∈ g • S ↔ g⁻¹ • x ∈ S

Tactic:
Set.mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, setOf, Set.image, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S : ValuationSubring K
x : K
⊢ x ∈ g⁻¹ • S ↔ g • x ∈ S

Tactic:
Set.mem_inv_smul_set_iff

Premises used: Set.Mem, setOf, Set.mem_inv_smul_set_iff, Set.image
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S T : ValuationSubring K
⊢ g • S ≤ g • T ↔ S ≤ T

Tactic:
Set.smul_set_subset_smul_set_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.image, Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S T : ValuationSubring K
⊢ g • S ≤ T ↔ S ≤ g⁻¹ • T

Tactic:
Set.smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.Mem, setOf, Set.Subset, Set.image, Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
G : Type u_1
inst_1 : Group G
inst_2 : MulSemiringAction G K
g : G
S T : ValuationSubring K
⊢ S ≤ g • T ↔ g⁻¹ • S ≤ T

Tactic:
Set.subset_smul_set_iff

Premises used: Set.Mem, setOf, Set.subset_smul_set_iff, Set.Subset, Set.image
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
A_1 : ValuationSubring K
L : Type u_1
J : Type u_2
inst_1 : Field L
inst_2 : Field J
A : ValuationSubring L
f : K →+* L
k : K
⊢ Membership.mem (γ := Set K)
      (Subsemigroup.carrier
        (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.comap f A.toSubring)))))
      k ∨
    Membership.mem (γ := Set K)
      (Subsemigroup.carrier
        (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.comap f A.toSubring)))))
      k⁻¹

Tactic:
simp [ValuationSubring.mem_or_inv_mem]

Premises used: ValuationSubring.mem_or_inv_mem
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
A : ValuationSubring L
f : K →+* L
⊢ (↑(A.comap f) : Set K) = (⇑f : (a : K) → L) ⁻¹' (↑A : Set L)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
L : Type u_1
inst_1 : Field L
A : ValuationSubring L
f : K →+* L
x : K
⊢ x ∈ A.comap f ↔ Membership.mem (α := L) A ((f : (a : K) → L) x : L)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
L : Type u_1
J : Type u_2
inst_1 : Field L
inst_2 : Field J
A : ValuationSubring J
g : L →+* J
f : K →+* L
⊢ (A.comap g).comap f = A.comap (g.comp f)

Tactic:
rfl

Premises used: Set.Mem, setOf, ValuationSubring.comap, Set.preimage, Subring.comap, rfl
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : Kˣ
⊢ x ∈ v.valuationSubring.unitGroup ↔ Eq.{u_1 + 1} (α := Γ) ((v : (a : K) → Γ) (↑x : K) : Γ) (1 : Γ)

Tactic:
IsEquiv.eq_one_iff_eq_one (Valuation.isEquiv_valuation_valuationSubring _).symm

Premises used: Valuation.isEquiv_valuation_valuationSubring, Set.Mem, setOf, Set.preimage, Set.singleton, Valuation.IsEquiv.eq_one_iff_eq_one, Valuation.IsEquiv.symm
-- Module: Mathlib.RingTheory.Valuation.ValuationSubring
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
a : ↥v.valuationSubring
⊢ Membership.mem (γ := Ideal ↥v.valuationSubring) (IsLocalRing.maximalIdeal ↥v.valuationSubring) a ↔
    LT.lt.{u_1} (α := Γ) ((v : (a : K) → Γ) (↑a : K) : Γ) (1 : Γ)

Tactic:
Integer.not_isUnit_iff_valuation_lt_one

Premises used: Set.Mem, setOf, nonunits, Valuation.Integer.not_isUnit_iff_valuation_lt_one, Valuation.integer, Valuation.valuationSubring, Not
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ ¬@vle _ inst _ x y ↔ y <ᵥ x

Tactic:
.rfl

Premises used: ValuativeRel.vlt, Iff.rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ ¬x <ᵥ y ↔ @vle _ inst _ y x

Tactic:
not_vle.not_left

Premises used: ValuativeRel.vlt, Iff.not_left, ValuativeRel.not_vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ x =ᵥ y ↔ @vle _ inst _ x y ∧ @vle _ inst _ y x

Tactic:
.rfl

Premises used: ValuativeRel.veq, Iff.rfl, AntisymmRel
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ x <ᵥ y ↔ ¬@vle _ inst _ y x

Tactic:
Iff.rfl

Premises used: ValuativeRel.vlt, Iff.rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
⊢ x =ᵥ y ↔ y =ᵥ x

Tactic:
antisymmRel_comm

Premises used: ValuativeRel.veq, antisymmRel_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : x =ᵥ y
⊢ @vle _ inst _ x y

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : x =ᵥ y
⊢ @vle _ inst _ y x

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : x =ᵥ y
⊢ ¬x <ᵥ y

Tactic:
h.vge.not_vlt

Premises used: ValuativeRel.vle.not_vlt, ValuativeRel.veq.vge
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : x =ᵥ y
⊢ ¬y <ᵥ x

Tactic:
h.vle.not_vlt

Premises used: ValuativeRel.vle.not_vlt, ValuativeRel.veq.vle
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ @vle _ inst _ x x

Tactic:
or_self_iff.1 <| vle_total x x

Premises used: or_self_iff, Iff.mp, ValuativeRel.vle_total
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ @vle _ inst _ x x

Tactic:
vle_refl x

Premises used: ValuativeRel.vle_refl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ x =ᵥ x

Tactic:
AntisymmRel.rfl

Premises used: ValuativeRel.veq, AntisymmRel.rfl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ x =ᵥ x

Tactic:
veq_refl x

Premises used: ValuativeRel.veq_refl
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ @vle _ inst _ 0 x

Tactic:
simpa using mul_vle_mul_left ((vle_total 0 1).resolve_right not_vle_one_zero) x

Premises used: ValuativeRel.not_vle_one_zero, Or.resolve_right, OfNat.ofNat, ValuativeRel.mul_vle_mul_left, ValuativeRel.vle_total
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
⊢ ¬x <ᵥ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
h : x <ᵥ 0
⊢ False

Tactic:
not_vlt_zero _ h

Premises used: ValuativeRel.not_vlt_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : R
h : x <ᵥ 0
⊢ False

Tactic:
exact not_vlt_zero _ h

Premises used: ValuativeRel.not_vlt_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
⊢ vlt.{u_1} (R := R) 0 1

Tactic:
not_vle_one_zero

Premises used: ValuativeRel.vlt, ValuativeRel.not_vle_one_zero
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h : @vle _ inst _ x y
⊢ @vle _ inst _ (x * z) (y * z)

Tactic:
mul_vle_mul_left h z

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : @vle _ inst _ x y
z : R
rw : @vle _ inst _ (x * z) (y * z)
⊢ @vle _ inst _ (z * x) (z * y)

Tactic:
rw [mul_comm z x, mul_comm z y]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : @vle _ inst _ x y
z : R
⊢ @vle _ inst _ (x * z) (y * z)

Tactic:
mul_vle_mul_left h z

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : @vle _ inst _ x y
z : R
⊢ @vle _ inst _ (x * z) (y * z)

Tactic:
exact mul_vle_mul_left h z

Premises used: ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h1 : @vle _ inst _ y z
h2 : @vle _ inst _ x y
⊢ @vle _ inst _ x z

Tactic:
h2.trans h1

Premises used: ValuativeRel.vle.trans
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
h1 : x =ᵥ y
h2 : y =ᵥ z
⊢ x =ᵥ z

Tactic:
AntisymmRel.trans h1 h2

Premises used: ValuativeRel.veq, AntisymmRel.trans
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x x' y y' : R
h1 : @vle _ inst _ x y
h2 : @vle _ inst _ x' y'
⊢ @vle _ inst _ (x * x') (y * y')

Tactic:
(mul_vle_mul_left h1 _).trans (mul_vle_mul_right h2 _)

Premises used: ValuativeRel.mul_vle_mul_right, ValuativeRel.vle.trans, ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
hz : 0 <ᵥ z
⊢ @vle _ inst _ (x * z) (y * z) ↔ @vle _ inst _ x y

Tactic:
⟨vle_mul_cancel hz, (mul_vle_mul_left · _)⟩

Premises used: ValuativeRel.vle_mul_cancel, Iff.intro, ValuativeRel.mul_vle_mul_left
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
⊢ @vle _ inst _ (x * y) (x * z) ↔ @vle _ inst _ y z

Tactic:
simp [mul_comm x, hx]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
hz : 0 <ᵥ z
⊢ x * z <ᵥ y * z ↔ x <ᵥ y

Tactic:
(mul_vle_mul_iff_left hz).not

Premises used: ValuativeRel.vlt, ValuativeRel.mul_vle_mul_iff_left, Iff.not
-- Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
⊢ x * y <ᵥ x * z ↔ y <ᵥ z

Tactic:
(mul_vle_mul_iff_right hx).not

Premises used: ValuativeRel.vlt, Iff.not, ValuativeRel.mul_vle_mul_iff_right