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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x : P
hb : Membership.mem (γ := Submodule R P) (span R s) x
⊢ IsInteger.{u_1, u_2} R (S := P) 0

Tactic:
isInteger_zero

Premises used: IsLocalization.isInteger_zero
-- 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x : P
hb : Membership.mem (γ := Submodule R P) (span R s) x
⊢ IsInteger.{u_1, u_2} R (S := P) 0

Tactic:
exact isInteger_zero

Premises used: IsLocalization.isInteger_zero
-- 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s) x_1
x y : P
h_2 : Membership.mem (γ := Submodule R P) (span R s) x
h_3 : Membership.mem (γ := Submodule R P) (span R s) y
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
rw : IsInteger R (a • x + a • y)
⊢ IsInteger R (a • (x + y))

Tactic:
rw [smul_add]

Premises used: smul_add
-- 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s) x_1
x y : P
h_2 : Membership.mem (γ := Submodule R P) (span R s) x
h_3 : Membership.mem (γ := Submodule R P) (span R s) y
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • x + a • y)

Tactic:
isInteger_add hx hy

Premises used: IsLocalization.isInteger_add
-- 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
s : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s) x_1
x y : P
h_2 : Membership.mem (γ := Submodule R P) (span R s) x
h_3 : Membership.mem (γ := Submodule R P) (span R s) y
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • x + a • y)

Tactic:
exact isInteger_add hx hy

Premises used: IsLocalization.isInteger_add
-- 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
s_1 : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s_1, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s_1, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s_1) x_1
s : R
x : P
h_2 : Membership.mem (γ := Submodule R P) (span R s_1) x
hx : IsInteger R (a • x)
rw : IsInteger R (s • a • x)
⊢ IsInteger R (a • s • x)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
s_1 : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s_1, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s_1, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s_1) x_1
s : R
x : P
h_2 : Membership.mem (γ := Submodule R P) (span R s_1) x
hx : IsInteger R (a • x)
⊢ IsInteger R (s • a • x)

Tactic:
isInteger_smul hx

Premises used: IsLocalization.isInteger_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
s_1 : Set P
h_1 : ∃ a ∈ S, ∀ b ∈ s_1, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s_1, IsInteger R (a • b)
x_1 : P
hb : Membership.mem (γ := Submodule R P) (span R s_1) x_1
s : R
x : P
h_2 : Membership.mem (γ := Submodule R P) (span R s_1) x
hx : IsInteger R (a • x)
⊢ IsInteger R (s • a • x)

Tactic:
exact isInteger_smul hx

Premises used: IsLocalization.isInteger_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
I : Submodule R P
hI : I.FG
rcases : ∀ (I : Finset P), IsFractional S (span R (↑I : Set P))
⊢ IsFractional S I

Tactic:
rcases hI with ⟨I, rfl⟩

Premises used: 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
I : Finset P
rcases :
  ∀ (s : R) (hs1 : s ∈ S) (hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)),
    IsFractional S (span R (↑I : Set P))
⊢ IsFractional S (span R (↑I : Set P))

Tactic:
rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩

Premises used: IsLocalization.exist_integer_multiples_of_finset
-- 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
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)
rw : ∃ a ∈ S, ∀ b ∈ (↑I : Set P), IsInteger R (a • b)
⊢ IsFractional S (span R (↑I : Set P))

Tactic:
rw [isFractional_span_iff]

Premises used: FractionalIdeal.isFractional_span_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
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)
⊢ ∃ a ∈ S, ∀ b ∈ (↑I : Set P), IsInteger R (a • b)

Tactic:
⟨s, hs1, hs⟩

Premises used: And.intro, Exists.intro
-- 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
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) s hs1) : R) • a)
⊢ ∃ a ∈ S, ∀ b ∈ (↑I : Set P), IsInteger R (a • b)

Tactic:
exact ⟨s, hs1, hs⟩
-- 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
I J : FractionalIdeal S P
x : P
hx : x ∈ I * J
⊢ x ∈ (↑I : Submodule R P) * (↑J : Submodule R P)

Tactic:
simpa using mem_coe.mpr hx

Premises used: Iff.mpr, FractionalIdeal.mem_coe
-- 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
I : (Submodule R P)ˣ
⊢ IsFractional S (↑I : Submodule R P)

Tactic:
FractionalIdeal.isFractional_of_fg (fg_unit _)

Premises used: FractionalIdeal.isFractional_of_fg, Submodule.fg_unit
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
rw :
  (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) =
    1
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯)) :
      Submodule R P) =
    (↑1 : Submodule R P)

Tactic:
rw [coe_mul, coe_one]

Premises used: FractionalIdeal.coe_one, FractionalIdeal.coe_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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) =
    1

Tactic:
I.mul_inv

Premises used: Set.Mem, Units.mul_inv
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) =
    1

Tactic:
exact I.mul_inv

Premises used: Units.mul_inv
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
rw :
  (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) =
    1
⊢ (↑(HMul.hMul (α := FractionalIdeal S P)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯)
          (Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯)) :
      Submodule R P) =
    (↑1 : Submodule R P)

Tactic:
rw [coe_mul, coe_one]

Premises used: FractionalIdeal.coe_one, FractionalIdeal.coe_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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) =
    1

Tactic:
I.inv_mul

Premises used: Set.Mem, Units.inv_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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I_1 J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
I : (Submodule R P)ˣ
⊢ (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I⁻¹ : Submodule R P) ⋯) : Submodule R P) *
      (↑(Subtype.mk (p := fun (I : Submodule R P) ↦ IsFractional S I) (↑I : Submodule R P) ⋯) : Submodule R P) =
    1

Tactic:
exact I.inv_mul

Premises used: Units.inv_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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
I : Ideal R
⊢ FG.{u_1, u_2} (M := P) (↑(↑I : FractionalIdeal S P) : Submodule R P) ↔ I.FG

Tactic:
coeSubmodule_fg _ inj _

Premises used: Submodule.FG, Ideal.FG, FractionalIdeal.coeToSubmodule, Submodule.map, IsLocalization.coeSubmodule_fg, IsLocalization.coeSubmodule
-- 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
I : (FractionalIdeal S P)ˣ
⊢ (↑(↑I : FractionalIdeal S P) : Submodule R P).FG

Tactic:
Submodule.fg_unit <| Units.map (coeSubmoduleHom S P).toMonoidHom I

Premises used: FractionalIdeal.coeSubmoduleHom, FractionalIdeal.coeToSubmodule, RingHom.toMonoidHom, DFunLike.coe, Units.map, Submodule.fg_unit
-- 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
I : FractionalIdeal S P
h : IsUnit I
⊢ (↑I : Submodule R P).FG

Tactic:
fg_unit h.unit

Premises used: FractionalIdeal.fg_unit, IsUnit.unit
-- 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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
I : Ideal R
h : IsUnit.{u_2} (M := FractionalIdeal S P) (↑I : FractionalIdeal S P)
rw : FG.{u_1, u_2} (M := P) (↑(↑I : FractionalIdeal S P) : Submodule R P)
⊢ I.FG

Tactic:
rw [← coeIdeal_fg S inj I]

Premises used: FractionalIdeal.coeIdeal_fg
-- 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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
I : Ideal R
h : IsUnit.{u_2} (M := FractionalIdeal S P) (↑I : FractionalIdeal S P)
⊢ FG.{u_1, u_2} (M := P) (↑(↑I : FractionalIdeal S P) : Submodule R P)

Tactic:
FractionalIdeal.fg_of_isUnit (R := R) I h

Premises used: FractionalIdeal.fg_of_isUnit, FractionalIdeal.coeIdeal
-- 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
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := P) (⇑(algebraMap R P) : (a : R) → P)
I : Ideal R
h : IsUnit.{u_2} (M := FractionalIdeal S P) (↑I : FractionalIdeal S P)
⊢ FG.{u_1, u_2} (M := P) (↑(↑I : FractionalIdeal S P) : Submodule R P)

Tactic:
exact FractionalIdeal.fg_of_isUnit (R := R) I h

