mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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ι)
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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)
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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))
Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange

Goal state before:
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 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))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
⊢ X.irreducibleComponentOpen Z = ⊤

Tactic:
rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z = Set.univ
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
⊢ X.irreducibleComponentOpen Z = ⊤
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := AlgebraicClosure K
⊢ Smooth f

Tactic:
let g : Spec (.of Ω) ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom <| algebraMap K Ω)

Goal state after:
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := AlgebraicClosure K
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom (algebraMap K Ω))
⊢ Smooth f
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: case hg
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g

pp: case hsnd
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ Smooth (Limits.pullback.snd f g)

Tactic:
·

Goal state after:
case hg
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) g
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: case hsnd
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ Smooth (Limits.pullback.snd f g)

Tactic:
·

Goal state after:
case hsnd
K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
Ω : Type u := ⋯
g : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of K) := ⋯
⊢ Smooth (Limits.pullback.snd f g)
Module: Mathlib.AlgebraicGeometry.Group.Smooth

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝² : LocallyOfFiniteType f
inst✝¹ : GrpObj (Over.mk f)
inst✝ : GeometricallyReduced f
⊢ Smooth f

Tactic:
by
  let Ω : Type u := AlgebraicClosure K
  let g : Spec (.of Ω) ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom <| algebraMap K Ω)
  apply MorphismProperty.of_pullback_snd_of_descendsAlong
    (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (g := g)
  · exact ⟨⟨inferInstance, inferInstance⟩, inferInstance⟩
  · let : GrpObj (Over.mk (Limits.pullback.snd f g)) := Over.grpObjMkPullbackSnd
    exact smooth_of_grpObj_of_isAlgClosed _

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.left)))

pp: case right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.right)))

Tactic:
·

Goal state after:
case left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.left)))
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.right)))

Tactic:
·

Goal state after:
case right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.right)))
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case id
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).left

pp: case init.left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).left

pp: case init.right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).left

Tactic:
·

Goal state after:
case id
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
i : WalkingSpan
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.id i)).left
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case init.left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).left

pp: case init.right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).left

Tactic:
·

Goal state after:
case init.left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left)).left
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case init.right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).left

Tactic:
·

Goal state after:
case init.right
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ IsOpenImmersion ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right)).left
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).obj x✝ = F.obj x✝

pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId

pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
·

Goal state after:
case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ (F.comp (id C)).obj x✝ = F.obj x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

Tactic:
·

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

Tactic:
·

Goal state after:
case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId

Tactic:
·

Goal state after:
case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (F.comp (id C)).mapId ≍ F.mapId
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
·

Goal state after:
case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ (F.comp (id C)).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).obj x✝ = F.obj x✝

pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

pp: case map₂
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((id B).comp F).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝¹.toQuiver (fun a b ↦ (homCategory a b).toQuiver) C inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

pp: case mapId
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ ((id B).comp F).mapId ≍ F.mapId

pp: case mapComp
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @LaxFunctor.mapComp B inst✝¹ C inst✝ ((id B).comp F).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝¹ C inst✝ F.toLaxFunctor

Tactic:
·

Goal state after:
case obj
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
x✝ : B
⊢ ((id B).comp F).obj x✝ = F.obj x✝
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor

Tactic:
·

Goal state after:
case map
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver ((id B).comp F).toPrefunctor ≍
    @Prefunctor.map B inst✝¹.toQuiver C inst✝.toQuiver F.toPrefunctor