awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
rw :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (β := K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
        ((algebraMap R₁ K : (a : R₁) → K) y : K)))
    1
rw₁ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y : K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))))
    1
rw₂ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (mk' K y (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    1
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
have rw₃ : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 1) 1
Tactic: rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
rw :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (β := K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
        ((algebraMap R₁ K : (a : R₁) → K) y : K)))
    1
rw₁ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (HMul.hMul (α := K) ((algebraMap R₁ K : (a : R₁) → K) y : K)
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))))
    1
rw₂ :
  Eq (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (mk' K y (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    1
rw₃ : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ 1) 1
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
have rw₄ : Eq.{u_4 + 1} (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 1
Tactic: rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {x} * I = Ideal.span {y} * J
have this : HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
  1
Tactic: have :
    spanSingleton R₁⁰ (IsLocalization.mk' _ (1 : R₁) ⟨y, hy⟩) *
        spanSingleton R₁⁰ (algebraMap R₁ K y) =
      1 := by
    rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
this :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
y' : (FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y)) this
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {x} * I = Ideal.span {y} * J
have coe_y' : (↑y' : FractionalIdeal R₁⁰ K) =
  spanSingleton R₁⁰
    (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
Tactic: have coe_y' : ↑y' = spanSingleton R₁⁰ (IsLocalization.mk' K (1 : R₁) ⟨y, hy⟩) := rfl
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : Membership.mem (γ := Submonoid R₁) R₁⁰ y
this :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (β := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y) : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) =
    1
y' : (FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)ˣ :=
  Units.mkOfMulEqOne
    (spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
    (spanSingleton R₁⁰ ((algebraMap R₁ K : (a : R₁) → K) y)) this
coe_y' :
  (↑y' : FractionalIdeal R₁⁰ K) =
    spanSingleton R₁⁰
      (mk' K 1 (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy))
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {x} * I = Ideal.span {y} * J
have refine : HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk' K x (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x) y hy)))
      (↑I : FractionalIdeal R₁⁰ K) =
    (↑J : FractionalIdeal R₁⁰ K) ↔
  (↑y' : FractionalIdeal R₁⁰ K) * (↑(Ideal.span {x} * I) : FractionalIdeal R₁⁰ K) =
    (↑y' : FractionalIdeal R₁⁰ K) * (↑(Ideal.span {y} * J) : FractionalIdeal R₁⁰ K)
Tactic: refine Iff.trans ?_ (y'.mul_right_inj.trans coeIdeal_inj)
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
z : K
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {(sec R₁⁰ z).1} * I = Ideal.span {(↑(sec R₁⁰ z).2 : R₁)} * J
have rw : HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
    (↑J : FractionalIdeal R₁⁰ K) ↔
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
      (spanSingleton R₁⁰
        (mk'.{u_3, u_4} (R := R₁) (M := R₁⁰) K (sec R₁⁰ z).1
          (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x)
            (↑(sec R₁⁰ z).2 : R₁) sorry)))
      (↑I : FractionalIdeal R₁⁰ K) =
    (↑J : FractionalIdeal R₁⁰ K)
Tactic: rw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop,
    IsLocalization.mk'_sec K z]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
I J : Ideal R₁
z : K
rw :
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K)
        (spanSingleton R₁⁰
          (mk'.{u_3, u_4} (R := R₁) (M := R₁⁰) K (sec R₁⁰ z).1
            (Subtype.mk (p := fun (x : R₁) ↦ Membership.mem (γ := Submonoid R₁) (R₁⁰ : Submonoid R₁) x)
              (↑(sec R₁⁰ z).2 : R₁) ⋯)))
        (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K)
⊢ HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
      (↑J : FractionalIdeal R₁⁰ K) ↔
    Ideal.span {(sec R₁⁰ z).1} * I = Ideal.span {(↑(sec R₁⁰ z).2 : R₁)} * J
have rw₁ : HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
    (↑J : FractionalIdeal R₁⁰ K) ↔
  HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ z) (↑I : FractionalIdeal R₁⁰ K) =
    (↑J : FractionalIdeal R₁⁰ K)
Tactic: rw [← mk'_mul_coeIdeal_eq_coeIdeal K (IsLocalization.sec R₁⁰ z).2.prop,
    IsLocalization.mk'_sec K z]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J
have rw : J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
Tactic: rw [← one_div_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have pos : ∀ (hd : d = 0),
  J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
pos :
  ∀ (hd : d = 0),
    J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have neg : ∀ (hd : ¬d = 0),
  J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
Tactic: have h_spand : spanSingleton R₁⁰ d ≠ 0 := mt spanSingleton_eq_zero_iff.mp hd
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have neg : J / spanSingleton R₁⁰ d ≤ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : J / spanSingleton R₁⁰ d ≤ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
⊢ J / spanSingleton R₁⁰ d = HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have neg₁ : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x ∈ J / spanSingleton R₁⁰ d
⊢ x ∈ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have hx₁ : ∀ (y : K),
  Membership.mem (γ := Submodule R₁ K) (↑(spanSingleton R₁⁰ d) : Submodule R₁ K) y → x * y ∈ (↑J : Submodule R₁ K)
Tactic: rw [← mem_coe, coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx :
  ∀ (y : K),
    Membership.mem (γ := Submodule R₁ K) (↑(spanSingleton R₁⁰ d) : Submodule R₁ K) y → x * y ∈ (↑J : Submodule R₁ K)
⊢ x ∈ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have hx₁ : x * d ∈ (↑J : Submodule R₁ K)
Tactic: specialize hx d (mem_spanSingleton_self R₁⁰ d)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (hypothesis)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
⊢ x ∈ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have h_xd : x = d⁻¹ * (x * d)
Tactic: have h_xd : x = d⁻¹ * (x * d) := by field
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
x : K
hx : x * d ∈ (↑J : Submodule R₁ K)
h_xd : x = d⁻¹ * (x * d)
⊢ x ∈ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J
have neg : d⁻¹ * (x * d) ∈ (↑(spanSingleton R₁⁰ d⁻¹) : Submodule R₁ K) * (↑J : Submodule R₁ K)
Tactic: rw [← mem_coe, coe_mul, one_div_spanSingleton, h_xd]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₁ : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₂ : J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
neg₂ :
  J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₃ : J * HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d⁻¹) (spanSingleton R₁⁰ d) ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
neg₂ :
  J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
neg₃ : J * HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d⁻¹) (spanSingleton R₁⁰ d) ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₄ : J * spanSingleton R₁⁰ (d⁻¹ * d) ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R₁ : Type u_3
inst : CommRing R₁
K : Type u_4
inst_1 : Field K
inst_2 : Algebra R₁ K
inst_3 : IsFractionRing R₁ K
inst_4 : IsDomain R₁
J : FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K
d : K
hd : ¬d = 0
h_spand : Ne (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d) 0
neg : HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J * spanSingleton R₁⁰ d ≤ J
neg₁ :
  HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * (J * spanSingleton R₁⁰ d) ≤ J
neg₂ :
  J * (HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * spanSingleton R₁⁰ d) ≤ J
neg₃ : J * HMul.hMul (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) (spanSingleton R₁⁰ d⁻¹) (spanSingleton R₁⁰ d) ≤ J
neg₄ : J * spanSingleton R₁⁰ (d⁻¹ * d) ≤ J
⊢ HDiv.hDiv (α := FractionalIdeal.{u_3, u_4} (R := R₁) R₁⁰ K) 1 (spanSingleton R₁⁰ d) * J ≤ J / spanSingleton R₁⁰ d
have neg₅ : J * spanSingleton R₁⁰ 1 ≤ J
Tactic: rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]