mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
S : Sieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
⊢ Presieve.IsSheafFor F S.arrows

Tactic:
refine (E.isStronglySheafFor hF).isSheafFor_sieve_of_pullback ?_ h₁ h₂

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
S : Sieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ (uliftFunctor.mapCone c).pt.str ≤
    ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str

Tactic:
rw [le_iInf_iff]
      rintro j s ⟨t, ht, rfl⟩
      refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
      apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
      apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht

Goal state after:
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
i : J✝
t : Set ↑(K.obj i)
ht : IsOpen t
⊢ ULift.down ⁻¹' ⇑(ConcreteCategory.hom (c.π.app i)) ⁻¹' t ∈ ⋃ i, {s | IsOpen s}

Tactic:
rw [Set.mem_iUnion]

Goal state after:
case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
i : J✝
t : Set ↑(K.obj i)
ht : IsOpen t
⊢ ∃ i_1, ULift.down ⁻¹' ⇑(ConcreteCategory.hom (c.π.app i)) ⁻¹' t ∈ {s | IsOpen s}
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝² : CommRing B
x✝¹ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
a : (i : I) → A i →ₐ[R] B ⧸ Ideal.span {1 - e i}
ha : ∀ (i : I) (x : A i), (Ideal.Quotient.mk (J' i)) ((a i) x) = (ι i) (g (Pi.single i x))
x✝ : (i : I) → A i
i : I
x : A i
y : B
hy : (Ideal.Quotient.mk (Ideal.span {1 - e i})) y = (a i) x
hy' : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i) = (a i) x
j : I
this : (a j) (Pi.single i x j) = (Ideal.Quotient.mk (Ideal.span {1 - e j})) (y * e i)
⊢ iso (↑↑iso.symm ((AlgHom.pi fun i ↦ (a i).comp (Pi.evalAlgHom R A i)) (Pi.single i x))) j = iso (y * e i) j

Tactic:
simpa using! this

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this✝¹ : Module.Finite K A
this✝ : IsArtinianRing A
this : IsReduced A
⊢ Algebra.IsSeparable K (A ⧸ p)

Tactic:
let := Ideal.Quotient.field p

Goal state after:
K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this✝² : Module.Finite K A
this✝¹ : IsArtinianRing A
this✝ : IsReduced A
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ Algebra.IsSeparable K (A ⧸ p)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
⊢ FormallyEtale K A ↔ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)

Tactic:
by
  classical
  constructor
  · intro H
    have := FormallyUnramified.finite_of_free K A
    have := FormallyUnramified.isReduced_of_field K A
    have : IsArtinianRing A := isArtinian_of_tower K inferInstance
    let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
    rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H
    exact ⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
  · intro ⟨I, _, Ai, _, _, e, _⟩
    rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
    exact fun I ↦ of_isSeparable K (Ai I)

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x✝ • (x • 1) ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)

Tactic:
smul_eq_mul,

Goal state after:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ x✝ • (x * 1) ⊗ₜ[R] (D R A) y✝ = x ⊗ₜ[R] (x✝ • (D R A) y✝)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ (tensorKaehlerEquiv R S A B) ((Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A) a) =
    (Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) • (D S B) ((algebraMap A B) a)

Tactic:
trans s • a' • D S B (algebraMap A B a)

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ (tensorKaehlerEquiv R S A B) ((Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) ⊗ₜ[A] (D R A) a) =
    s • a' • (D S B) ((algebraMap A B) a)

R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ s • a' • (D S B) ((algebraMap A B) a) = (Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) • (D S B) ((algebraMap A B) a)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (D S (S ⊗[R] A)) ((s • 1) ⊗ₜ[R] a)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (S ⊗[R] A)) (s ⊗ₜ[R] a) = (D S (S ⊗[R] A)) ((s * 1) ⊗ₜ[R] a)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : AdicCompletion I R
x✝ : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

Tactic:
smul_mk I hmn

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : AdicCompletion I R
x✝ : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r m • Submodule.Quotient.mk (↑x m) = ↑r m • Submodule.Quotient.mk (↑x m)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(AlgebraTensorModule.map LinearMap.id f)

Tactic:
rw [tensor_map_id_left_eq_map I f]

