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
inst_4 : IsDomain R
inst_5 : Module.IsTorsionFree R P
x y : P
⊢ Eq (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y) ↔ ∃ (z : Rˣ), z • x = y
have rw : Eq (α := FractionalIdeal S P) (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ x) sorry)
    (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ y) sorry) ↔
  Eq (α := Submodule R P) (R ∙ x) (R ∙ y)
Tactic: rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, 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
I : FractionalIdeal S P
inst_4 : (↑I : Submodule R P).IsPrincipal
⊢ I = spanSingleton S (generator (↑I : Submodule R P))
have rw : I = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) sorry
Tactic: rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]
-- 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
I : FractionalIdeal S P
inst_4 : (↑I : Submodule R P).IsPrincipal
rw : I = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯
⊢ I = spanSingleton S (generator (↑I : Submodule R P))
have rw₁ : (↑I : Submodule R P) =
  (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) sorry) :
    Submodule R P)
Tactic: rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]
-- 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
I : FractionalIdeal S P
inst_4 : (↑I : Submodule R P).IsPrincipal
rw : I = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯
rw₁ :
  (↑I : Submodule R P) =
    (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯) :
      Submodule R P)
⊢ I = spanSingleton S (generator (↑I : Submodule R P))
have rw₂ : (↑I : Submodule R P) = R ∙ generator (↑I : Submodule R P)
Tactic: rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]
-- 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
I : FractionalIdeal S P
inst_4 : (↑I : Submodule R P).IsPrincipal
rw : I = Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯
rw₁ :
  (↑I : Submodule R P) =
    (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (R ∙ generator (↑I : Submodule R P)) ⋯) :
      Submodule R P)
rw₂ : (↑I : Submodule R P) = R ∙ generator (↑I : Submodule R P)
⊢ I = spanSingleton S (generator (↑I : Submodule R P))
have rw₃ : (↑I : Submodule R P) = (↑I : Submodule R P)
Tactic: rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]
-- 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
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (spanSingleton S 0) 0
have a : ∀ (x : P),
  Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 0) x ↔ Membership.mem (γ := FractionalIdeal S P) 0 x
Tactic: ext
-- 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
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) (spanSingleton S 1) 1
have a : ∀ (x : P),
  Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 1) x ↔ Membership.mem (γ := FractionalIdeal S P) 1 x
Tactic: ext
-- 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 : P
⊢ Membership.mem (γ := FractionalIdeal S P) (spanSingleton S 1) x ↔ Membership.mem (γ := FractionalIdeal S P) 1 x
have a : ∀ (a : R), HSMul.hSMul (β := P) a 1 = x ↔ (algebraMap R P : (a : R) → P) a = x
Tactic: refine (mem_spanSingleton S).trans ((exists_congr ?_).trans (mem_one_iff S).symm)
-- 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 : P
x' : R
⊢ HSMul.hSMul (β := P) x' 1 = x ↔ (algebraMap R P : (a : R) → P) x' = x
have a : HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) (1 : P) = x ↔ (algebraMap R P : (a : R) → P) x' = x
Tactic: rw [Algebra.smul_def, mul_one]
-- 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 : P
x' : R
a :
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) (1 : P) = x ↔
    (algebraMap R P : (a : R) → P) x' = x
⊢ HSMul.hSMul (β := P) x' 1 = x ↔ (algebraMap R P : (a : R) → P) x' = x
have a₁ : (algebraMap R P : (a : R) → P) x' = x ↔ (algebraMap R P : (a : R) → P) x' = x
Tactic: rw [Algebra.smul_def, mul_one]
-- 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
⊢ HMul.hMul (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y) = spanSingleton S (x * y)
have a : Eq.{u_2 + 1} (α := Submodule R P)
  ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P))
    (HMul.hMul (α := FractionalIdeal S P) (spanSingleton S x) (spanSingleton S y)))
  ((fun (I : FractionalIdeal S P) ↦ (↑I : Submodule R P)) (spanSingleton S (x * y)))
Tactic: apply coeToSubmodule_injective
-- 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 : P
⊢ HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)
have zero : Eq (α := FractionalIdeal S P) 1 (spanSingleton S (HPow.hPow (β := ℕ) x 0))
Tactic: rw [pow_zero, pow_zero, spanSingleton_one]
-- 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 : P
zero : Eq (α := FractionalIdeal S P) 1 (spanSingleton S (HPow.hPow (β := ℕ) x 0))
⊢ HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)
have zero₁ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 (spanSingleton S 1)
Tactic: rw [pow_zero, pow_zero, spanSingleton_one]
-- 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 : P
zero : Eq (α := FractionalIdeal S P) 1 (spanSingleton S (HPow.hPow (β := ℕ) x 0))
zero₁ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 (spanSingleton S 1)
⊢ HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)
have zero₂ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 1
Tactic: rw [pow_zero, pow_zero, spanSingleton_one]
-- 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 : P
n : ℕ
hn : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))
have succ : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n * spanSingleton S x = spanSingleton S (x ^ (n + 1))
Tactic: rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
-- 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 : P
n : ℕ
hn : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
succ : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n * spanSingleton S x = spanSingleton S (x ^ (n + 1))
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))
have succ₁ : HMul.hMul (α := FractionalIdeal S P) (spanSingleton S (x ^ n)) (spanSingleton S x) = spanSingleton S (x ^ (n + 1))
Tactic: rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
-- 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 : P
n : ℕ
hn : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
succ : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n * spanSingleton S x = spanSingleton S (x ^ (n + 1))
succ₁ :
  HMul.hMul (α := FractionalIdeal S P) (spanSingleton S (x ^ n)) (spanSingleton S x) = spanSingleton S (x ^ (n + 1))
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))
have succ₂ : Eq (α := FractionalIdeal S P) (spanSingleton S (x ^ n * x)) (spanSingleton S (x ^ (n + 1)))
Tactic: rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
-- 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 : P
n : ℕ
hn : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
succ : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n * spanSingleton S x = spanSingleton S (x ^ (n + 1))
succ₁ :
  HMul.hMul (α := FractionalIdeal S P) (spanSingleton S (x ^ n)) (spanSingleton S x) = spanSingleton S (x ^ (n + 1))
succ₂ : Eq (α := FractionalIdeal S P) (spanSingleton S (x ^ n * x)) (spanSingleton S (x ^ (n + 1)))
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))
have succ₃ : Eq (α := FractionalIdeal S P) (spanSingleton S (x ^ n * x)) (spanSingleton S (x ^ n * x))
Tactic: rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
-- 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 : P
n : ℕ
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
have zero : HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)
Tactic: induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
Cleared hypotheses: n
-- 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 : P
n : ℕ
zero : HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)
have succ : ∀ (n : ℕ) (hn : HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)),
  HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))
Tactic: induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]
Cleared hypotheses: n
-- 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 : R
⊢ Eq.{u_2 + 1} (α := FractionalIdeal S P) ((↑(Ideal.span {x}) : FractionalIdeal S P) : FractionalIdeal S P)
    (spanSingleton S ((algebraMap R P : (a : R) → P) x) : FractionalIdeal S P)
have a : ∀ (y : P),
  Membership.mem (γ := FractionalIdeal S P) (↑(Ideal.span {x}) : FractionalIdeal S P) y ↔
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S ((algebraMap R P : (a : R) → P) x) : FractionalIdeal S P)
      y
Tactic: ext y
-- 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 : R
y : P
⊢ Membership.mem (γ := FractionalIdeal S P) (↑(Ideal.span {x}) : FractionalIdeal S P) y ↔
    Membership.mem (γ := FractionalIdeal S P) (spanSingleton S ((algebraMap R P : (a : R) → P) x) : FractionalIdeal S P)
      y
have a : (∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) x' = y) ↔
  ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = y
Tactic: refine (mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)
-- 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 : R
y : P
⊢ (∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) x' = y) ↔
    ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = y
have a : (∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) x' = y) →
  ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : 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
x : R
y : P
a :
  (∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) x' = y) →
    ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = y
⊢ (∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) x' = y) ↔
    ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = y
have a₁ : (∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = y) →
  ∃ (x' : R), Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧ (algebraMap R P : (a : R) → P) 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' : R
hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) y'
⊢ ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) y'
have a : ∀ (x' : R) (hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) (x' • x)),
  ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
Tactic: obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'
Cleared hypotheses: y', 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 x' : R
hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) (x' • x)
⊢ ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
have h : HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
Tactic: use 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
x x' : R
hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) (x' • x)
⊢ HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
have h : HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' * x)
Tactic: rw [smul_eq_mul, map_mul, Algebra.smul_def]
-- 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 x' : R
hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) (x' • x)
h : HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' * x)
⊢ HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
have h₁ : HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) =
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) ((algebraMap R P : (a : R) → P) x : P)
Tactic: rw [smul_eq_mul, map_mul, Algebra.smul_def]
-- 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 x' : R
hy' : Membership.mem (γ := Ideal R) (Ideal.span {x}) (x' • x)
h : HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' * x)
h₁ :
  HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) =
    HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) ((algebraMap R P : (a : R) → P) x : P)
⊢ HSMul.hSMul (β := P) x' ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)
have h₂ : HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) ((algebraMap R P : (a : R) → P) x : P) =
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) x' : P) ((algebraMap R P : (a : R) → P) x : P)
Tactic: rw [smul_eq_mul, map_mul, Algebra.smul_def]
-- 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' : R
⊢ ∃ (x' : R),
    Membership.mem (γ := Ideal R) (Ideal.span {x}) x' ∧
      (algebraMap R P : (a : R) → P) x' = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
have a : (algebraMap R P : (a : R) → P) (y' * x) = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
Tactic: refine ⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', 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' : R
⊢ (algebraMap R P : (a : R) → P) (y' * x) = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
have a : HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) y' : P) ((algebraMap R P : (a : R) → P) x : P) =
  HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
Tactic: rw [map_mul, Algebra.smul_def]
-- 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' : R
a :
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) y' : P) ((algebraMap R P : (a : R) → P) x : P) =
    HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
⊢ (algebraMap R P : (a : R) → P) (y' * x) = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
have a₁ : HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) y' : P) ((algebraMap R P : (a : R) → P) x : P) =
  HMul.hMul (α := P) (β := P) ((algebraMap R P : (a : R) → P) y' : P) ((algebraMap R P : (a : R) → P) x : P)
Tactic: rw [map_mul, Algebra.smul_def]
-- 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
⊢ Eq.{u_5 + 1} (α := 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')
    (spanSingleton S ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x) :
      FractionalIdeal S P')
have apply : ∀ (x_1 : P'),
  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')
      x_1 ↔
    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')
      x_1
Tactic: apply SetLike.ext_iff.mpr
-- 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'
⊢ 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 : 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) sorry : (a : P) → P') x) :
      FractionalIdeal S P')
    y
Tactic: constructor