awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
h : ∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
hinj : Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
this_1 : IsDomain 𝒪
this_2 : FaithfulSMul 𝒪 K
this_3 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
neg :
  ∀ (ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a),
    ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
      HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
have neg₁ : ∀ (ha : HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1),
  ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
Tactic: cases ha with
    | inl ha => exact ⟨⟨a, 1⟩, by simpa⟩
    | inr ha => exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
⊢ ValuationRing 𝒪
have this : IsDomain 𝒪
Tactic: haveI := hh.hom_inj.isDomain
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ ValuationRing 𝒪
have suffices : PreValuationRing 𝒪
Tactic: suffices PreValuationRing 𝒪 from .mk
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
⊢ PreValuationRing 𝒪
have cond' : ∀ (a b : 𝒪), ∃ (c : 𝒪), a * c = b ∨ b * c = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have cond' : ∀
  (h :
    LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
      ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)),
  ∃ (c : 𝒪), a * c = b ∨ b * c = a
Tactic: rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
cond' :
  ∀
    (h :
      LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
        ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)),
    ∃ (c : 𝒪), a * c = b ∨ b * c = a
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have cond'₁ : ∀
  (h :
    LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
      ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)),
  ∃ (c : 𝒪), a * c = b ∨ b * c = a
Tactic: rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have cond' : ∀ (c : 𝒪) (hc : a = b * c), ∃ (c : 𝒪), a * c = b ∨ b * c = a
Tactic: obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
c : 𝒪
hc : a = b * c
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have h₁ : a * c = b ∨ b * c = a
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have cond' : ∀ (c : 𝒪) (hc : b = a * c), ∃ (c : 𝒪), a * c = b ∨ b * c = a
Tactic: obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
Γ : Type w
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
hh : v.Integers 𝒪
this : IsDomain 𝒪
a b : 𝒪
h :
  LE.le.{w} (α := Γ) ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) b : K) : Γ)
    ((v : (a : K) → Γ) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) : Γ)
c : 𝒪
hc : b = a * c
⊢ ∃ (c : 𝒪), a * c = b ∨ b * c = a
have h₁ : a * c = b ∨ b * c = a
Tactic: use c
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
      Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
have refine_1 : ∀ (h : IsFractionRing 𝒪 K) (x : K),
  ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
refine_1 :
  ∀ (h : IsFractionRing 𝒪 K) (x : K),
    ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
⊢ IsFractionRing 𝒪 K ↔
    (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
      Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)
have refine_2 : ∀
  (h :
    (∀ (x : K), ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a) ∧
      Function.Injective.{u + 1, v + 1} (α := 𝒪) (β := K) (⇑(algebraMap 𝒪 K) : (a : 𝒪) → K)),
  IsFractionRing 𝒪 K
Tactic: refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
have refine_1 : ∀ (a : 𝒪) (e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x),
  ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
Tactic: obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
𝒪 : Type u
K : Type v
inst : CommRing 𝒪
inst_1 : Field K
inst_2 : Algebra 𝒪 K
inst_3 : IsDomain 𝒪
inst_4 : ValuationRing 𝒪
h : IsFractionRing 𝒪 K
x : K
refine_1 :
  ∀ (a : 𝒪) (e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x),
    ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
⊢ ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
have refine_1₁ : ∀ (a : 𝒪) (e : (algebraMap 𝒪 K : (a : 𝒪) → K) a = x⁻¹),
  ∃ (a : 𝒪), x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
Tactic: obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
⊢ ∀ ⦃a₂ : ValuationSubring K⦄,
    Eq.{u + 1} (α := Set K)
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
          { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
        ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K)) a₂) →
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = a₂
have this : ∀ (toSubring_1 : Subring K) (mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier),
  Eq.{u + 1} (α := Set K)
      ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
        { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
      ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
        { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }) →
    { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }
