mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_3.refine_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
⊢ (Over.Hom.left γ) xe = xe

Tactic:
·

Goal state after:
case refine_3.refine_2
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
⊢ (Over.Hom.left γ) xe = xe
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_3
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
⊢ Over.Hom.left (GrpObj.commutator G) ≫ G.hom = Over.Hom.left (toUnit (G ⊗ G) ≫ η) ≫ G.hom

Tactic:
·

Goal state after:
case refine_3
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H✝¹ :
  ⇑(Over.Hom.left γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H✝ : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
⊢ Over.Hom.left (GrpObj.commutator G) ≫ G.hom = Over.Hom.left (toUnit (G ⊗ G) ≫ η) ≫ G.hom
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ IsOpen {x | QuasiFiniteAt f x}

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : IsAffineHom f
⊢ IsOpen {x | QuasiFiniteAt f x}

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ IsOpen {x | QuasiFiniteAt f x}
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ Ideal.map (algebraMap R S) I ≤ f.range

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ f.range ≤ Ideal.map (algebraMap R S) I

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ Ideal.map (algebraMap R S) I ≤ f.range
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ f.range ≤ Ideal.map (algebraMap R S) I

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
⊢ f.range ≤ Ideal.map (algebraMap R S) I
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x} ⊆ {x | QuasiFiniteAt f x}

pp: case inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ x ∈ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x}

Tactic:
·

Goal state after:
case inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x} ⊆ {x | QuasiFiniteAt f x}
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ x ∈ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x}

Tactic:
·

Goal state after:
case inr.refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
U : Y.Opens
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
inst : IsAffineHom (resLE f U V hVU)
⊢ x ∈ Subtype.val '' {x | QuasiFiniteAt (resLE f U V hVU) x}
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ y ∈ V

pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)

Tactic:
·

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ y ∈ V
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)

Tactic:
·

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
a✝ : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x y : T ⊗[R] ↥(Submodule.restrictScalars R I)
a : T ⊗[R] I.Cotangent
ha :
  (tensorCotangentHom R T I) a =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩
b : T ⊗[R] I.Cotangent
hb :
  (tensorCotangentHom R T I) b =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩
⊢ (tensorCotangentHom R T I) (a + b) =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (x + y), ⋯⟩

Tactic:
by simp only [map_add, ha, hb]; rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := ⋯
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := ⋯
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑g

Tactic:
·

Goal state after:
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
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := ⋯
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := ⋯
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 := ⋯
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑g
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case left
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R]

pp: case right
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Subsingleton (H1Cotangent R S)

Tactic:
·

Goal state after:
case left
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Module.Projective S Ω[S⁄R]
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case right
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Subsingleton (H1Cotangent R S)

Tactic:
·

Goal state after:
case right
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Subsingleton (H1Cotangent R S)
Module: Mathlib.RingTheory.Etale.Descent

Goal state before:
pp: case right
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✝¹ : Module.FaithfullyFlat R T
inst✝ : Smooth T (T ⊗[R] S)
this : FinitePresentation R S
⊢ Subsingleton (H1Cotangent R S)

Tactic:
have : Subsingleton (T ⊗[R] H1Cotangent R S) := (tensorH1CotangentOfFlat R S T).subsingleton
    exact Module.FaithfullyFlat.lTensor_reflects_triviality R T (H1Cotangent R S)

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

Goal state before:
pp: case hf₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑0

pp: case hf₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor T (↑R h1Cotangentι))

pp: case hf₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(LinearMap.lTensor T (↑R h1Cotangentι)) ⇑(LinearMap.lTensor T (↑R P.cotangentComplex))

pp: case hg₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑0

pp: case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(↑R h1Cotangentι)

pp: case hg₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.baseChange.cotangentComplex)

pp: case hi₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Surjective ⇑0

pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

pp: case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
·

Goal state after:
case hf₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑0
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hf₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor T (↑R h1Cotangentι))

pp: case hf₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(LinearMap.lTensor T (↑R h1Cotangentι)) ⇑(LinearMap.lTensor T (↑R P.cotangentComplex))

pp: case hg₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑0

pp: case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(↑R h1Cotangentι)

pp: case hg₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.baseChange.cotangentComplex)

pp: case hi₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Surjective ⇑0

pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

pp: case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
·

Goal state after:
case hf₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor T (↑R h1Cotangentι))
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
pp: case hf₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(LinearMap.lTensor T (↑R h1Cotangentι)) ⇑(LinearMap.lTensor T (↑R P.cotangentComplex))

pp: case hg₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑0

pp: case hg₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑0 ⇑(↑R h1Cotangentι)

pp: case hg₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(↑R h1Cotangentι) ⇑(↑R P.baseChange.cotangentComplex)

pp: case hi₁
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Surjective ⇑0

pp: case hi₂
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑0

pp: case hi₄
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Bijective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T))

pp: case hi₅
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Injective ⇑↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T))

Tactic:
·

Goal state after:
case hf₃
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Extension R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Module.Flat R T
⊢ Function.Exact ⇑(LinearMap.lTensor T (↑R h1Cotangentι)) ⇑(LinearMap.lTensor T (↑R P.cotangentComplex))