awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
h₁ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
h₂ :
  LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
(Algebra.formallyEtale_iff _ _).trans
    (and_congr h₁.subsingleton_congr.symm h₂.subsingleton_congr.symm)

Premises used: Set.Mem, Equiv.subsingleton_congr, Algebra.etaleLocus, setOf, Algebra.formallyEtale_iff, LinearEquiv.toAddEquiv, Iff.trans, AddEquiv.toEquiv, Iff.symm, and_congr
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
h₁ : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
h₂ :
  LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R]) ∧
      Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
exact (Algebra.formallyEtale_iff _ _).trans
    (and_congr h₁.subsingleton_congr.symm h₂.subsingleton_congr.symm)

Premises used: Equiv.subsingleton_congr, Algebra.formallyEtale_iff, LinearEquiv.toAddEquiv, Iff.trans, AddEquiv.toEquiv, Iff.symm, and_congr
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
rw :
  Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ∧ Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ↔
    Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R] ∧ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f))
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A ↔
    FormallyEtale.{u_1, u_2} R (Localization.Away f)

Tactic:
rw [etaleLocus_eq_compl_support, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl, Set.subset_compl_comm, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset,
    ← LocalizedModule.subsingleton_iff_support_subset, formallyEtale_iff]

Premises used: compl_compl, Set.subset_inter_iff, Set.subset_compl_comm, Algebra.formallyEtale_iff, LocalizedModule.subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Algebra.etaleLocus_eq_compl_support
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ∧ Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ↔
    Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R] ∧ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f))

Tactic:
and_congr (IsLocalizedModule.iso (.powers f)
    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
    (IsLocalizedModule.iso (.powers f)
      (H1Cotangent.map R R A (Localization.Away f))).subsingleton_congr

Premises used: IsLocalizedModule.iso, Equiv.subsingleton_congr, Localization.Away, Algebra.H1Cotangent.map, LinearEquiv.toAddEquiv, Submonoid.powers, AddEquiv.toEquiv, and_congr, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ∧ Subsingleton (LocalizedModule.Away f (H1Cotangent R A)) ↔
    Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R] ∧ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.Away f))

Tactic:
exact and_congr (IsLocalizedModule.iso (.powers f)
    (KaehlerDifferential.map R R A (Localization.Away f))).subsingleton_congr
    (IsLocalizedModule.iso (.powers f)
      (H1Cotangent.map R R A (Localization.Away f))).subsingleton_congr

Premises used: IsLocalizedModule.iso, Equiv.subsingleton_congr, Localization.Away, Algebra.H1Cotangent.map, LinearEquiv.toAddEquiv, Submonoid.powers, AddEquiv.toEquiv, and_congr, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw :
  Eq (α := Set (PrimeSpectrum A)) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ) Set.univ ↔
    FormallyEtale R A
rw₁ :
  Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A))ᶜ Set.univ ↔
    FormallyEtale R A
rw₂ :
  Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ↔
    FormallyEtale R A
rw₃ :
  Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ↔ FormallyEtale R A
rw₄ :
  Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ∅ ↔ FormallyEtale R A
