mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
inst✝¹ : ExpChar k p
inst✝ : Algebra.EssFiniteType k K
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
i : (sigmaOpenCover fun i ↦ 𝒰.X i).I₀
⊢ P ((sigmaOpenCover fun i ↦ 𝒰.X i).f i ≫ p)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
h✝ : CharZero k
s : Finset K
hs : adjoin k ↑s = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin k ↑s)) K
t : Finset K
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis k Subtype.val
⊢ Algebra.IsAlgebraic (↥(adjoin k ↑t)) K

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
⊢ ∃ Y p, Surjective p ∧ P p ∧ IsAffine Y

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
obtain _ | ⟨p, hp, hpk⟩ := CharP.exists' k
  · obtain ⟨s, hs⟩ := IntermediateField.fg_top k K
    have : Algebra.IsAlgebraic (Algebra.adjoin k (s : Set K)) K := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      exact Algebra.isIntegral_of_surjective topEquiv.surjective
    obtain ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := k) (s : Set K)
    lift t to Finset K using s.finite_toSet.subset hts
    have : Algebra.IsAlgebraic (IntermediateField.adjoin k (t : Set K)) K := by
      convert! ht.isAlgebraic_field <;> simp
    exact ⟨t, ht, inferInstance⟩
  have : ExpChar k p := .prime hp.out
  have : CharP K p := .of_ringHom_of_ne_zero (algebraMap k K) p hp.out.ne_zero
  refine exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType
    p hp.out fun s hs ↦ ?_
  apply hs.map_of_injective_injective (frobeniusEquiv k p).symm (frobenius K p).toAddMonoidHom <;>
    simp [frobenius, Algebra.smul_def, mul_pow, ← map_pow, frobeniusEquiv_symm_pow]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: ⊢ RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Injective

Goal state before:
pp: ⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
⊢ LinearMap.lTensor S (Algebra.linearMap R T) = ↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Injective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Injective ⇑(algebraMap R T)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ LinearMap.lTensor S (Algebra.linearMap R T) = ↑R (Algebra.linearMap S (S ⊗[R] T) ∘ₗ ↑(AlgebraTensorModule.rid R S S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : FaithfullyFlat R S
H : Function.Surjective ⇑(algebraMap S (S ⊗[R] T))
⊢ Function.Surjective ⇑(algebraMap R T)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f ↦ Function.Surjective ⇑f) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ @Surjective ⊓ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) = @Surjective ⊓ @Flat ⊓ @QuasiCompact

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]

Goal state after:
case refine_1
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
⊢ RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom ↑(Ideal.Quotient.mkₐ (↑Γ(Y, U)) I))) ^ 2 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
S T : C
f : T ⟶ S
hf : P f
⊢ (Over.pullback f).Faithful

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst : HasPushout f g], Q f → P (pushout.inl f g) → P g
A X Y Z : C
f : A ⟶ X
g : A ⟶ Y
inl : X ⟶ Z
inr : Y ⟶ Z
h : IsPushout f g inl inr
hf : Q f
hfst : P inl
⊢ P g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
⊢ e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
Z✝ X✝ Y✝ A✝ : C
f✝ : Z✝ ⟶ X✝
g✝ : Z✝ ⟶ Y✝
inl✝ : X✝ ⟶ A✝
inr✝ : Y✝ ⟶ A✝
inst✝² : Q.IsStableUnderCobaseChange
inst✝¹ : P.HasOfPostcompProperty Q
inst✝ : P.RespectsLeft Q
X Y Z A : C
f : X ⟶ Y
g : X ⟶ Z
inl : Y ⟶ A
inr : Z ⟶ A
h : IsPushout f g inl inr
hf : Q f
hinl : P inl
⊢ P g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
⊢ Spec.map (CommRingCat.ofHom ↑(Ideal.Quotient.mkₐ (↑Γ(Y, U)) I)) ≫ Spec.map (CommRingCat.ofHom ↑g₁) ≫ hV.fromSpec =
    Spec.map (CommRingCat.ofHom ↑(Ideal.Quotient.mkₐ (↑Γ(Y, U)) I)) ≫ Spec.map (CommRingCat.ofHom ↑g₂) ≫ hV.fromSpec

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyClosed (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsClosed (⇑(pullback.snd (Spec.map φ) f) ⁻¹' ⇑(pullback.fst f g) '' s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x✝¹ : CommRing R
x✝ : Algebra (↑Γ(Y, U)) R
I : Ideal R
hI : I ^ 2 = ⊥
g₁ g₂ : ↑Γ(X, V) →ₐ[↑Γ(Y, U)] R
hg₁g₂ : (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₁ = (Ideal.Quotient.mkₐ (↑Γ(Y, U)) I).comp g₂
hg₁ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₁ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
hg₂ : Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom ↑g₂ = CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U))) R)
⊢ (Spec.map (CommRingCat.ofHom ↑g₁) ≫ hV.fromSpec) ≫ f = (Spec.map (CommRingCat.ofHom ↑g₂) ≫ hV.fromSpec) ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
x✝¹ : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyOpen (pullback.fst (Spec.map φ) g)
left✝ : Surjective (Spec.map φ)
right✝ : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
x✝ : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) ⟶ pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsOpen (⇑(pullback.snd (Spec.map φ) f) ⁻¹' ⇑(pullback.fst f g) '' s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
⊢ P.DescendsAlong P'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ DescendsAlong (@UniversallyInjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat) (φ : R ⟶ S),
    Function.Surjective ⇑(ConcreteCategory.hom φ) →
      RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
⊢ FormallyUnramified f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case H₁
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]

Goal state after:
case H₁
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
hf : P (pullback.fst (Spec.map ψ) (Spec.map φ))
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ P (Spec.map φ)

Tactic:
replace hf : P (pullback.fst (Spec.map <| CommRingCat.ofHom <| algebraMap R T)
    (Spec.map <| CommRingCat.ofHom <| algebraMap R S)) := hf

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst✝¹ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑T := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑T))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))
⊢ P (Spec.map φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : P.RespectsIso
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
g : Spec S ⟶ Spec R
h : P' f
hf : P (pullback.fst f g)
⊢ P g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (pullback.fst (Spec.map φ) g)
this✝ : IsAffine Y
this :
  ∀ {Y : Scheme} (g : Y ⟶ Spec R),
    IsIso (pullback.fst (Spec.map φ) g) → IsAffine Y → (∃ T, Y = Spec T) → isomorphisms Scheme g
hY : ¬∃ T, Y = Spec T
⊢ (Y.isoSpec.inv ≫ g) ≫ 𝟙 (Spec R) = Y.isoSpec.inv ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
⊢ CompactSpace ↥X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ IsStandardOpenImmersion R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
h : ∃ r, Away r S
⊢ ∃ r, Away r T

Tactic:
obtain ⟨r, hr⟩ := h

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
r : R
hr : Away r S
⊢ ∃ r, Away r T
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_4
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
h : IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion R T

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ (isomorphisms Scheme).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_4
S' : Type u_5
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsPushout R S R' S'
inst✝ : IsStandardOpenImmersion R S
⊢ IsPushout R R' S S'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).IsStandardOpenImmersion ↔ Algebra.IsStandardOpenImmersion R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.OpenImmersion

Goal state before:
pp: ⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
⊢ Set.range ⇑g ⊆ Set.range ⇑U.ι

Tactic:
by

Goal state after: