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
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ LE.le (α := { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        a :
      { S : ValuationSubring K // A ≤ S })
    ((Equiv.trans OrderDual.ofDual A.primeSpectrumEquiv :
          (a : (PrimeSpectrum ↥A)ᵒᵈ) → { S : ValuationSubring K // A ≤ S })
        b :
      { S : ValuationSubring K // A ≤ S })
have h₁ : LE.le.{u} (α := Ideal ↥A) (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) b))
  (PrimeSpectrum.asIdeal ((OrderDual.ofDual : (a : (PrimeSpectrum ↥A)ᵒᵈ) → PrimeSpectrum ↥A) a))
Tactic: apply ofPrime_le_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
⊢ A = B ∨ B = ⊤
have inl : ∀
  (h :
    Eq (α := PrimeSpectrum ↥A)
      ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
        PrimeSpectrum ↥A)
      (⊥ : PrimeSpectrum ↥A)),
  A = B ∨ B = ⊤
Tactic: obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top (A.primeSpectrumEquiv.symm ⟨B, hle⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
inl :
  ∀
    (h :
      Eq (α := PrimeSpectrum ↥A)
        ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
            (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
          PrimeSpectrum ↥A)
        (⊥ : PrimeSpectrum ↥A)),
    A = B ∨ B = ⊤
⊢ A = B ∨ B = ⊤
have inr : ∀
  (h :
    Eq (α := PrimeSpectrum ↥A)
      ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
          (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
        PrimeSpectrum ↥A)
      (⊤ : PrimeSpectrum ↥A)),
  A = B ∨ B = ⊤
Tactic: obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top (A.primeSpectrumEquiv.symm ⟨B, hle⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := PrimeSpectrum ↥A)
    ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
      PrimeSpectrum ↥A)
    (⊥ : PrimeSpectrum ↥A)
⊢ A = B ∨ B = ⊤
have h₁ : Eq (α := { S : ValuationSubring K // A ≤ S })
  ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
      ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
    { S : ValuationSubring K // A ≤ S })
  ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊥ :
    { S : ValuationSubring K // A ≤ S })
Tactic: replace h := congr(primeSpectrumEquiv A $h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h :
  Eq (α := PrimeSpectrum ↥A)
    ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle) :
      PrimeSpectrum ↥A)
    (⊤ : PrimeSpectrum ↥A)
⊢ A = B ∨ B = ⊤
have h₁ : Eq (α := { S : ValuationSubring K // A ≤ S })
  ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S })
      ((A.primeSpectrumEquiv.symm : (a : { S : ValuationSubring K // A ≤ S }) → PrimeSpectrum ↥A)
        (Subtype.mk (p := fun (S : ValuationSubring K) ↦ A ≤ S) B hle)) :
    { S : ValuationSubring K // A ≤ S })
  ((A.primeSpectrumEquiv : (a : PrimeSpectrum ↥A) → { S : ValuationSubring K // A ≤ S }) ⊤ :
    { S : ValuationSubring K // A ≤ S })
Tactic: replace h := congr(primeSpectrumEquiv A $h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
⊢ A = B
have inl : ∀ (h : A = B), A = B
Tactic: obtain h | h := eq_self_or_eq_top_of_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
inl : ∀ (h : A = B), A = B
⊢ A = B
have inr : ∀ (h : B = ⊤), A = B
Tactic: obtain h | h := eq_self_or_eq_top_of_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
⊢ B = ⊤
have inl : ∀ (h : A = B), B = ⊤
Tactic: obtain h | h := eq_self_or_eq_top_of_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
inl : ∀ (h : A = B), B = ⊤
⊢ B = ⊤
have inr : ∀ (h : B = ⊤), B = ⊤
Tactic: obtain h | h := eq_self_or_eq_top_of_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hlt : A < B
⊢ B = ⊤
have inl : ∀ (h : A = B), B = ⊤
Tactic: obtain h | h := eq_self_or_eq_top_of_le hlt.le
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
inst_1 : Ring.KrullDimLE.{u} 1 ↥A
B : ValuationSubring K
hlt : A < B
inl : ∀ (h : A = B), B = ⊤
⊢ B = ⊤
have inr : ∀ (h : B = ⊤), B = ⊤
Tactic: obtain h | h := eq_self_or_eq_top_of_le hlt.le
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
have inl : ∀ (h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)), x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
Tactic: rcases val_le_one_or_val_inv_le_one v x with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ : Type u_1
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ
inst_2 : LinearOrderedCommGroupWithZero Γ₁
inst_3 : LinearOrderedCommGroupWithZero Γ₂
v : Valuation K Γ
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
x : K
inl : ∀ (h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)), x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
⊢ x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
have inr : ∀ (h : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x⁻¹ : Γ) (1 : Γ)), x ∈ v.integer.carrier ∨ x⁻¹ ∈ v.integer.carrier
Tactic: rcases val_le_one_or_val_inv_le_one v x with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
⊢ v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring
have mp : v₁.IsEquiv v₂ → v₁.valuationSubring = v₂.valuationSubring
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
mp : v₁.IsEquiv v₂ → v₁.valuationSubring = v₂.valuationSubring
⊢ v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring
have mpr : v₁.valuationSubring = v₂.valuationSubring → v₁.IsEquiv v₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
⊢ v₁.valuationSubring = v₂.valuationSubring
have mp : ∀ (x : K), x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
have h₁ : LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) ((v₁ : (a : K) → Γ₁) 1 : Γ₁) ↔
  LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) ((v₂ : (a : K) → Γ₂) 1 : Γ₂)
Tactic: specialize h x 1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
⊢ v₁.IsEquiv v₂
have mpr : ∀ (x : K),
  LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) (1 : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) (1 : Γ₂)
Tactic: apply isEquiv_of_val_le_one
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
have rw : x ∈ v₂.valuationSubring ↔ x ∈ v₂.valuationSubring
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst_1 : LinearOrderedCommGroupWithZero Γ₁
inst_2 : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
⊢ LE.le.{u_2} (α := Γ₁) ((v₁ : (a : K) → Γ₁) x : Γ₁) (1 : Γ₁) ↔
    LE.le.{u_3} (α := Γ₂) ((v₂ : (a : K) → Γ₂) x : Γ₂) (1 : Γ₂)
have this : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
Tactic: have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsEquiv v.valuationSubring.valuation
have rw : ∀ {x : K},
  LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔
    LE.le (α := v.valuationSubring.ValueGroup)
      ((v.valuationSubring.valuation : (a : K) → v.valuationSubring.ValueGroup) x : v.valuationSubring.ValueGroup)
      (1 : v.valuationSubring.ValueGroup)
Tactic: rw [isEquiv_iff_val_le_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔
    LE.le (α := v.valuationSubring.ValueGroup)
      ((v.valuationSubring.valuation : (a : K) → v.valuationSubring.ValueGroup) x : v.valuationSubring.ValueGroup)
      (1 : v.valuationSubring.ValueGroup)
have rw : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔ x ∈ v.valuationSubring
Tactic: rw [ValuationSubring.valuation_le_one_iff, mem_valuationSubring_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
Γ : Type u_1
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
x : K
rw : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔ x ∈ v.valuationSubring
⊢ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔
    LE.le (α := v.valuationSubring.ValueGroup)
      ((v.valuationSubring.valuation : (a : K) → v.valuationSubring.ValueGroup) x : v.valuationSubring.ValueGroup)
      (1 : v.valuationSubring.ValueGroup)
have rw₁ : LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ) ↔ LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) x : Γ) (1 : Γ)
Tactic: rw [ValuationSubring.valuation_le_one_iff, mem_valuationSubring_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ A.valuation.valuationSubring = A
have h : ∀ (x : K), x ∈ A.valuation.valuationSubring ↔ x ∈ A
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.valuation.valuationSubring ↔ x ∈ A
have h : x ∈ A.valuation.valuationSubring ↔
  LE.le (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rw [← A.valuation_le_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
⊢ { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b) : Kˣ) : K) ⋯,
      inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b)⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ } =
    { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a : Kˣ) : K) ⋯,
        inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ } *
      { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b : Kˣ) : K) ⋯,
        inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b⁻¹ : Kˣ) : K) ⋯, val_inv := ⋯, inv_val := ⋯ : (↥A)ˣ }
have huv : (↑(↑{ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b) : Kˣ) : K) sorry,
            inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑(a * b)⁻¹ : Kˣ) : K) sorry, val_inv := sorry, inv_val := sorry :
            (↥A)ˣ } :
        ↥A) :
    K) =
  (↑(↑({ val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a : Kˣ) : K) sorry,
              inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑a⁻¹ : Kˣ) : K) sorry, val_inv := sorry, inv_val := sorry : (↥A)ˣ } *
            { val := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b : Kˣ) : K) sorry,
              inv := Subtype.mk (p := fun (x : K) ↦ x ∈ A) (↑(↑b⁻¹ : Kˣ) : K) sorry, val_inv := sorry, inv_val := sorry : (↥A)ˣ }) :
        ↥A) :
    K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B
