awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ 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:
simp only [coe_mul, coe_spanSingleton, span_mul_span, singleton_mul_singleton]

Premises used: Submodule.span_mul_span, FractionalIdeal.coe_mul, FractionalIdeal.coe_spanSingleton, Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
zero₂ zero₃ : Eq.{u_2 + 1} (α := FractionalIdeal S P) 1 1
⊢ HPow.hPow (α := FractionalIdeal S P) (β := ℕ) (spanSingleton S x) 0 = spanSingleton S (HPow.hPow (β := ℕ) x 0)

Tactic:
rw [pow_zero, pow_zero, spanSingleton_one]

Premises used: pow_zero, FractionalIdeal.spanSingleton_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)))
succ₃ succ₄ : Eq (α := FractionalIdeal S P) (spanSingleton S (x ^ n * x)) (spanSingleton S (x ^ n * x))
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) (n + 1) = spanSingleton S (x ^ (n + 1))

Tactic:
rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, pow_succ
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
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))
⊢ HPow.hPow (α := FractionalIdeal S P) (spanSingleton S x) n = spanSingleton S (x ^ n)

Tactic:
induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

Premises used: FractionalIdeal.spanSingleton_mul_spanSingleton, pow_succ, pow_zero, Submodule.zero, FractionalIdeal.spanSingleton_one
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ 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)

Tactic:
ext y
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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

Tactic:
(mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)

Premises used: FractionalIdeal.mem_coeIdeal, FractionalIdeal.mem_spanSingleton, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
⊢ 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:
refine (mem_coeIdeal S).trans (Iff.trans ?_ (mem_spanSingleton S).symm)

Premises used: FractionalIdeal.mem_coeIdeal, FractionalIdeal.mem_spanSingleton, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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
⊢ (∃ (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
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'
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)
⊢ ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) y'

Tactic:
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hy'

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
⊢ ∃ (z : R), HSMul.hSMul (β := P) z ((algebraMap R P : (a : R) → P) x : P) = (algebraMap R P : (a : R) → P) (x' • x)

Tactic:
use x'
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
h₂ 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)
⊢ 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]

Premises used: map_mul, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)

Tactic:
⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', rfl⟩, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Submodule.mem_span_singleton, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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 : (algebraMap R P : (a : R) → P) (y' * x) = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)
⊢ ∃ (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)

Tactic:
refine ⟨y' * x, Submodule.mem_span_singleton.mpr ⟨y', rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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)
a₁ 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)
⊢ (algebraMap R P : (a : R) → P) (y' * x) = HSMul.hSMul (β := P) y' ((algebraMap R P : (a : R) → P) x : P)

Tactic:
rw [map_mul, Algebra.smul_def]

Premises used: map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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) ⋯ : (a : P) → P') x) :
          FractionalIdeal S P')
        x_1
⊢ 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')

Tactic:
apply SetLike.ext_iff.mpr

Premises used: Iff.mpr, SetLike.ext_iff
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
mpr :
  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')
      (((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

Tactic:
constructor
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
mp :
  ∃ (z : R),
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : 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

Tactic:
rw [mem_spanSingleton]

Premises used: FractionalIdeal.mem_spanSingleton
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
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) ⋯ : (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'
⊢ ∃ (z : R),
    HSMul.hSMul (β := P') z ((IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') x : P') = y

Tactic:
obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h

Premises used: Iff.mp, FractionalIdeal.mem_canonicalEquiv_apply, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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')
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) ⋯ : (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)
⊢ ∃ (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'

Tactic:
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp hx'

Premises used: FractionalIdeal.mem_spanSingleton, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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') =
    (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') (z • x)
⊢ ∃ (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)

Tactic:
use z
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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')
h₂ h₃ :
  HSMul.hSMul (β := P') z ((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')
⊢ 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)

Tactic:
rw [IsLocalization.map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, IsLocalization.map_smul
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
mpr :
  ∃ (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
⊢ 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:
rw [mem_canonicalEquiv_apply]

Premises used: FractionalIdeal.mem_canonicalEquiv_apply
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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
mpr :
  ∀ (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')
⊢ ∃ (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

Tactic:
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h

Premises used: FractionalIdeal.mem_spanSingleton, Iff.mp, rfl
-- Module: Mathlib.RingTheory.FractionalIdeal.Operations
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'))
h₁ :
  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')
⊢ ∃ (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')

Tactic:
use z • x