rw₅ :
  Subset (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ∅ ↔
    FormallyEtale R A
rw₆ :
  Subset (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
      Subset (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
    FormallyEtale R A
rw₇ :
  Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
      Subset (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
    FormallyEtale R A
rw₈ :
  Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
      Eq (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
    FormallyEtale R A
rw₉ :
  Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Eq (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
    FormallyEtale R A
rw₁₀ : Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ FormallyEtale R A
rw₁₁ rw₁₂ :
  Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔
    Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A)
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A

Tactic:
rw [etaleLocus_eq_compl_support, ← Set.compl_union, compl_eq_comm, Set.compl_univ, eq_comm,
    ← Set.subset_empty_iff, Set.union_subset_iff, Set.subset_empty_iff, Set.subset_empty_iff,
    Module.support_eq_empty_iff, Module.support_eq_empty_iff, Algebra.formallyEtale_iff]

Premises used: Set.compl_union, Set.union_subset_iff, Algebra.formallyEtale_iff, Set.compl_univ, eq_comm, Module.support_eq_empty_iff, Set.subset_empty_iff, compl_eq_comm, Algebra.etaleLocus_eq_compl_support
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
rw : IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A ∩ smoothLocus R A)
⊢ IsOpen (X := PrimeSpectrum A) (etaleLocus R A)

Tactic:
rw [etaleLocus_eq_unramfiedLocus_inter_smoothLocus]

Premises used: Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A ∩ smoothLocus R A)

Tactic:
isOpen_unramifiedLocus.inter isOpen_smoothLocus

Premises used: Algebra.isOpen_smoothLocus, Algebra.isOpen_unramifiedLocus, IsOpen.inter
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A ∩ smoothLocus R A)

Tactic:
exact isOpen_unramifiedLocus.inter isOpen_smoothLocus

Premises used: Algebra.isOpen_smoothLocus, Algebra.isOpen_unramifiedLocus, IsOpen.inter
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
rw : FormallyEtale.{u_1, u_2} R (Localization.Away f) ↔ Etale.{u_1, u_2} R (Localization.Away f)
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A ↔ Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
rw [basicOpen_subset_etaleLocus_iff]

Premises used: Algebra.basicOpen_subset_etaleLocus_iff
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ FormallyEtale.{u_1, u_2} R (Localization.Away f) ↔ Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

Premises used: Algebra.Etale.mk, inferInstance, Iff.intro
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
f : A
⊢ FormallyEtale.{u_1, u_2} R (Localization.Away f) ↔ Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
rw : FormallyEtale R A ↔ Etale R A
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ Etale R A

Tactic:
rw [etaleLocus_eq_univ_iff]

Premises used: Algebra.etaleLocus_eq_univ_iff
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ FormallyEtale R A ↔ Etale R A

Tactic:
⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

Premises used: Algebra.Etale.mk, inferInstance, Iff.intro
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
⊢ FormallyEtale R A ↔ Etale R A

Tactic:
refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
P : Ideal A
inst_4 : P.IsPrime
inst_5 : IsEtaleAt R P
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (etaleLocus R A) { asIdeal := P, isPrime := inst_4 : PrimeSpectrum A }

Tactic:
assumption
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
P : Ideal A
inst_4 : P.IsPrime
inst_5 : IsEtaleAt R P
obtain :
  ∀ (r : A)
    (hpr :
      { asIdeal := P, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)))
    (hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A),
    ∃ f ∉ P, Etale.{u_1, u_2} R (Localization.Away f)
⊢ ∃ f ∉ P, Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hpr, hr⟩ :=
    PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open
      (show ⟨P, ‹_›⟩ ∈ etaleLocus R A by assumption) isOpen_etaleLocus

Premises used: Algebra.isOpen_etaleLocus, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
P : Ideal A
inst_4 : P.IsPrime
inst_5 : IsEtaleAt R P
r : A
hpr : { asIdeal := P, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A))
hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A
⊢ ∃ f ∉ P, Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
⟨r, hpr, ⟨basicOpen_subset_etaleLocus_iff.mp hr, .of_isLocalizationAway r⟩⟩

Premises used: Algebra.Etale.mk, Algebra.basicOpen_subset_etaleLocus_iff, And.intro, Exists.intro, Iff.mp, Algebra.FinitePresentation.of_isLocalizationAway
-- Module: Mathlib.RingTheory.Etale.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
P : Ideal A
inst_4 : P.IsPrime
inst_5 : IsEtaleAt R P
r : A
hpr : { asIdeal := P, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A))
hr : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A
⊢ ∃ f ∉ P, Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
exact ⟨r, hpr, ⟨basicOpen_subset_etaleLocus_iff.mp hr, .of_isLocalizationAway r⟩⟩
-- Module: Mathlib.RingTheory.Etale.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : Finite I
simp_rw :
  FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified.{u_3, u_1} R (A x)) ∧ ∀ (x : I), FormallySmooth.{u_1, u_3} R (A x)
⊢ FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), FormallyEtale.{u_1, u_3} R (A i)

Tactic:
simp_rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, forall_and]

