awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑u : A) : K)
      (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
        (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K)) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑u : A) : K)
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n /
        HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑w : A) : K)
          (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m))
have h : HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
    (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K) =
  HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n /
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑w : A) : K)
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
      (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K) =
    HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n /
      HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (↑w : A) : K)
        (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)
have h : HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
    (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K) =
  HMul.hMul (β := K)
    (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹)
    (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K)
Tactic: rw [div_eq_mul_inv, mul_inv, mul_comm ((algebraMap A _) ↑w)⁻¹ _, ←
      mul_assoc _ _ ((algebraMap A _) ↑w)⁻¹]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m))
      (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K) =
    HMul.hMul (β := K)
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
        (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹)
      (((algebraMap A K : (a : A) → K) (↑w : A))⁻¹ : K)
have h : HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m) =
  HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
    (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) (n - m) =
    HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) n *
      (HPow.hPow (α := K) ((algebraMap A K : (a : A) → K) π : K) m)⁻¹
have rw : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) π : K) (0 : K)
Tactic: rw [pow_sub₀ _ _ h_mn]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) π : K) (0 : K)
have hx : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) π
Tactic: apply IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬(↑u : A) * π ^ n = 0
m : ℕ
w : Aˣ
h_frac :
  HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) ((↑u : A) * π ^ n) : K)
      ((algebraMap A K : (a : A) → K) ((↑w : A) * π ^ m) : K) =
    x
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A) (π ^ m)
H :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        n /
      HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((intValuation (maximalIdeal A) : Valuation A (WithZero (Multiplicative ℤ))) :
              (a : A) → WithZero (Multiplicative ℤ))
            π :
          WithZero (Multiplicative ℤ))
        m ≤
    1
h_mn : m ≤ n
⊢ Membership.mem (γ := Submonoid A) (nonZeroDivisors A) π
have hx : π ≠ 0
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
⊢ Eq (α := Submonoid K) (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A)))
    (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A))
have h : ∀ (a : K),
  Membership.mem (γ := Submonoid K)
      (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) a ↔
    Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
have h : ∀
  (h :
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h :
  ∀
    (h :
      Eq (α := WithZero (Multiplicative ℤ))
        (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            a :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
have h₁ : ∀ (h : ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a),
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
have h₁ : ∀ (b : A)
  (h :
    Eq (α := WithZero (Multiplicative ℤ))
      (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap A K : (a : A) → K) b) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap A K : (a : A) → K) b) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
have h₁ : b ∉ asIdeal (maximalIdeal A)
Tactic: rw [valuation_eq_one_iff_notMem] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h : b ∉ asIdeal (maximalIdeal A)
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
have h₁ : IsUnit b
Tactic: simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h : IsUnit b
w : A
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
have left : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) b
Tactic: use b, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
b : A
h : IsUnit b
w : A
left : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) b
⊢ ∃ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) b : K)
have right : Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) b : K) ((algebraMap A K : (a : A) → K) b : K)
Tactic: use b, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
a : K
h : ∃ (x : A), Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ∧ (algebraMap A K : (a : A) → K) x = a
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have h₁ : ∀ (x : A) (h : Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x),
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap A K : (a : A) → K) x) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨x, h, rfl⟩ := h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
⊢ ∃ (u : Aˣ), u • x = y
have pos : ∀ (hx : x = 0), ∃ (u : Aˣ), u • x = y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
pos : ∀ (hx : x = 0), ∃ (u : Aˣ), u • x = y
⊢ ∃ (u : Aˣ), u • x = y
have neg : ∀ (hx : ¬x = 0), ∃ (u : Aˣ), u • x = y
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : x = 0
⊢ ∃ (u : Aˣ), u • x = y
have h₁ : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      y :
    WithZero (Multiplicative ℤ))
  (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      x :
    WithZero (Multiplicative ℤ))
Tactic: rw [eq_comm] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
⊢ ∃ (u : Aˣ), u • x = y
have pos : ∀ (hy : y = 0), ∃ (u : Aˣ), u • x = y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
pos : ∀ (hy : y = 0), ∃ (u : Aˣ), u • x = y
⊢ ∃ (u : Aˣ), u • x = y
have neg : ∀ (hy : ¬y = 0), ∃ (u : Aˣ), u • x = y
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
⊢ ∃ (u : Aˣ), u • x = y
have this : Membership.mem (γ := Submonoid K)
  (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) (y / x)
Tactic: have : (y / x) ∈ MonoidHom.mker (((maximalIdeal A).valuation K)) := by simp_all
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsDiscreteValuationRing A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (maximalIdeal A) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
hx : ¬x = 0
hy : ¬y = 0
this :
  Membership.mem (γ := Submonoid K)
    (MonoidHom.mker (F := Valuation K (WithZero (Multiplicative ℤ))) (valuation K (maximalIdeal A))) (y / x)
⊢ ∃ (u : Aˣ), u • x = y
have this₁ : Membership.mem (γ := Submonoid K) (Submonoid.map (F := A →+* K) (algebraMap A K) (IsUnit.submonoid A)) (y / x)
Tactic: rw [mker_valuation_eq_isUnitSubmonoid] at this
Cleared hypotheses: this