Goal state after:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M))
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (P.ofAlgEquiv e).jacobian = e P.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det, jacobian_eq_jacobiMatrix_det]

Goal state after:
case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (P.ofAlgEquiv e).Ring T) (P.ofAlgEquiv e).jacobiMatrix.det = e ((algebraMap P.Ring S) P.jacobiMatrix.det)
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀) = AlgHom.id R (R ⊗[R₀] ModelOfHasCoeffs R₀)

Tactic:
ext x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  simp

Goal state after:
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsStandardSmooth R S
⊢ Subsingleton (H1Cotangent R S)

Tactic:
by
  obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
  exact P.equivH1Cotangent.symm.toEquiv.subsingleton

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ ((localizationAway T g).comp P).ker =
    Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
have : (localizationAway T g).ker = Ideal.map ((localizationAway T g).ofComp P).toAlgHom
      (Ideal.span {MvPolynomial.rename Sum.inr f * MvPolynomial.X (Sum.inl ()) - 1}) := by
    rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway,
      Hom.toAlgHom_X, toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ ((localizationAway T g).comp P).ker =
    Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0

Tactic:
rw [addU, hQz, mul_zero <| P z, div_zero]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
have hJ : J ≤ P.ker := by simp [J, Ideal.span_le, Set.range_subset_iff]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Submodule.map Extension.Cotangent.mk ⊤ ≤
    Submodule.restrictScalars P.Ring (Submodule.span S (Set.range fun x ↦ Extension.Cotangent.mk (v x)))

Tactic:
refine le_trans le_top (top_le_iff.mpr ?_)

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Submodule.restrictScalars P.Ring (Submodule.span S (Set.range fun x ↦ Extension.Cotangent.mk (v x))) = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ f.Etale ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f

Tactic:
← this,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : @RingHom.Etale = @RingHom.IsStandardSmoothOfRelativeDimension 0
⊢ f.Etale ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
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
    apply P.of_postcomp (W' := Q) g inr (Q.of_isPushout h.flip hf)
    rw [← h.1.1]
    exact RespectsLeft.precomp _ hf _ hinl

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

Goal state before:
pp: case inr
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (pullback.fst (Spec.map φ) g)
this : ∀ {Y : Scheme} (g : Y ⟶ Spec R), P (pullback.fst (Spec.map φ) g) → (∃ S, Y = Spec S) → P g
hY : ¬∃ S, Y = Spec S
⊢ P g

pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : Scheme
g : Y ⟶ Spec R
hf : P (pullback.fst (Spec.map φ) g)
hY : ∃ S, Y = Spec S
⊢ P g

Tactic:
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) Y.affineCover]
    intro i
    have heq : pullback.fst (Spec.map φ) (Y.affineCover.f i ≫ g) =
        pullback.map _ _ _ _ (𝟙 _) (Y.affineCover.f i) (𝟙 _) (by simp) (by simp) ≫
          pullback.fst (Spec.map φ) g := (pullback.lift_fst _ _ _).symm
    exact this _ (heq ▸ AlgebraicGeometry.IsZariskiLocalAtSource.comp hf _) ⟨_, rfl⟩

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'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
hQQ' : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : Scheme
g : Y ⟶ Spec R
hf : P (pullback.fst (Spec.map φ) g)
hY : ∃ S, Y = Spec S
⊢ P g
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ ∀ {R S : CommRingCat} {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
· rw [inf_comm]
    gcongr
    exact IsLocalIso.le_of_isZariskiLocalAtSource @Flat

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦
    RingHom.FaithfullyFlat
⊢ ∀ {R S : CommRingCat} {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : ⇑f '' ↑V = Set.univ
⊢ Surjective (V.ι ≫ f)

pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : ⇑f '' ↑V = Set.univ
⊢ P (pullback.fst V.ι (pullback.fst f g))

Tactic:
· exact ⟨fun x ↦ have ⟨y, hyV, e⟩ := e.ge (Set.mem_univ x); ⟨⟨y, hyV⟩, e⟩⟩

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst✝ : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : ⇑f '' ↑V = Set.univ
⊢ P (pullback.fst V.ι (pullback.fst f g))