Premises used: FractionalIdeal.fg_of_isUnit, FractionalIdeal.coeIdeal
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
P'' : Type u_4
inst_5 : CommRing P''
inst_6 : Algebra R P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
inst_7 : IsLocalization S P
inst_8 : IsLocalization S P'
rw : Submonoid.map (F := R →* R) (MonoidHom.id R) S = S
rw₁ rw₂ : S = S
⊢ Submonoid.map (F := R →* R) (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S

Tactic:
rw [RingEquiv.toMonoidHom_refl, Submonoid.map_id]

Premises used: Submonoid.map_id, RingEquiv.toMonoidHom_refl
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P
x : P'
rw :
  (∃ x_1 ∈ I,
      ((↑(let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) :
              P →ₐ[R] P') :
            (a : P) → P')
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y = x
⊢ Membership.mem (γ := FractionalIdeal S P')
      (((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
            (a : FractionalIdeal S P) → FractionalIdeal S P')
          I :
        FractionalIdeal S P')
      x ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y = x

Tactic:
rw [canonicalEquiv, mapEquiv_apply, mem_map]

Premises used: FractionalIdeal.mapEquiv_apply, FractionalIdeal.mem_map, FractionalIdeal.canonicalEquiv
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ (∃ x_1 ∈ I,
      ((↑(let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) :
              P →ₐ[R] P') :
            (a : P) → P')
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y = x

Tactic:
⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Premises used: RingEquiv.toEquiv, RingEquiv.refl, IsLocalization.map, AlgEquiv.toAlgHom, _private.0.FractionalIdeal.mem_canonicalEquiv_apply.match_1, Membership.mem, Exists, FractionalIdeal.definition._proof_3._@.2078496209._hygCtx._hyg.2, FractionalIdeal.definition._proof_6._@.2078496209._hygCtx._hyg.2, IsLocalization.ringEquivOfRingEquiv, AlgEquiv.mk, FractionalIdeal.definition._proof_4._@.2078496209._hygCtx._hyg.2, And, And.intro, Iff.intro, Exists.intro, _private.0.FractionalIdeal.mem_canonicalEquiv_apply.match_2, FractionalIdeal.definition._proof_5._@.2078496209._hygCtx._hyg.2, RingHom.id, Eq, DFunLike.coe
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ (∃ x_1 ∈ I,
      ((↑(let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }) :
              P →ₐ[R] P') :
            (a : P) → P')
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P' (RingHom.id R) ⋯ : (a : P) → P') y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
x : P
rw :
  (∃ x_1 ∈ I,
      ((↑(AlgEquiv.symm
                  (let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })) :
              P' →ₐ[R] P) :
            (a : P') → P)
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P (RingHom.id R) ⋯ : (a : P') → P) y = x
⊢ Membership.mem (γ := FractionalIdeal S P)
      (((RingEquiv.symm (canonicalEquiv S P P') : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
            (a : FractionalIdeal S P') → FractionalIdeal S P)
          I :
        FractionalIdeal S P)
      x ↔
    Membership.mem (γ := FractionalIdeal S P)
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
            (a : FractionalIdeal S P') → FractionalIdeal S P)
          I :
        FractionalIdeal S P)
      x

Tactic:
rw [mem_canonicalEquiv_apply, canonicalEquiv, mapEquiv_symm, mapEquiv_apply,
        mem_map]

Premises used: FractionalIdeal.mapEquiv_apply, FractionalIdeal.mapEquiv_symm, FractionalIdeal.mem_map, FractionalIdeal.canonicalEquiv, 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ (∃ x_1 ∈ I,
      ((↑(AlgEquiv.symm
                  (let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })) :
              P' →ₐ[R] P) :
            (a : P') → P)
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P (RingHom.id R) ⋯ : (a : P') → P) y = x

Tactic:
⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Premises used: RingEquiv.toEquiv, RingEquiv.refl, IsLocalization.map, AlgEquiv.toAlgHom, AlgEquiv.symm, Membership.mem, Exists, FractionalIdeal.definition._proof_3._@.2078496209._hygCtx._hyg.2, FractionalIdeal.definition._proof_6._@.2078496209._hygCtx._hyg.2, IsLocalization.ringEquivOfRingEquiv, AlgEquiv.mk, FractionalIdeal.definition._proof_4._@.2078496209._hygCtx._hyg.2, _private.0.FractionalIdeal.canonicalEquiv_symm.match_2, And, And.intro, Iff.intro, Exists.intro, FractionalIdeal.definition._proof_5._@.2078496209._hygCtx._hyg.2, RingHom.id, Eq, DFunLike.coe, _private.0.FractionalIdeal.canonicalEquiv_symm.match_1
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ (∃ x_1 ∈ I,
      ((↑(AlgEquiv.symm
                  (let __src : P ≃+* P' := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
                  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })) :
              P' →ₐ[R] P) :
            (a : P') → P)
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map (M := S) (T := S) P (RingHom.id R) ⋯ : (a : P') → P) y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩
-- 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
P' : Type u_3
inst_3 : CommRing P'
inst_4 : Algebra R P'
inst_5 : IsLocalization S P
inst_6 : IsLocalization S P'
I : FractionalIdeal S P'
rw :
  ((RingEquiv.symm (canonicalEquiv S P' P) : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
          (a : FractionalIdeal S P') → FractionalIdeal S P)
        I) =
    I
rw₁ rw₂ : I = I
⊢ ((canonicalEquiv S P P' : RingEquiv.{u_2, u_3} (FractionalIdeal S P) (FractionalIdeal S P')) :
        (a : FractionalIdeal S P) → FractionalIdeal S P')
      (((canonicalEquiv S P' P : RingEquiv.{u_3, u_2} (FractionalIdeal S P') (FractionalIdeal S P)) :
          (a : FractionalIdeal S P') → FractionalIdeal S P)
        I) =
    I

Tactic:
rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]

Premises used: FractionalIdeal.canonicalEquiv_symm, RingEquiv.symm_apply_apply