awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A ↔
    FormallyEtale.{u_1, u_2} R (Localization.Away f)
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw : Eq (α := Set (PrimeSpectrum A)) ((Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₁ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₂ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₃ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₄ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ∅ ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₅ : Subset (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R] ∪ Module.support A (H1Cotangent R A)) ∅ ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₆ : Subset (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
    Subset (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₇ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
    Subset (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₈ : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R]) ∅ ∧
    Eq (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₉ : Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Eq (α := Set (PrimeSpectrum A)) (Module.support A (H1Cotangent R A)) ∅ ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₁₀ : Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ FormallyEtale R A
have rw₁₁ : Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔
  Subsingleton.{u_2 + 1} Ω[A⁄R] ∧ Subsingleton (H1Cotangent 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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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) (etaleLocus R A)
have rw : IsOpen (X := PrimeSpectrum A) (unramifiedLocus R A ∩ smoothLocus R A)
Tactic: rw [etaleLocus_eq_unramfiedLocus_inter_smoothLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ etaleLocus R A ↔ Etale.{u_1, u_2} R (Localization.Away f)
have rw : FormallyEtale.{u_1, u_2} R (Localization.Away f) ↔ Etale.{u_1, u_2} R (Localization.Away f)
Tactic: rw [basicOpen_subset_etaleLocus_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ Eq (α := Set (PrimeSpectrum A)) (etaleLocus R A) Set.univ ↔ Etale R A
have rw : FormallyEtale R A ↔ Etale R A
Tactic: rw [etaleLocus_eq_univ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Locus (goal)
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
⊢ ∃ f ∉ P, Etale.{u_1, u_2} R (Localization.Away f)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Pi (goal)
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
⊢ FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), FormallyEtale.{u_1, u_3} R (A i)
have 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)
Tactic: simp_rw [FormallyEtale.iff_formallyUnramified_and_formallySmooth, forall_and]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Pi (goal)
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
⊢ 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)
have 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)
Tactic: rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Pi (goal)
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)
⊢ 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)
have 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)
Tactic: rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.QuasiFinite (goal)
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)
⊢ 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)
have 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)
Tactic: ext x