have mp : A.unitGroup ≤ B.unitGroup → A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : A.unitGroup ≤ B.unitGroup → A ≤ B
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B
have mpr : A ≤ B → A.unitGroup ≤ B.unitGroup
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : x ∈ A
⊢ x ∈ B
have hx₁ : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
  Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
Tactic: rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ B
have pos : ∀ (h_1 : x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
pos : ∀ (h_1 : x = 0), x ∈ B
⊢ x ∈ B
have neg : ∀ (h_1 : ¬x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
⊢ x ∈ B
have pos : ∀ (h_2 : 1 + x = 0), x ∈ B
Tactic: by_cases h_2 : 1 + x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
pos : ∀ (h_2 : 1 + x = 0), x ∈ B
⊢ x ∈ B
have neg : ∀ (h_2 : ¬1 + x = 0), x ∈ B
Tactic: by_cases h_2 : 1 + x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
⊢ x ∈ B
have neg : ∀ (hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)), x ∈ B
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx :
  LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup) ∨
    Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
neg :
  ∀ (hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)), x ∈ B
⊢ x ∈ B
have neg₁ : ∀ (hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)), x ∈ B
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ B
have this : Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 (1 + x) h_2 : Kˣ)
Tactic: have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ B
have this : Membership.mem (α := Kˣ) B.unitGroup (Units.mk0 x h_1 : Kˣ)
Tactic: have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K) : A.ValueGroup) (1 : A.ValueGroup)
⊢ x ∈ B.unitGroup
have hx₁ : Eq (α := B.ValueGroup)
  ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑x : K)) : B.ValueGroup)
  ((A.mapOfLE B h : (a : A.ValueGroup) → B.ValueGroup) 1 : B.ValueGroup)
