awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
y : P'
mp :
  Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (spanSingleton S x) :
        FractionalIdeal S P')
      y →
    Membership.mem (γ := FractionalIdeal S P')
      (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
        FractionalIdeal S P')
      y
⊢ Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (spanSingleton S x) :
        FractionalIdeal S P')
      y ↔
    Membership.mem (γ := FractionalIdeal S P')
      (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
        FractionalIdeal S P')
      y
have mpr : Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x) :
      FractionalIdeal S P')
    y →
  Membership.mem (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
y : P'
h :
  Membership.mem (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    y
⊢ Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    y
have mp : ∃ (z : R),
  HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') = y
Tactic: rw [mem_spanSingleton]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
y : P'
h :
  Membership.mem (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    y
⊢ ∃ (z : R),
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') = y
have mp : ∀ (x' : P) (hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x')
  (h :
    Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (spanSingleton S x) :
        FractionalIdeal S P')
      ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x' : P')),
  ∃ (z : R),
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') =
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x'
Tactic: obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
h :
  Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x' : P')
⊢ ∃ (z : R),
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') =
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x'
have mp : ∀ (z : R) (hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x))
  (h :
    Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          (spanSingleton S x) :
        FractionalIdeal S P')
      ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') (z • x) : P')),
  ∃ (z_1 : R),
    HSMul.hSMul (β := P') z_1 ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') =
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') (z • x)
Tactic: obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp hx'
Cleared hypotheses: x', hx', h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x)
h :
  Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) : P')
⊢ ∃ (z_1 : R),
    HSMul.hSMul (β := P') z_1 ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') =
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x)
have h₁ : HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') =
  (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') (z • x)
Tactic: use z
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x)
h :
  Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) : P')
⊢ HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') =
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x)
have h₁ : HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') =
  HSMul.hSMul (α := R) (β := P') ((RingHom.id R : (a : R) → R) z : R)
    ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P')
Tactic: rw [IsLocalization.map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x)
h :
  Membership.mem.{u_5, u_5} (α := P') (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) : P')
h₁ :
  HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') =
    HSMul.hSMul (α := R) (β := P') ((RingHom.id R : (a : R) → R) z : R)
      ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')
⊢ HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') =
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x)
have h₂ : HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P') =
  HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P')
Tactic: rw [IsLocalization.map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
y : P'
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    y
⊢ Membership.mem (γ := FractionalIdeal S P')
    (((canonicalEquiv S P P' : RingEquiv.{u_2, u_5} (FractionalIdeal S P) (FractionalIdeal S P')) :
          (a : FractionalIdeal S P) → FractionalIdeal S P')
        (spanSingleton S x) :
      FractionalIdeal S P')
    y
have mpr : ∃ (y_1 : P),
  Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) y_1 ∧
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') y_1 = y
Tactic: rw [mem_canonicalEquiv_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
y : P'
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    y
⊢ ∃ (y_1 : P),
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) y_1 ∧
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y_1 = y
have mpr : ∀ (z : R)
  (h :
    Membership.mem (γ := FractionalIdeal S P')
      (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x) :
        FractionalIdeal S P')
      (HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P'))),
  ∃ (y : P),
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) y ∧
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') y =
        HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P')
Tactic: obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    (HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P'))
⊢ ∃ (y : P),
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) y ∧
      (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y =
        HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')
have h₁ : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x) ∧
  (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') (z • x) =
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P')
Tactic: use z • x
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
P' : Type u_5
inst_4 : CommRing P'
inst_5 : Algebra R P'
inst_6 : IsLocalization S P'
x : P
z : R
h :
  Membership.mem (γ := FractionalIdeal S P')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
    (HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P'))
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) (z • x) ∧
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x) =
      HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P')
have right : (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') (z • x) =
  HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) sorry : (a : P) → P') x : P')
Tactic: use (mem_spanSingleton _).mpr ⟨z, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
⊢ y ∈ spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'
have mp : y ∈ spanSingleton S x * I → ∃ y' ∈ I, y = x * y'
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
mp : y ∈ spanSingleton S x * I → ∃ y' ∈ I, y = x * y'
⊢ y ∈ spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'
have mpr : (∃ y' ∈ I, y = x * y') → y ∈ spanSingleton S x * I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∃ y' ∈ I, y = x * y'
have mp : ∀ (i : P), Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) i → ∀ j ∈ I, ∃ y' ∈ I, i * j = x * y'
Tactic: refine FractionalIdeal.mul_induction_on h ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
mp : ∀ (i : P), Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) i → ∀ j ∈ I, ∃ y' ∈ I, i * j = x * y'
⊢ ∃ y' ∈ I, y = x * y'
have mp₁ : ∀ (x_1 y : P), (∃ y' ∈ I, x_1 = x * y') → (∃ y' ∈ I, y = x * y') → ∃ y' ∈ I, x_1 + y = x * y'
Tactic: refine FractionalIdeal.mul_induction_on h ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1
have mp : ∀ (a : R) (ha : a • x = x'), ∃ y'_1 ∈ I, x' * y' = x * y'_1
Tactic: obtain ⟨a, ha⟩ := (mem_spanSingleton S).mp hx'
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ ∃ y'_1 ∈ I, x' * y' = x * y'_1
have right : x' * y' = x * a • y'
Tactic: use a • y', Submodule.smul_mem (I : Submodule R P) a hy'
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
⊢ x' * y' = x * a • y'
have right : a • x * y' = x * a • y'
Tactic: rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
right : a • x * y' = x * a • y'
⊢ x' * y' = x * a • y'
have right₁ : a • x * y' = a • (x * y')
Tactic: rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.FractionalIdeal.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
P : Type u_2
inst_1 : CommRing P
inst_2 : Algebra R P
inst_3 : IsLocalization S P
x y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
x' : P
hx' : Membership.mem (γ := FractionalIdeal S P) (spanSingleton S x) x'
y' : P
hy' : y' ∈ I
a : R
ha : a • x = x'
right : a • x * y' = x * a • y'
right₁ : a • x * y' = a • (x * y')
⊢ x' * y' = x * a • y'
have right₂ : a • (x * y') = a • (x * y')
Tactic: rw [← ha, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
-- 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
⊢ 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 (α := 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
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
⊢ 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 (α := 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
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
⊢ 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 (α := 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
Tactic: rw [spanSingleton_mul_spanSingleton, mul_comm, ← IsLocalization.mk'_eq_mul_mk'_one,
      IsLocalization.mk'_self, spanSingleton_one]