awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
pos :
  ∀ (ha : a = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (((MonoidWithZeroHom.comp MonoidWithZero.inverse
                (Valuation.toMonoidWithZeroHom
                  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
              K →*₀ WithZero (Multiplicative ℤ)) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
neg :
  ∀ (ha : ¬a = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (((MonoidWithZeroHom.comp MonoidWithZero.inverse
                (Valuation.toMonoidWithZeroHom
                  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
              K →*₀ WithZero (Multiplicative ℤ)) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
ha : a = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
ha : ¬a = 0
neg :
  ∀ (x y : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y)
    (ha :
      ¬HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
        WithZero (Multiplicative ℤ))
      (((MonoidWithZeroHom.comp MonoidWithZero.inverse
                (Valuation.toMonoidWithZeroHom
                  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
              K →*₀ WithZero (Multiplicative ℤ)) :
            (a : K) → WithZero (Multiplicative ℤ))
          (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) a

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
ha : ¬HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
      WithZero (Multiplicative ℤ))

Tactic:
simp_all [ordFrac_eq_intValuation _, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
    IsDiscreteValuationRing.intValuation_maximalIdeal]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, Ring.ordFrac_eq_intValuation, IsDiscreteValuationRing.intValuation_maximalIdeal
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((((IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R) :
              Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          x)⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
simp [ordFrac_eq_inverse_comp_valuation]

Premises used: Ring.ordFrac_eq_inverse_comp_valuation
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
ϖ : R
hϖ : Irreducible ϖ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) ϖ) :
      WithZero (Multiplicative ℤ))
    (WithZero.exp 1 : WithZero (Multiplicative ℤ))

Tactic:
simp [ordFrac_eq_valuation_inv, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
    IsDiscreteValuationRing.intValuation_maximalIdeal,
    IsDiscreteValuationRing.addVal_uniformizer hϖ, ← WithZero.exp_eq_coe_ofAdd]

Premises used: WithZero.exp_eq_coe_ofAdd, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDiscreteValuationRing.addVal_uniformizer, IsDiscreteValuationRing.intValuation_maximalIdeal, Ring.ordFrac_eq_valuation_inv
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x : R
⊢ IsUnit x ↔
    Eq (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) x) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [ordFrac_eq_valuation_inv, IsDiscreteValuationRing.maximalIdeal]

Premises used: IsDiscreteValuationRing.maximalIdeal, Ring.ordFrac_eq_valuation_inv
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
rw :
  Eq (α := Submonoid K)
    (Submonoid.comap (F := K →*₀ WithZero (Multiplicative ℤ))
      (Valuation.toMonoidWithZeroHom (valuation K (IsDiscreteValuationRing.maximalIdeal R))) ⊥)
    (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))
⊢ Eq (α := Submonoid K) (MonoidHom.mker (F := K →*₀ WithZero (Multiplicative ℤ)) (ordFrac R))
    (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))

Tactic:
rw [ordFrac_eq_inverse_comp_valuation, ← MonoidWithZeroHom.comap_mker,
      MonoidWithZeroHom.mker_inverse]

Premises used: MonoidWithZeroHom.mker_inverse, MonoidWithZeroHom.comap_mker, Ring.ordFrac_eq_inverse_comp_valuation
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
⊢ Eq (α := Submonoid K)
    (Submonoid.comap (F := K →*₀ WithZero (Multiplicative ℤ))
      (Valuation.toMonoidWithZeroHom (valuation K (IsDiscreteValuationRing.maximalIdeal R))) ⊥)
    (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))

Tactic:
IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid

Premises used: MonoidHom.mker, IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid, Valuation.extendToLocalization, Submonoid.comap, IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
⊢ Eq (α := Submonoid K)
    (Submonoid.comap (F := K →*₀ WithZero (Multiplicative ℤ))
      (Valuation.toMonoidWithZeroHom (valuation K (IsDiscreteValuationRing.maximalIdeal R))) ⊥)
    (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))

Tactic:
exact IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid

Premises used: IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
simp :
  LE.le (α := WithZero (Multiplicative ℤ))
    (min
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            x)⁻¹
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            y)⁻¹ :
      WithZero (Multiplicative ℤ))
    ((((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          (x + y))⁻¹ :
      WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (min (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) x)
        (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) y) :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (x + y) :
      WithZero (Multiplicative ℤ))

Tactic:
simp only [ordFrac_eq_valuation_inv]

Premises used: Ring.ordFrac_eq_valuation_inv
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
h₂ :
  LT.lt (α := WithZero (Multiplicative ℤ)) 0
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      (x + y))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (min
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            x)⁻¹
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            y)⁻¹ :
      WithZero (Multiplicative ℤ))
    ((((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          (x + y))⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
grw [Valuation.map_add, min_inv_inv_le]

Premises used: Valuation.map_add, min_inv_inv_le
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) 0
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      (x + y))

Tactic:
simpa [WithZero.pos_iff_ne_zero]

Premises used: WithZero.pos_iff_ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) y :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))