Tactic: apply_fun A.mapOfLE B h at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x ∈ A.nonunits ↔ x = 0 ∨ x⁻¹ ∉ A
have rw : x = 0 → x ∈ A.nonunits
Tactic: rw [← valuation_le_one_iff, ← or_congr_right' fun h ↦ (A.valuation.one_le_val_iff h).not,
    ← lt_iff_not_ge, ← mem_nonunits_iff, or_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
⊢ x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A
have rw : x⁻¹ = 0 ∨ x⁻¹⁻¹ ∉ A ↔ x = 0 ∨ x ∉ A
Tactic: rw [mem_nonunits_iff_or, inv_inv, inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
rw : x⁻¹ = 0 ∨ x⁻¹⁻¹ ∉ A ↔ x = 0 ∨ x ∉ A
⊢ x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A
have rw₁ : x⁻¹ = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
Tactic: rw [mem_nonunits_iff_or, inv_inv, inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
x : K
rw : x⁻¹ = 0 ∨ x⁻¹⁻¹ ∉ A ↔ x = 0 ∨ x ∉ A
rw₁ : x⁻¹ = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
⊢ x⁻¹ ∈ A.nonunits ↔ x = 0 ∨ x ∉ A
have rw₂ : x = 0 ∨ x ∉ A ↔ x = 0 ∨ x ∉ A
Tactic: rw [mem_nonunits_iff_or, inv_inv, inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
⊢ B.nonunits ≤ A.nonunits ↔ A ≤ B
have mp : B.nonunits ≤ A.nonunits → A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
mp : B.nonunits ≤ A.nonunits → A ≤ B
⊢ B.nonunits ≤ A.nonunits ↔ A ≤ B
have mpr : A ≤ B → B.nonunits ≤ A.nonunits
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
⊢ x ∈ B
have pos : ∀ (h_1 : x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
pos : ∀ (h_1 : x = 0), x ∈ B
⊢ x ∈ B
have neg : ∀ (h_1 : ¬x = 0), x ∈ B
Tactic: by_cases h_1 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B
have neg : ∀ (hx : ¬LT.lt (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) x⁻¹ : A.ValueGroup) (1 : A.ValueGroup))
  (h_1 : ¬x = 0),
  ¬LT.lt (α := B.ValueGroup) ((B.valuation : (a : K) → B.ValueGroup) x⁻¹ : B.ValueGroup) (1 : B.ValueGroup)
Tactic: rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢
Cleared hypotheses: hx, h_1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A B : ValuationSubring K
h : A ≤ B
x : K
hx : x ∈ B.nonunits
⊢ x ∈ A.nonunits
have mpr : ∀ (h_1 : x ∉ A.nonunits), False
Tactic: by_contra h_1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
⊢ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) = (↑A.nonunits : Set K)
have h : ∀ (a : K),
  a ∈ Subtype.val (p := fun (x : K) ↦ x ∈ A) '' (↑(IsLocalRing.maximalIdeal ↥A) : Set ↥A) ↔ a ∈ (↑A.nonunits : Set K)
Tactic: ext a