awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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)))
⊢ (↑((A.unitGroupMulEquiv.symm : (a : (↥A)ˣ) → ↥A.unitGroup) (↑x : (↥A)ˣ)) : Kˣ) ∈ A.principalUnitGroup
have 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)ˣ)
Tactic: rw [A.coe_mem_principalUnitGroup_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h : ∀ (x : ↥A.unitGroup),
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h : x ∈ A.unitGroupToResidueFieldUnits.ker ↔
  Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₂ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔
  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)ˣ) x : (↥A)ˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
h₂ :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    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)ˣ) x : (↥A)ˣ)
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₃ : x ∈
    MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (MonoidHom.comp
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
        A.unitGroupMulEquiv.toMonoidHom) ↔
  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)ˣ) x : (↥A)ˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
h₂ :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    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)ˣ) x : (↥A)ˣ)
h₃ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    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)ˣ) x : (↥A)ˣ)
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₄ : x ∈
    MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (MonoidHom.comp
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
        A.unitGroupMulEquiv.toMonoidHom) ↔
  Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
    (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
    ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : ↥A.unitGroup
h :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    Membership.mem (α := Kˣ) A.principalUnitGroup ((A.unitGroup.subtype : (a : ↥A.unitGroup) → Kˣ) x : Kˣ)
h₁ : x ∈ A.unitGroupToResidueFieldUnits.ker ↔ (↑x : Kˣ) ∈ A.principalUnitGroup
h₂ :
  x ∈ A.unitGroupToResidueFieldUnits.ker ↔
    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)ˣ) x : (↥A)ˣ)
h₃ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    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)ˣ) x : (↥A)ˣ)
h₄ :
  x ∈
      MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (MonoidHom.comp
          (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
          A.unitGroupMulEquiv.toMonoidHom) ↔
    Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
      (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
      ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
⊢ x ∈ A.unitGroupToResidueFieldUnits.ker ↔ x ∈ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
have h₅ : x ∈
    MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (MonoidHom.comp
        (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* ↥A ⧸ IsLocalRing.maximalIdeal ↥A))
        A.unitGroupMulEquiv.toMonoidHom) ↔
  Membership.mem (α := (↥A)ˣ) (γ := Subgroup (↥A)ˣ)
    (MonoidHom.ker (M := (IsLocalRing.ResidueField ↥A)ˣ)
      (Units.map (↑(Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)) : ↥A →* IsLocalRing.ResidueField ↥A)))
    ((A.unitGroupMulEquiv : (a : ↥A.unitGroup) → (↥A)ˣ) x : (↥A)ˣ)
Tactic: simp_rw [Subgroup.mem_comap, Subgroup.coe_subtype, coe_mem_principalUnitGroup_iff,
    unitGroupToResidueFieldUnits, IsLocalRing.residue, RingHom.toMonoidHom_eq_coe,
    MulEquiv.toMonoidHom_eq_coe, MonoidHom.mem_ker, MonoidHom.coe_comp, MonoidHom.coe_coe,
    Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
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
⊢ g⁻¹ • x⁻¹ ∈ S.toSubring
have rwa : (g⁻¹ • x)⁻¹ ∈ S.toSubring
Tactic: rwa [smul_inv'']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
h : @vle _ inst _ x y
z : R
⊢ @vle _ inst _ (z * x) (z * y)
have rw : @vle _ inst _ (x * z) (y * z)
Tactic: rw [mul_comm z x, mul_comm z y]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : 0 <ᵥ y
⊢ 0 <ᵥ x * y
have contrapose : ∀ (hy : ¬0 <ᵥ x * y), ¬0 <ᵥ y
Tactic: contrapose hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : ¬0 <ᵥ x * y
⊢ ¬0 <ᵥ y
have rw : ∀ (hy : @vle _ inst _ (x * y) 0), @vle _ inst _ y 0
Tactic: rw [not_vlt] at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : @vle _ inst _ (x * y) 0
⊢ @vle _ inst _ y 0
have hy₁ : @vle _ inst _ (y * x) (0 * x)
Tactic: rw [show (0 : R) = x * 0 by simp, mul_comm x y, mul_comm x 0] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ (↑x : R) ≠ 0
have this : Membership.mem (γ := Submonoid R) (posSubmonoid R) (↑x : R)
Tactic: have := x.prop
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
this : Membership.mem (γ := Submonoid R) (posSubmonoid R) (↑x : R)
⊢ (↑x : R) ≠ 0
have this₁ : 0 <ᵥ (↑x : R)
Tactic: rw [posSubmonoid_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x : ↥(posSubmonoid R)
this : 0 <ᵥ (↑x : R)
⊢ (↑x : R) ≠ 0
have contrapose : ∀ (this : (↑x : R) = 0), ¬0 <ᵥ (↑x : R)
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
⊢ match (motive := R × ↥(posSubmonoid R) → Prop) (r, u) with
  | (x, s) =>
    match (motive := R × ↥(posSubmonoid R) → Prop) (t, w) with
    | (y, t) => @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) ∧ @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
have left : @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
left : @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
⊢ match (motive := R × ↥(posSubmonoid R) → Prop) (r, u) with
  | (x, s) =>
    match (motive := R × ↥(posSubmonoid R) → Prop) (t, w) with
    | (y, t) => @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) ∧ @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
have right : @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
⊢ @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
have this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑u : R) * (↑w : R))
Tactic: have := mul_vle_mul h1 (vle_refl ↑w)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑u : R) * (↑w : R))
⊢ @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
have this₁ : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
Tactic: rw [mul_right_comm s] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
⊢ @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
have this₁ : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (t * (↑v : R) * (↑u : R))
Tactic: have := vle_trans this (mul_vle_mul h3 (vle_refl _))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (s * (↑w : R) * (↑u : R))
this : @vle _ inst _ (r * (↑v : R) * (↑w : R)) (t * (↑v : R) * (↑u : R))
⊢ @vle _ inst _ (r * (↑w : R)) (t * (↑u : R))
have this₁ : @vle _ inst _ (r * (↑w : R) * (↑v : R)) (t * (↑u : R) * (↑v : R))
Tactic: rw [mul_right_comm r, mul_right_comm t] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
⊢ @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
have this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑w : R) * (↑u : R))
Tactic: have := mul_vle_mul h4 (vle_refl ↑u)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑w : R) * (↑u : R))
⊢ @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
have this₁ : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
Tactic: rw [mul_right_comm s] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
⊢ @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
have this₁ : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (r * (↑v : R) * (↑w : R))
Tactic: have := vle_trans this (mul_vle_mul h2 (vle_refl _))
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x y z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : @vle _ inst _ (r * (↑v : R)) (s * (↑u : R))
h2 : @vle _ inst _ (s * (↑u : R)) (r * (↑v : R))
h3 : @vle _ inst _ (s * (↑w : R)) (t * (↑v : R))
h4 : @vle _ inst _ (t * (↑v : R)) (s * (↑w : R))
this_1 : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (s * (↑u : R) * (↑w : R))
this : @vle _ inst _ (t * (↑v : R) * (↑u : R)) (r * (↑v : R) * (↑w : R))
⊢ @vle _ inst _ (t * (↑u : R)) (r * (↑w : R))
have this₁ : @vle _ inst _ (t * (↑u : R) * (↑v : R)) (r * (↑w : R) * (↑v : R))
Tactic: rw [mul_right_comm t, mul_right_comm r] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) x s z
      v)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) y t w
      u)
have h₅ : @vle _ inst _ (x * z * (↑(t * u) : R)) (y * w * (↑(s * v) : R))
Tactic: apply ValueGroupWithZero.sound
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
h₅ : @vle _ inst _ (x * z * (↑(t * u) : R)) (y * w * (↑(s * v) : R))
⊢ Eq.{u_1 + 1} (α := ValueGroupWithZero R)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) x s z
      v)
    ((fun (a : R) (b : ↥(posSubmonoid R)) (c : R) (d : ↥(posSubmonoid R)) ↦ ValueGroupWithZero.mk (a * c) (b * d)) y t w
      u)
have h₆ : @vle _ inst _ (y * w * (↑(s * v) : R)) (x * z * (↑(t * u) : R))
Tactic: apply ValueGroupWithZero.sound
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
⊢ @vle _ inst _ (x * z * (↑(t * u) : R)) (y * w * (↑(s * v) : R))
have h₅ : @vle _ inst _ (x * (↑t : R) * (z * (↑u : R))) (y * (↑s : R) * (w * (↑v : R)))
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul,
        mul_mul_mul_comm x, mul_mul_mul_comm y]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
x_1 y_1 z_1 x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : @vle _ inst _ (x * (↑t : R)) (y * (↑s : R))
h₂ : @vle _ inst _ (y * (↑s : R)) (x * (↑t : R))
h₃ : @vle _ inst _ (z * (↑u : R)) (w * (↑v : R))
h₄ : @vle _ inst _ (w * (↑v : R)) (z * (↑u : R))
⊢ @vle _ inst _ (y * w * (↑(s * v) : R)) (x * z * (↑(t * u) : R))
have h₅ : @vle _ inst _ (y * (↑s : R) * (w * (↑v : R))) (x * (↑t : R) * (z * (↑u : R)))
Tactic: rw [Submonoid.coe_mul, Submonoid.coe_mul,
        mul_mul_mul_comm x, mul_mul_mul_comm y]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
α : Type u_2
inst_2 : Mul α
f : R → ↥(posSubmonoid R) → α
hf :
  ∀ (x y : R) (t s : ↥(posSubmonoid R)),
    @vle _ inst _ (x * (↑t : R)) (y * (↑s : R)) → @vle _ inst _ (y * (↑s : R)) (x * (↑t : R)) → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
a b : ValueGroupWithZero R
⊢ ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b
have mk : ∀ (x : R) (y : ↥(posSubmonoid R)),
  ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y * b) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) * ValueGroupWithZero.lift f hf b
Tactic: induction a using ValueGroupWithZero.ind
Cleared hypotheses: a