Tactic:
rw [ordFrac_eq_valuation_inv, ordFrac_eq_valuation_inv, inv_inj] at h

Premises used: inv_inj, Ring.ordFrac_eq_valuation_inv
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
⊢ ∃ (u : Rˣ), u • x = y

Tactic:
IsDiscreteValuationRing.associated_of_valuation_eq _ _ h

Premises used: IsDiscreteValuationRing.associated_of_valuation_eq
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        y :
      WithZero (Multiplicative ℤ))
⊢ ∃ (u : Rˣ), u • x = y

Tactic:
exact IsDiscreteValuationRing.associated_of_valuation_eq _ _ h

Premises used: IsDiscreteValuationRing.associated_of_valuation_eq
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
rw : ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 0 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)
⊢ Eq (α := OreLocalization S R) (0 /ₒ s) 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, OreLocalization.zero_def
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
⊢ HSMul.hSMul (β := R) s 0 = HSMul.hSMul (α := R) (β := R) 1 0 ∧ (↑s : R) * (↑1 : R) = 1 * (↑s : R)

Tactic:
simp [Submonoid.smul_def]

Premises used: Submonoid.smul_def
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
⊢ ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 0 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)

Tactic:
exact ⟨s, 1, by simp [Submonoid.smul_def]⟩
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
⊢ 0 * x = 0

Tactic:
induction x using OreLocalization.ind with | _ r s
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ HMul.hMul (α := R) (↑1 : R) 0 = 0 * (↑s : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (0 /ₒ 1) (r /ₒ s) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (0 * r /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S R) (0 /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
c₃ c₄ : Eq.{u_1 + 1} (α := OreLocalization S R) (0 /ₒ 1) (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]

Premises used: MulZeroClass.zero_mul, OreLocalization.zero_def, OreLocalization.oreDiv_mul_char, OfNat.ofNat, one_mul
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
⊢ x * 0 = 0

Tactic:
induction x using OreLocalization.ind with | _ r s
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (r * 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S R) (0 /ₒ s) (0 /ₒ 1)
c₃ : Eq.{u_1 + 1} (α := OreLocalization S R) 0 (0 /ₒ 1)
c₄ c₅ : Eq.{u_1 + 1} (α := OreLocalization S R) 0 0
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0

Tactic:
rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']

Premises used: OreLocalization.mul_div_one, MulZeroClass.mul_zero, OreLocalization.zero_def, OreLocalization.zero_oreDiv'
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
rw :
  (∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 1 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)) ↔
    0 ∈ S
⊢ Subsingleton.{u_1 + 1} (OreLocalization S R) ↔ 0 ∈ S

Tactic:
rw [← subsingleton_iff_zero_eq_one, OreLocalization.one_def,
    OreLocalization.zero_def, oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff, OreLocalization.zero_def, subsingleton_iff_zero_eq_one, OreLocalization.one_def
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
⊢ (∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 1 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)) ↔
    0 ∈ S

Tactic:
simp
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
rw : ¬Subsingleton.{u_1 + 1} (OreLocalization S R) ↔ ¬0 ∈ S
rw₁ rw₂ : ¬0 ∈ S ↔ ¬0 ∈ S
⊢ Nontrivial.{u_1} (OreLocalization S R) ↔ ¬0 ∈ S

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Premises used: OreLocalization.subsingleton_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
⊢ (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = oreNum (↑s₁ : R) s₂ * (↑s₂ : R)

Tactic:
have ha := ore_eq (s₁ : R) s₂
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = oreNum (↑s₁ : R) s₂ * (↑s₂ : R)
generalize :
  ∀ (ra : R) (ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = ra * (↑s₂ : R)),
    Eq (α := OreLocalization S X) ((oreDenom (↑s₁ : R) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
      ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
⊢ Eq (α := OreLocalization S X)
    ((oreDenom (↑s₁ : R) s₂ • r₁ + oreNum (↑s₁ : R) s₂ • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)

Tactic:
generalize oreNum (s₁ : R) s₂ = ra at *

Premises used: OreLocalization.oreNum, Subtype.val
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = ra * (↑s₂ : R)
generalize :
  ∀ (sa : ↥S) (ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)),
    Eq (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁))
      ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
⊢ Eq (α := OreLocalization S X) ((oreDenom (↑s₁ : R) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)

Tactic:
generalize oreDenom (s₁ : R) s₂ = sa at *

Premises used: Subtype.val, OreLocalization.oreDenom
-- Module: Mathlib.RingTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rw :
  ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
⊢ Eq (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)

Tactic:
rw [oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff