awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
x : BasicConstructibleSetData R
h : x ∈ (↑S : Set (BasicConstructibleSetData R))
⊢ IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})ᶜ

Tactic:
exact (isRetrocompact_zeroLocus_compl (Set.finite_singleton _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl, PrimeSpectrum.isRetrocompact_zeroLocus_compl, IsRetrocompact.isConstructible, Set.finite_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ (S : ConstructibleSetData R), S.toSet = s) ↔ IsConstructible s

Tactic:
⟨fun ⟨S, H⟩ ↦ H ▸ S.isConstructible_toSet, fun H ↦ ?_⟩

Premises used: Eq.rec, PrimeSpectrum.ConstructibleSetData.isConstructible_toSet, _private.0.PrimeSpectrum.exists_constructibleSetData_iff.match_1, Iff.intro, Topology.IsConstructible
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
refine : ∀ (H : IsConstructible s), ∃ (S : ConstructibleSetData R), S.toSet = s
⊢ (∃ (S : ConstructibleSetData R), S.toSet = s) ↔ IsConstructible s

Tactic:
refine ⟨fun ⟨S, H⟩ ↦ H ▸ S.isConstructible_toSet, fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
i : R
⊢ IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))

Tactic:
isCompact_basicOpen _

Premises used: PrimeSpectrum.isCompact_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
i : R
⊢ IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))

Tactic:
exact isCompact_basicOpen _

Premises used: PrimeSpectrum.isCompact_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Finite s := hs
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ (S : ConstructibleSetData R),
    S.toSet = (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))

Tactic:
⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩

Premises used: Exists.intro, Singleton.singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
sdiff :
  ConstructibleSetData.toSet
      {{ f := i, n := Nat.card.{u_1} (↑s : Type u_1),
          g := fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
            (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                  i) :
              R) :
          BasicConstructibleSetData R }} =
    (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
⊢ ∃ (S : ConstructibleSetData R),
    S.toSet = (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))

Tactic:
refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
sdiff :
  Eq (α := Set (PrimeSpectrum R))
    (zeroLocus
        (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
          (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                i) :
            R)) \
      zeroLocus {i})
    (zeroLocus s \ zeroLocus {i})
⊢ ConstructibleSetData.toSet
      {{ f := i, n := Nat.card.{u_1} (↑s : Type u_1),
          g := fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
            (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                  i) :
              R) :
          BasicConstructibleSetData R }} =
    (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))

Tactic:
simp only [ConstructibleSetData.toSet, Finset.mem_singleton, BasicConstructibleSetData.toSet,
      Set.iUnion_iUnion_eq_left, basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂,
        compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]

Premises used: Set.compl_iInter₂, PrimeSpectrum.BasicConstructibleSetData.toSet, Finset.mem_singleton, compl_sdiff_compl, Set.biUnion_of_singleton, Set.iUnion_iUnion_eq_left, PrimeSpectrum.zeroLocus_iUnion₂, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.ConstructibleSetData.toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
sdiff :
  (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
      (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
        R)) =
    s
⊢ Eq (α := Set (PrimeSpectrum R))
    (zeroLocus
        (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
          (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                i) :
            R)) \
      zeroLocus {i})
    (zeroLocus s \ zeroLocus {i})

Tactic:
congr! 2
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
sdiff :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
          (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                i) :
            R))
        x ↔
      x ∈ s
⊢ (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
      (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
        R)) =
    s

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
x : R
⊢ Membership.mem (γ := Set R)
      (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
        (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
          R))
      x ↔
    x ∈ s

Tactic:
simp [← (Finite.equivFin s).exists_congr_right, -Nat.card_coe_set_eq]

Premises used: Equiv.exists_congr_right, Set.Elem, Nat.card_coe_set_eq, Finite.equivFin
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s_1 s : Set (PrimeSpectrum R)
hs : IsConstructible s
t : Set (PrimeSpectrum R)
ht : IsConstructible t
Hs : ∃ (S : ConstructibleSetData R), S.toSet = s
Ht : ∃ (S : ConstructibleSetData R), S.toSet = t
union :
  ∀ (S : ConstructibleSetData R) (hs : IsConstructible (X := PrimeSpectrum R) S.toSet),
    ∃ (S_1 : ConstructibleSetData R), S_1.toSet = S.toSet ∪ t
⊢ ∃ (S : ConstructibleSetData R), S.toSet = s ∪ t

Tactic:
obtain ⟨S, rfl⟩ := Hs

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsConstructible t
Ht : ∃ (S : ConstructibleSetData R), S.toSet = t
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
union :
  ∀ (T : ConstructibleSetData R) (ht : IsConstructible (X := PrimeSpectrum R) T.toSet),
    ∃ (S_1 : ConstructibleSetData R), Eq (α := Set (PrimeSpectrum R)) S_1.toSet (S.toSet ∪ T.toSet)