Tactic: ⟨_, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
toSubring_1 : Subring K
mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier
h :
  Eq.{u + 1} (α := Set K)
    ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
      { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' })
    ((fun (A : ValuationSubring K) ↦ (↑A.toSubring : Set K))
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 })
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }
have h₁ : { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
  { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring
Tactic: replace h := SetLike.coe_injective' h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
x y : ValuationSubring K
h : x.toSubring = y.toSubring
⊢ x = y
have mk : ∀ (toSubring : Subring K) (mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier)
  (h : { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring = y.toSubring),
  { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
y : ValuationSubring K
toSubring : Subring K
mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier
h : { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring = y.toSubring
⊢ { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } = y
have mk : ∀ (toSubring_1 : Subring K) (mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier)
  (h :
    { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K }.toSubring =
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }.toSubring),
  { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' : ValuationSubring K } =
    { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have pos : ∀ (h : (↑b : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: by_cases h : (b : K) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
pos : ∀ (h : (↑b : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have neg : ∀ (h : ¬(↑b : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: by_cases h : (b : K) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have h₁ : a * 0 = b ∨ b * 0 = a
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
⊢ a * 0 = b ∨ b * 0 = a
have h₁ : a * 0 = b
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : (↑b : K) = 0
⊢ a * 0 = b
have h₁ : (↑(a * 0) : K) = (↑b : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : ¬(↑b : K) = 0
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have pos : ∀ (h : (↑a : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: by_cases h : (a : K) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : ¬(↑b : K) = 0
pos : ∀ (h : (↑a : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have neg : ∀ (h : ¬(↑a : K) = 0), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: by_cases h : (a : K) = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have h₁ : a * 0 = b ∨ b * 0 = a
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
⊢ a * 0 = b ∨ b * 0 = a
have h₁ : b * 0 = a
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : (↑a : K) = 0
⊢ b * 0 = a
have h₁ : (↑(b * 0) : K) = (↑a : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have neg : ∀ (hh : (↑a : K) / (↑b : K) ∈ A), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: rcases A.mem_or_inv_mem (a / b) with hh | hh
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
neg : ∀ (hh : (↑a : K) / (↑b : K) ∈ A), ∃ (c : ↥A), a * c = b ∨ b * c = a
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have neg₁ : ∀ (hh : ((↑a : K) / (↑b : K))⁻¹ ∈ A), ∃ (c : ↥A), a * c = b ∨ b * c = a
Tactic: rcases A.mem_or_inv_mem (a / b) with hh | hh
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have h₁ : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = b ∨
  b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
Tactic: use ⟨a / b, hh⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
have h₁ : b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
Tactic: right
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑a : K) / (↑b : K) ∈ A
⊢ b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh = a
have h₁ : (↑(b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑a : K) / (↑b : K)) hh) : K) = (↑a : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (hypothesis)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : ((↑a : K) / (↑b : K))⁻¹ ∈ A
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have hh₁ : (↑b : K) / (↑a : K) ∈ A
Tactic: rw [show (a / b : K)⁻¹ = b / a by simp] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
⊢ ∃ (c : ↥A), a * c = b ∨ b * c = a
have h₁ : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b ∨
  b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = a
Tactic: use ⟨b / a, hh⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b ∨
    b * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = a
have h₁ : a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h_1 : ¬(↑b : K) = 0
h : ¬(↑a : K) = 0
hh : (↑b : K) / (↑a : K) ∈ A
⊢ a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh = b
have h₁ : (↑(a * Subtype.mk (p := fun (x : K) ↦ x ∈ A) ((↑b : K) / (↑a : K)) hh) : K) = (↑b : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have pos : ∀ (h : z = 0),
  ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
Tactic: by_cases h : z = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
pos :
  ∀ (h : z = 0),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have neg : ∀ (h : ¬z = 0),
  ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
Tactic: by_cases h : z = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : z = 0
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have h₁ : HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑(0, 1).2 : ↥A) : K) =
  (algebraMap (↥A) K : (a : ↥A) → K) (0, 1).1
Tactic: use (0, 1)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have neg : ∀ (hh : z ∈ A),
  ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
Tactic: rcases A.mem_or_inv_mem z with hh | hh
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
neg :
  ∀ (hh : z ∈ A),
    ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
      HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have neg₁ : ∀ (hh : z⁻¹ ∈ A),
  ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
Tactic: rcases A.mem_or_inv_mem z with hh | hh
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have h₁ : HMul.hMul (β := K) z
    ((algebraMap (↥A) K : (a : ↥A) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).2 : ↥A) : K) =
  (algebraMap (↥A) K : (a : ↥A) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z hh, 1).1
Tactic: use (⟨z, hh⟩, 1)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ (x : ↥A × ↥(nonZeroDivisors ↥A)),
    HMul.hMul (β := K) z ((algebraMap (↥A) K : (a : ↥A) → K) (↑x.2 : ↥A) : K) = (algebraMap (↥A) K : (a : ↥A) → K) x.1
have neg : Membership.mem (γ := Submonoid ↥A) (nonZeroDivisors ↥A) (Subtype.mk (p := fun (x : K) ↦ x ∈ A) z⁻¹ hh)
Tactic: refine ⟨⟨1, ⟨⟨_, hh⟩, ?_⟩⟩, mul_inv_cancel₀ h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a b : ↥A
h : Eq (α := K) ((algebraMap (↥A) K : (a : ↥A) → K) a : K) ((algebraMap (↥A) K : (a : ↥A) → K) b : K)
⊢ (↑1 : ↥A) * a = (↑1 : ↥A) * b
have a₁ : (↑((↑1 : ↥A) * a) : K) = (↑((↑1 : ↥A) * b) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ Eq (α := A.ValueGroup) ((A.valuation : (a : K) → A.ValueGroup) (↑(↑a : ↥A) : K) : A.ValueGroup) (1 : A.ValueGroup)
have rw : ∃ (a_1 : (↥A)ˣ), (↑(↑a_1 : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)
Tactic: rw [← A.valuation.map_one, valuation_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationSubring (goal)
Goal:
K : Type u
inst : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ (a_1 : (↥A)ˣ), (↑(↑a_1 : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)
have h : (↑(↑a : ↥A) : K) * 1 = (↑(↑a : ↥A) : K)
Tactic: use a