mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U)

Tactic:
apply (D.t j i ≫ D.f i j).hom.continuous_toFun.isOpen_preimage

Goal state after:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen ↑U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) =
    ↑((ConcreteCategory.hom (h.t j j)) ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
h.t_id

Goal state after:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this : ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) = ↑(id ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ (ConcreteCategory.hom (h.t i i)) x✝ =
    (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝

Tactic:
h.t_id

Goal state after:
D : GlueData
h : MkCore
i : h.J
x✝ : ↑((Opens.toTopCat (h.U i)).obj (h.V i i))
⊢ id x✝ = (ConcreteCategory.hom (𝟙 ((Opens.toTopCat (h.U (i, i).1)).obj (h.V (i, i).1 (i, i).2)))) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
    (ConcreteCategory.hom (h.t i k)) ⟨x, hx'⟩

Tactic:
refine Subtype.ext ?_

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
    ↑((ConcreteCategory.hom (h.t i k)) ⟨x, hx'⟩)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left, ← Over.comp_left_assoc,
    Iso.hom_inv_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (𝟙 ((pullback f).obj (R ⊗ S))) ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
⊢ x✝ ∈ ⋃ i, ↑(U i) → x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
rintro ⟨_, ⟨i, rfl⟩, hx⟩

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x✝ : ↑(of α)
i : J
hx : x✝ ∈ (fun i ↦ ↑(U i)) i
⊢ x✝ ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)

Tactic:
delta gluedCoverT'

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
delta gluedCoverT'

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))).hom ≫
        (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
              (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ ∃ (eq :
    (Opens.map (D.t k i).base).op.obj (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
      op
        ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
          (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))),
    invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
        (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (D.V (k, i)).presheaf.map (eqToHom eq) =
      (D.t' k i j).c.app (op U) ≫
        invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))

Tactic:
fconstructor

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (Opens.map (D.t k i).base).op.obj (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) =
    op
      ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).obj
        (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U))))))

case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ invApp (pullback.snd (D.f i j) (D.f i k)) U ≫
      (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
        (D.V (k, i)).presheaf.map (eqToHom ?w) =
    (D.t' k i j).c.app (op U) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) (unop (op ((Opens.map (D.t' k i j).base).1 (unop (op U)))))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case inst
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι := ⋯
⊢ IsOpenImmersion (α ≫ pullback.fst (V F i j).ι (V F i k).ι)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_π_app, α]

Goal state after:
case inst
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
⊢ IsOpenImmersion ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
⊢ (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom) ≫ (F.obj i).homOfLE h₁ =
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ≫ (F.obj i).homOfLE h₂

Tactic:
simp [← cancel_mono (Scheme.Opens.ι _), ← Functor.map_comp,
        Subsingleton.elim (hli ≫ k₁.2.1) (hlj ≫ k₂.2.1)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ pullback (p1 𝒰 f g) (𝒰.f i) ≅ pullback (𝒰.f i ≫ f) g

Tactic:
fconstructor

Goal state after:
case hom
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ pullback (p1 𝒰 f g) (𝒰.f i) ⟶ pullback (𝒰.f i ≫ f) g

case inv
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ pullback (𝒰.f i ≫ f) g ⟶ pullback (p1 𝒰 f g) (𝒰.f i)

case hom_inv_id
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ autoParam (?hom ≫ ?inv = 𝟙 (pullback (p1 𝒰 f g) (𝒰.f i))) Iso.hom_inv_id._autoParam

case inv_hom_id
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ autoParam (?inv ≫ ?hom = 𝟙 (pullback (𝒰.f i ≫ f) g)) Iso.inv_hom_id._autoParam
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ∃ (eq :
    op U =
      op
        ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj
          (⋯.functor.obj U))),
    D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).presheaf.map (eqToHom eq)

Tactic:
fconstructor

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ op U =
    op ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))

case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).presheaf.map (eqToHom ?w)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P g'

Tactic:
← P.cancel_left_of_respectsIso h.isoPullback.inv,

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (h.isoPullback.inv ≫ g')
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P f'

Tactic:
← P.cancel_left_of_respectsIso h.isoPullback.inv,

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (h.isoPullback.inv ≫ f')
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P.diagonal (U.ι ≫ f)

pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f

Tactic:
· change P _
    apply P.of_postcomp (W' := @IsOpenImmersion) (pullback.diagonal (U.ι ≫ f)) (g f U) inferInstance
    rw [← pullback.comp_diagonal]
    apply IsZariskiLocalAtSource.comp
    exact hf

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)
i : ι
⊢ P ((U i).carrier.restrictPreimage ⇑f)

Tactic:
← morphismRestrict_base

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ∣_ U i)
i : ι
⊢ P ⇑(f ∣_ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
⊢ IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑W).carrier ∩ ↑↑V)

Tactic:
hW

Goal state after:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact ((S ⊔ ↑W).carrier ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P (↑x ⊔ ⨆ x ∈ s, ↑x)

Tactic:
sup_comm

Goal state after:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact ↑(⨆ i ∈ s✝, ↑i)
x : ↑X.affineOpens
s : Set ↑X.affineOpens
x✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, ↑i)
⊢ P ((⨆ x ∈ s, ↑x) ⊔ ↑x)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ Order.height { asIdeal := I, isPrime := inst✝ } = 0 ↔ I ∈ minimalPrimes R

Tactic:
Order.height_eq_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ IsMin { asIdeal := I, isPrime := inst✝ } ↔ I ∈ minimalPrimes R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
e : R ≃+* S
p : Ideal S
inst✝ : p.IsPrime
⊢ (comap e p).height = p.height

Tactic:
rw [height_eq_primeHeight, height_eq_primeHeight, primeHeight, primeHeight,
    ← Order.height_orderIso (PrimeSpectrum.comapEquiv e.symm) ⟨p, ‹_›⟩]
  have := p.map_comap_of_equiv e.symm
  congr

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
this✝ : P.IsPrime
this : IsLocalization.AtPrime (Localization.AtPrime P) (comap (algebraMap R S) P)
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
P,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
this✝ : P.IsPrime
this :
  IsLocalization.AtPrime (Localization.AtPrime (Ideal.map (algebraMap R S) p))
    (comap (algebraMap R S) (Ideal.map (algebraMap R S) p))
⊢ (Ideal.map (algebraMap R S) p).height = p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

Tactic:
obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), IsOpen ↑s

Tactic:
rintro ⟨_, i, rfl⟩

Goal state after:
case hS
X : Scheme
i : X.affineCover.I₀
⊢ IsOpen ↑⟨(fun x ↦ Set.range ⇑(X.affineCover.f x)) i, ⋯⟩
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inst
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), QuasiSober ↑↑s

Tactic:
rintro ⟨_, i, rfl⟩

Goal state after:
case inst
X : Scheme
i : X.affineCover.I₀
⊢ QuasiSober ↑↑⟨(fun x ↦ Set.range ⇑(X.affineCover.f x)) i, ⋯⟩