⊢ ∃ (S_1 : ConstructibleSetData R), S_1.toSet = S.toSet ∪ t

Tactic:
obtain ⟨T, rfl⟩ := Ht

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
T : ConstructibleSetData R
ht : IsConstructible (X := PrimeSpectrum R) T.toSet
⊢ ∃ (S_1 : ConstructibleSetData R), Eq (α := Set (PrimeSpectrum R)) S_1.toSet (S.toSet ∪ T.toSet)

Tactic:
⟨S ∪ T, ?_⟩

Premises used: Exists.intro, Union.union
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
T : ConstructibleSetData R
ht : IsConstructible (X := PrimeSpectrum R) T.toSet
union : Eq (α := Set (PrimeSpectrum R)) (S ∪ T).toSet (S.toSet ∪ T.toSet)
⊢ ∃ (S_1 : ConstructibleSetData R), Eq (α := Set (PrimeSpectrum R)) S_1.toSet (S.toSet ∪ T.toSet)

Tactic:
refine ⟨S ∪ T, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
T : ConstructibleSetData R
ht : IsConstructible (X := PrimeSpectrum R) T.toSet
⊢ Eq (α := Set (PrimeSpectrum R)) (S ∪ T).toSet (S.toSet ∪ T.toSet)

Tactic:
simp only [ConstructibleSetData.toSet, Set.biUnion_union, ← Finset.mem_coe, Finset.coe_union]