Premises used: Algebra.FormallyEtale.iff_formallyUnramified_and_formallySmooth, forall_and
-- Module: Mathlib.RingTheory.Etale.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : Finite I
rw :
  (∀ (i : I), FormallyUnramified.{u_3, u_1} R (A i)) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified.{u_3, u_1} R (A x)) ∧ ∀ (x : I), FormallySmooth.{u_1, u_3} R (A x)
rw₁ rw₂ :
  ((∀ (i : I), FormallyUnramified.{u_3, u_1} R (A i)) ∧ ∀ (i : I), FormallySmooth.{u_1, u_3} R (A i)) ↔
    (∀ (x : I), FormallyUnramified.{u_3, u_1} R (A x)) ∧ ∀ (x : I), FormallySmooth.{u_1, u_3} R (A x)
⊢ FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified.{u_3, u_1} R (A x)) ∧ ∀ (x : I), FormallySmooth.{u_1, u_3} R (A x)

Tactic:
rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]

Premises used: Algebra.FormallyUnramified.pi_iff, Algebra.FormallySmooth.pi_iff
-- Module: Mathlib.RingTheory.Etale.Pi
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : Finite I
inst_4 : ∀ (i : I), FormallyEtale.{u_1, u_3} R (A i)
⊢ FormallyEtale R ((i : I) → A i)

Tactic:
.of_formallyUnramified_and_formallySmooth

