awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ ValuationRing R
have inl : ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
  (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
inl :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ ValuationRing R
have inr : ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
  (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
inl :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr inr₁ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ ValuationRing R
have inr₂ : ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
  (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1), a * g ∣ b * g ∨ b * g ∣ a * g
Tactic: classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
inl :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr inr₁ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr₂ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1), a * g ∣ b * g ∨ b * g ∣ a * g
⊢ ValuationRing R
have inr₃ : ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
  (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1) (h' : IsUnit (x * a)), a * g ∣ b * g
Tactic: classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
inst_5 : IsLocalRing R
inst_6 : IsBezout R
refine : ∀ (a b : R), a ∣ b ∨ b ∣ a
refine₁ : ∀ (a b g : R) (e : Eq (α := Ideal R) (Ideal.span {a, b}) (Ideal.span {g})), a ∣ b ∨ b ∣ a
refine₂ : ∀ (b g a : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b}) (Ideal.span {g})), a * g ∣ b ∨ b ∣ a * g
refine₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})), a * g ∣ b * g ∨ b * g ∣ a * g
refine₄ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g), a * g ∣ b * g ∨ b * g ∣ a * g
inl :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g = 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr inr₁ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0), a * g ∣ b * g ∨ b * g ∣ a * g
inr₂ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1), a * g ∣ b * g ∨ b * g ∣ a * g
inr₃ :
  ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
    (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1) (h' : IsUnit (x * a)), a * g ∣ b * g
⊢ ValuationRing R
have inr₄ : ∀ (g a b : R) (e : Eq (α := Ideal R) (Ideal.span {a * g, b * g}) (Ideal.span {g})) (x y : R)
  (e' : x * (a * g) + y * (b * g) = g) (h : g ≠ 0) (this : x * a + y * b = 1) (h' : IsUnit (y * b)), b * g ∣ a * g
Tactic: classical
  refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
  obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
  obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show a ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨b, rfl⟩ := Ideal.mem_span_singleton'.mp
      (show b ∈ Ideal.span {g} by rw [← e]; exact Ideal.subset_span (by simp))
  obtain ⟨x, y, e'⟩ := Ideal.mem_span_pair.mp
      (show g ∈ Ideal.span {a * g, b * g} by rw [e]; exact Ideal.subset_span (by simp))
  rcases eq_or_ne g 0 with h | h
  · simp [h]
  have : x * a + y * b = 1 := by
    apply mul_left_injective₀ h; convert! e' using 1 <;> ring
  rcases IsLocalRing.isUnit_or_isUnit_of_add_one this with h' | h' <;> [left; right]
  all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
have tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
Tactic: tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
have tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
Tactic: tfae_have 1 ↔ 3 := iff_dvd_total
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
have tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
Tactic: tfae_have 1 ↔ 4 := iff_ideal_total
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun (x1 x2 : R) ↦ x1 ∣ x2, Std.Total fun (x1 x2 : Ideal R) ↦ x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
have tfae_1_iff_5 : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
Tactic: tfae_have 1 ↔ 5 := iff_local_bezout_domain
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : S
⊢ ∃ (c : S), a * c = b ∨ b * c = a
have obtain : ∀ (a b : R),
  ∃ (c : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c = (f : (a : R) → S) a
Tactic: obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
⊢ ∃ (c : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c = (f : (a : R) → S) a
have inl : ∀ (c : R),
  ∃ (c_1 : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c_1 = (f : (a : R) → S) (a * c) ∨
      HMul.hMul (α := S) ((f : (a : R) → S) (a * c) : S) c_1 = (f : (a : R) → S) a
Tactic: obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : PreValuationRing R
inst_2 : Mul S
f : R →ₙ* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
inl :
  ∀ (c : R),
    ∃ (c_1 : S),
      HMul.hMul (α := S) ((f : (a : R) → S) a : S) c_1 = (f : (a : R) → S) (a * c) ∨
        HMul.hMul (α := S) ((f : (a : R) → S) (a * c) : S) c_1 = (f : (a : R) → S) a
⊢ ∃ (c : S),
    HMul.hMul (α := S) ((f : (a : R) → S) a : S) c = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c = (f : (a : R) → S) a
have inr : ∀ (c : R),
  ∃ (c_1 : S),
    HMul.hMul (α := S) ((f : (a : R) → S) (b * c) : S) c_1 = (f : (a : R) → S) b ∨
      HMul.hMul (α := S) ((f : (a : R) → S) b : S) c_1 = (f : (a : R) → S) (b * c)
Tactic: obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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)
⊢ IsFractionRing 𝒪 K
have this : IsDomain 𝒪
Tactic: have : IsDomain 𝒪 := hinj.isDomain
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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 : IsDomain 𝒪
⊢ IsFractionRing 𝒪 K
have this₁ : FaithfulSMul 𝒪 K
Tactic: have := (faithfulSMul_iff_algebraMap_injective ..).2 hinj
-- 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 : IsDomain 𝒪
⊢ IsFractionRing 𝒪 K
have refine : ∀ (z : K),
  ∃ (x : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) z ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x.1
Tactic: refine ⟨by simp, ?_, fun hab ↦ ⟨1, by simpa using hab⟩⟩
-- 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 : IsDomain 𝒪
x : K
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
have obtain : ∀ (a : 𝒪) (ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ 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
Tactic: obtain ⟨a, ha⟩ := h 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
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 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ 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
have pos : ∀ (h0 : a = 0),
  ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
Tactic: by_cases h0 : a = 0
-- 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 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
pos :
  ∀ (h0 : a = 0),
    ∃ (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 : ∀ (h0 : ¬a = 0),
  ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
Tactic: by_cases h0 : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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 : IsDomain 𝒪
x : K
a : 𝒪
ha : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
have this₁ : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
Tactic: have : algebraMap 𝒪 K a ≠ 0 := by simpa using h0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuationRing (hypothesis)
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 ∨ x⁻¹ = (algebraMap 𝒪 K : (a : 𝒪) → K) a
h0 : ¬a = 0
this : Ne.{v + 1} (α := K) ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) (0 : K)
⊢ ∃ (x_1 : 𝒪 × ↥(nonZeroDivisors 𝒪 : Submonoid 𝒪)),
    HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) (↑x_1.2 : 𝒪) : K) = (algebraMap 𝒪 K : (a : 𝒪) → K) x_1.1
have ha₁ : x = (algebraMap 𝒪 K : (a : 𝒪) → K) a ∨ HMul.hMul (β := K) x ((algebraMap 𝒪 K : (a : 𝒪) → K) a : K) = 1
Tactic: rw [inv_eq_iff_eq_inv, ← one_div, eq_div_iff this] at ha
Cleared hypotheses: ha, h0, this
-- 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)
⊢ ∃ (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 : 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
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