Premises used: Set.biUnion_union, Finset.mem_coe, PrimeSpectrum.ConstructibleSetData.toSet, Finset.coe_union
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
H : IsConstructible s
isCompact_basis : ∀ (i : R), IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))
sdiff :
  ∀ (i : R) (s : Set R) (hs : s.Finite),
    ∃ (S : ConstructibleSetData R),
      S.toSet = (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
union :
  ∀ (s : Set (PrimeSpectrum R)) (hs : IsConstructible s) (t : Set (PrimeSpectrum R)) (ht : IsConstructible t)
    (Hs : ∃ (S : ConstructibleSetData R), S.toSet = s) (Ht : ∃ (S : ConstructibleSetData R), S.toSet = t),
    ∃ (S : ConstructibleSetData R), S.toSet = s ∪ t
⊢ ∃ (S : ConstructibleSetData R), S.toSet = s

Tactic:
induction s, H using IsConstructible.induction_of_isTopologicalBasis
      _ (isTopologicalBasis_basic_opens (R := R)) with
  | isCompact_basis i => exact isCompact_basicOpen _
  | sdiff i s hs =>
    have : Finite s := hs
    refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
    simp only [ConstructibleSetData.toSet, Finset.mem_singleton, BasicConstructibleSetData.toSet,
      Set.iUnion_iUnion_eq_left, basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂,
        compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
    congr! 2
    ext
    simp [← (Finite.equivFin s).exists_congr_right, -Nat.card_coe_set_eq]
  | union s hs t ht Hs Ht =>
    obtain ⟨S, rfl⟩ := Hs
    obtain ⟨T, rfl⟩ := Ht
    refine ⟨S ∪ T, ?_⟩
    simp only [ConstructibleSetData.toSet, Set.biUnion_union, ← Finset.mem_coe, Finset.coe_union]

Premises used: Set.compl_iInter₂, PrimeSpectrum.BasicConstructibleSetData.toSet, Finset.mem_singleton, compl_sdiff_compl, Set.biUnion_of_singleton, Nat.card_coe_set_eq, Set.biUnion_union, SDiff.sdiff, Set.iUnion_iUnion_eq_left, PrimeSpectrum.zeroLocus_iUnion₂, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, PrimeSpectrum.isCompact_basicOpen, Finset.mem_coe, PrimeSpectrum.ConstructibleSetData.toSet, rfl, Finset.coe_union
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : IsConstructible s
obtain :
  ∀ (s : ConstructibleSetData R) (hs : IsConstructible (X := PrimeSpectrum R) s.toSet),
    ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s.toSet
⊢ ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s

Tactic:
obtain ⟨s, rfl⟩ := exists_constructibleSetData_iff.mpr hs

Premises used: Iff.mpr, PrimeSpectrum.exists_constructibleSetData_iff, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
⊢ ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s.toSet

Tactic:
⟨Π i : s, Localization.Away (Ideal.Quotient.mk (Ideal.span (Set.range i.1.g)) i.1.f),
    inferInstance, algebraMap _ _, ?_⟩

Premises used: Algebra.algebraMap, inferInstance, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
refine :
  Eq (α := Set (PrimeSpectrum R))
    (Set.range (ι :=
      PrimeSpectrum
        ((i : ↥s) →
          Localization.Away (M :=
            HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
            ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                  (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                (↑i : BasicConstructibleSetData R).f :
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))
      (comap
        (algebraMap R
          ((i : ↥s) →
            Localization.Away (M :=
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
              ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                    (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                  (↑i : BasicConstructibleSetData R).f :
                HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))))
    s.toSet
⊢ ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s.toSet

Tactic:
refine ⟨Π i : s, Localization.Away (Ideal.Quotient.mk (Ideal.span (Set.range i.1.g)) i.1.f),
    inferInstance, algebraMap _ _, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderSpecialization s
hs' : IsConstructible s
obtain :
  ∀ (S : Type u_4) (w : CommRing S) (f : R →+* S) (hs : StableUnderSpecialization (Set.range (comap f)))
    (hs' : IsConstructible (Set.range (comap f))), IsClosed (Set.range (comap f))
⊢ IsClosed s

Tactic:
obtain ⟨S, _, f, rfl⟩ := exists_range_eq_of_isConstructible hs'

Premises used: PrimeSpectrum.exists_range_eq_of_isConstructible, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
S : Type u_4
w : CommRing S
f : R →+* S
hs : StableUnderSpecialization (Set.range (comap f))
hs' : IsConstructible (Set.range (comap f))
⊢ IsClosed (Set.range (comap f))

Tactic:
isClosed_range_of_stableUnderSpecialization _ hs

Premises used: PrimeSpectrum.isClosed_range_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
S : Type u_4
w : CommRing S
f : R →+* S
hs : StableUnderSpecialization (Set.range (comap f))
hs' : IsConstructible (Set.range (comap f))
⊢ IsClosed (Set.range (comap f))

Tactic:
exact isClosed_range_of_stableUnderSpecialization _ hs

Premises used: PrimeSpectrum.isClosed_range_of_stableUnderSpecialization
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
rw : IsClosed sᶜ
⊢ IsOpen s

Tactic:
rw [← isClosed_compl_iff]

Premises used: isClosed_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsClosed sᶜ

Tactic:
isClosed_of_stableUnderSpecialization_of_isConstructible hs.compl hs'.compl

Premises used: Topology.IsConstructible.compl, StableUnderGeneralization.compl, PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsClosed sᶜ

Tactic:
exact isClosed_of_stableUnderSpecialization_of_isConstructible hs.compl hs'.compl

Premises used: Topology.IsConstructible.compl, StableUnderGeneralization.compl, PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible
-- Module: Mathlib.RingTheory.Spectrum.Prime.Defs
Goal:
R : Type u_1
inst : CommSemiring R
x y : PrimeSpectrum R
⊢ x.asIdeal ≤ y.asIdeal ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Defs
Goal:
R : Type u_1
inst : CommSemiring R
x y : PrimeSpectrum R
⊢ x.asIdeal < y.asIdeal ↔ x < y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔
    Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Module.freeLocus
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
apply : LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[(↑e : Localization.AtPrime p.asIdeal →+* Rₚ)] Mₚ
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔ Free Rₚ Mₚ

Tactic:
apply Module.Free.iff_of_equiv (σ := e)

Premises used: Module.Free.iff_of_equiv
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
refine :
  ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun (m • x) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
        (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ) m : Rₚ)
        ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)
⊢ LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[(↑e : Localization.AtPrime p.asIdeal →+* Rₚ)] Mₚ

Tactic:
refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }

Premises used: IsLocalizedModule.iso, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
r : Localization.AtPrime p.asIdeal
x : LocalizedModule p.asIdeal.primeCompl M
obtain :
  ∀ (r : R) (s : ↥p.asIdeal.primeCompl),
    (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
        (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s)
          x) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
        (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ)
            (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) :
          Rₚ)
        ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)
⊢ (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun (r • x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
      (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ) r : Rₚ)
      ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)

Tactic:
obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq p.asIdeal.primeCompl r

Premises used: Ideal.primeCompl, PrimeSpectrum.asIdeal, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
x : LocalizedModule p.asIdeal.primeCompl M
r : R
s : ↥p.asIdeal.primeCompl
a :
  Eq (α := Mₚ)
    ((((algebraMap R (End R Mₚ) : (a : R) → End R Mₚ) (↑s : R) : End R Mₚ) : (a : Mₚ) → Mₚ)
        ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
          (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s)
            x)) :
      Mₚ)
    ((((algebraMap R (End R Mₚ) : (a : R) → End R Mₚ) (↑s : R) : End R Mₚ) : (a : Mₚ) → Mₚ)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
          (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ)
              (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) :
            Rₚ)
          ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
            x)) :
      Mₚ)
⊢ (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun
      (HSMul.hSMul (α := Localization.AtPrime p.asIdeal) (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
      (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ)
          (IsLocalization.mk' (Localization.AtPrime p.asIdeal) r s) :
        Rₚ)
      ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)

Tactic:
apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, IsLocalizedModule.map_units