Premises used: Algebra.FormallyEtale.of_formallyUnramified_and_formallySmooth
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
Q : (↑(p.primesOver S) : Type u_3)
h :
  ∀ (x : S),
    Membership.mem (γ := Ideal S)
        (comap (F := S →+* R' ⊗[R] S) (↑Algebra.TensorProduct.includeRight : S →+* R' ⊗[R] S)
          (↑((OrderIso.symm (fiberIsoOfBijectiveResidueField H) :
                  (a : (↑(p.primesOver S) : Type u_3)) → (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3)))
                Q) :
            Ideal (R' ⊗[R] S)))
        x ↔
      x ∈ (↑Q : Ideal S)
⊢ comap (F := S →+* R' ⊗[R] S) (↑Algebra.TensorProduct.includeRight : S →+* R' ⊗[R] S)
      (↑((OrderIso.symm (fiberIsoOfBijectiveResidueField H) :
              (a : (↑(p.primesOver S) : Type u_3)) → (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3)))
            Q) :
        Ideal (R' ⊗[R] S)) =
    (↑Q : Ideal S)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
Q : (↑(p.primesOver S) : Type u_3)
x : S
⊢ Membership.mem (γ := Ideal S)
      (comap (F := S →+* R' ⊗[R] S) (↑Algebra.TensorProduct.includeRight : S →+* R' ⊗[R] S)
        (↑((OrderIso.symm (fiberIsoOfBijectiveResidueField H) :
                (a : (↑(p.primesOver S) : Type u_3)) → (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3)))
              Q) :
          Ideal (R' ⊗[R] S)))
      x ↔
    x ∈ (↑Q : Ideal S)

Tactic:
simp [Ideal.fiberIsoOfBijectiveResidueField,
    PrimeSpectrum.primesOverOrderIsoFiber, PrimeSpectrum.preimageOrderIsoFiber,
    PrimeSpectrum.preimageEquivFiber]

Premises used: PrimeSpectrum.preimageEquivFiber, PrimeSpectrum.primesOverOrderIsoFiber, Ideal.fiberIsoOfBijectiveResidueField, PrimeSpectrum.preimageOrderIsoFiber
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
Q : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))
⊢ Eq (α := Ideal S)
    (↑((fiberIsoOfBijectiveResidueField H :
            (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
          Q) :
      Ideal S)
    (comap (F := S →ₐ[R] R' ⊗[R] S) Algebra.TensorProduct.includeRight (↑Q : Ideal (R' ⊗[R] S)))

Tactic:
simpa using (Ideal.comap_fiberIsoOfBijectiveResidueField_symm H
    (Ideal.fiberIsoOfBijectiveResidueField H Q)).symm

Premises used: Ideal.fiberIsoOfBijectiveResidueField, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst_8 : P₁.IsPrime
inst_9 : P₂.IsPrime
inst_10 : P₁.LiesOver q
inst_11 : P₂.LiesOver q
H₂ :
  Eq (α := Ideal S) (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₁)
    (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₂)
a :
  Eq.{u_3 + 1} (α := Ideal S)
    (↑((fiberIsoOfBijectiveResidueField H :
            (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
          (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
            Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₁ ⋯)) :
      Ideal S)
    (↑((fiberIsoOfBijectiveResidueField H :
            (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
          (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
            Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₂ ⋯)) :
      Ideal S)
⊢ Eq.{u_3 + 1} (α := (↑(p.primesOver S) : Type u_3))
    ((fiberIsoOfBijectiveResidueField H :
          (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
        (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
          Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₁ ⋯) :
      (↑(p.primesOver S) : Type u_3))
    ((fiberIsoOfBijectiveResidueField H :
          (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
        (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
          Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₂ ⋯) :
      (↑(p.primesOver S) : Type u_3))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst_8 : P₁.IsPrime
inst_9 : P₂.IsPrime
inst_10 : P₁.LiesOver q
inst_11 : P₂.LiesOver q
H₂ :
  Eq (α := Ideal S) (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₁)
    (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₂)
⊢ Eq.{u_3 + 1} (α := Ideal S)
    (↑((fiberIsoOfBijectiveResidueField H :
            (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
          (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
            Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₁ ⋯)) :
      Ideal S)
    (↑((fiberIsoOfBijectiveResidueField H :
            (a : (↑(q.primesOver (R' ⊗[R] S)) : Type (max u_2 u_3))) → (↑(p.primesOver S) : Type u_3))
          (Subtype.mk (p := fun (x : Ideal (R' ⊗[R] S)) ↦
            Membership.mem (γ := Set (Ideal (R' ⊗[R] S))) (q.primesOver (R' ⊗[R] S)) x) P₂ ⋯)) :
      Ideal S)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing R'
inst_2 : CommRing S
inst_3 : Algebra R R'
inst_4 : Algebra R S
p : Ideal R
q : Ideal R'
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := p.ResidueField) (β := q.ResidueField)
    (⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯) : (a : p.ResidueField) → q.ResidueField)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst_8 : P₁.IsPrime
inst_9 : P₂.IsPrime
inst_10 : P₁.LiesOver q
inst_11 : P₂.LiesOver q
H₂ :
  Eq (α := Ideal S) (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₁)
    (comap (F := S →+* R' ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) P₂)
⊢ P₁ = P₂

Tactic:
refine congr_arg Subtype.val ((Ideal.fiberIsoOfBijectiveResidueField
  (S := S) H).injective (a₁ := ⟨P₁, ‹_›, ‹_›⟩) (a₂ := ⟨P₂, ‹_›, ‹_›⟩) (by ext1; simpa))

Premises used: congr_arg, Ideal.fiberIsoOfBijectiveResidueField, OrderIso.injective, Subtype.val
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra.FiniteType R T
inst_6 : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg :
  Function.Surjective.{v + 1, u_1 + 1} (α := Away g) (β := Away (M := T) ((f : (a : S) → T) g : T))
    (⇑(awayMapₐ f g) : (a : Away g) → Away ((f : (a : S) → T) g))
p : Ideal R
inst_7 : p.IsPrime
hgp : IsUnit (M := p.Fiber S) (1 ⊗ₜ[R] g)
⊢ IsClosed (X := PrimeSpectrum R)
    (Set.image (α := PrimeSpectrum S) (PrimeSpectrum.comap (algebraMap R S)) (PrimeSpectrum.zeroLocus {g}))

Tactic:
have := PrimeSpectrum.isClosedMap_comap_of_isIntegral (algebraMap R S)
    (algebraMap_isIntegral_iff.mpr ‹_›) _ (PrimeSpectrum.isClosed_zeroLocus {g})