awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
refine_2 : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))
refine_2₁ :
  (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
            (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
          y =
        x)
    (this.lift x ⋯)
refine_2₂ :
  ∀ (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
                (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
                  (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
              y =
            x)
        y →
      y = this.lift x ⋯
⊢ ∃! y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
          (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
            (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
        y =
      x

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
refine_2 :
  ∀ (a b : ↥(Spec S))
    (hfab :
      Eq (α := ↥(Opposite.unop (Opposite.op (Spec R)))) ((Spec.map f) a : ↥(Opposite.unop (Opposite.op (Spec R))))
        ((Spec.map f) b : ↥(Opposite.unop (Opposite.op (Spec R))))),
    Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) a : T) ((x : (a : ↥(Spec S)) → T) b : T)
⊢ (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))

Tactic:
refine Topology.IsQuotientMap.lift this x fun a b hfab ↦ ?_

Premises used: Topology.IsQuotientMap.lift
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
a b : ↥(Spec S)
hfab :
  Eq (α := ↥(Opposite.unop (Opposite.op (Spec R)))) ((Spec.map f) a : ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) b : ↥(Opposite.unop (Opposite.op (Spec R))))
refine_2 :
  ∀ (c : ↥(pullback (Spec.map f) (Spec.map f)))
    (hfab :
      Eq (α := ↥(Opposite.unop (Opposite.op (Spec R))))
        ((Spec.map f) ((pullback.fst (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
        ((Spec.map f) ((pullback.snd (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))),
    Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) ((pullback.fst (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
      ((x : (a : ↥(Spec S)) → T) ((pullback.snd (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
⊢ Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) a : T) ((x : (a : ↥(Spec S)) → T) b : T)

Tactic:
obtain ⟨c, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback a b hfab

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
c : ↥(pullback (Spec.map f) (Spec.map f))
hfab :
  Eq (α := ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) ((pullback.fst (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) ((pullback.snd (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
⊢ Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) ((pullback.fst (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
    ((x : (a : ↥(Spec S)) → T) ((pullback.snd (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)

Tactic:
congr($(h (pullback.fst (Spec.map f) (Spec.map f))
        (pullback.snd _ _) pullback.condition).1 c)

Premises used: congrArg, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Spec.map, id, CategoryTheory.Limits.pullback.fst, ContinuousMap.toFun, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
c : ↥(pullback (Spec.map f) (Spec.map f))
hfab :
  Eq (α := ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) ((pullback.fst (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
    ((Spec.map f) ((pullback.snd (Spec.map f) (Spec.map f)) c) : ↥(Opposite.unop (Opposite.op (Spec R))))
⊢ Eq.{v + 1} (α := T) ((x : (a : ↥(Spec S)) → T) ((pullback.fst (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)
    ((x : (a : ↥(Spec S)) → T) ((pullback.snd (Spec.map f) (Spec.map f)) c : ↥(Spec S)) : T)

Tactic:
exact congr($(h (pullback.fst (Spec.map f) (Spec.map f))
        (pullback.snd _ _) pullback.condition).1 c)
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
⊢ (fun (y : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
            (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
              (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
          y =
        x)
    (this.lift x ⋯)

Tactic:
apply Topology.IsQuotientMap.lift_comp

Premises used: Topology.IsQuotientMap.lift_comp
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
T : Type v
inst : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map f)
x : ContinuousMap.{u_1, v} (↥(Spec S)) T
h :
  ∀ {Z : Scheme.{u_1}} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      Eq (α := (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₁.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map p₂.op) :
              (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S)))) →
                (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
            x :
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op Z)))
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((continuousMapPresheaf T).map (Spec.map f).op) :
        (a : (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))) →
          (fun (X : Type (max u_1 v)) ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec S))))
      y =
    x
refine_2 :
  ContinuousMap.comp y
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        TopCat.carrier) (Spec.map f).base) =
    (this.lift x ⋯).comp
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        TopCat.carrier) (Spec.map f).base)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ContinuousMap.comp y
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        TopCat.carrier) (Spec.map f).base) =
    x
⊢ y = this.lift x ⋯

Tactic:
rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]

Premises used: AlgebraicGeometry.Spec.map, ContinuousMap.cancel_right, Topology.IsQuotientMap.lift_comp, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
a :
  Eq (α := (a : ConnectedComponents ↥U) → T)
    (⇑((fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
            { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
              ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
          ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
              f.comp
                { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ :
                  C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
            f)) :
      (a : ConnectedComponents ↥U) → T)
    (⇑f : (a : ConnectedComponents ↥U) → T)
⊢ (fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
        { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ : ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
      ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
          f.comp
            { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ :
              C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
        f) =
    f

Tactic:
apply ContinuousMap.coe_injective

Premises used: ContinuousMap.coe_injective
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
a :
  Eq (α := (a : ConnectedComponents ↥U) → T)
    (Continuous.connectedComponentsLift (f :=
      Function.comp (β := ConnectedComponents ↥U) (⇑f : (a : ConnectedComponents ↥U) → T) ConnectedComponents.mk) ⋯)
    (⇑f : (a : ConnectedComponents ↥U) → T)
⊢ Eq (α := (a : ConnectedComponents ↥U) → T)
    (⇑((fun (f : (continuousMapPresheaf T).obj (Opposite.op U)) ↦
            { toFun := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
              ContinuousMap.{u, v} (ConnectedComponents ↥U) T })
          ((fun (f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T) ↦
              f.comp
                { toFun := ConnectedComponents.mk, continuous_toFun := ⋯ :
                  C(↥(Opposite.unop (Opposite.op U)), ConnectedComponents ↥U) })
            f)) :
      (a : ConnectedComponents ↥U) → T)
    (⇑f : (a : ConnectedComponents ↥U) → T)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
⊢ Eq (α := ↥U → T)
    (Function.comp (β := ConnectedComponents ↥U) (⇑f : (a : ConnectedComponents ↥U) → T) ConnectedComponents.mk)
    (Function.comp (β := ConnectedComponents ↥U) (⇑f : (a : ConnectedComponents ↥U) → T) ConnectedComponents.mk)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
S : Scheme
T : Type v
inst : TopologicalSpace T
inst_1 : TotallyDisconnectedSpace T
U : Scheme
f : ContinuousMap.{u, v} (ConnectedComponents ↥U) T
⊢ Eq (α := (a : ConnectedComponents ↥U) → T)
    (Continuous.connectedComponentsLift (f :=
      Function.comp (β := ConnectedComponents ↥U) (⇑f : (a : ConnectedComponents ↥U) → T) ConnectedComponents.mk) ⋯)
    (⇑f : (a : ConnectedComponents ↥U) → T)

Tactic:
exact (Continuous.connectedComponentsLift_unique _ _ (by simp)).symm

Premises used: Continuous.connectedComponentsLift_unique, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
A : Type v
inst : TopologicalSpace A
inst_1 : AddCommGroup A
inst_2 : IsTopologicalAddGroup A
apply :
  Presheaf.IsSheaf Scheme.fpqcTopology
    (continuousMapPresheafAb A ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 v)) →+ (↑x2 : Type (max u_1 v))) (CC :=
        AddCommGrpCat.carrier))
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheafAb A)

Tactic:
apply Presheaf.isSheaf_of_isSheaf_comp _ _ (forget Ab)

Premises used: CategoryTheory.Presheaf.isSheaf_of_isSheaf_comp, Ab, CategoryTheory.forget
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
A : Type v
inst : TopologicalSpace A
inst_1 : AddCommGroup A
inst_2 : IsTopologicalAddGroup A
⊢ Presheaf.IsSheaf Scheme.fpqcTopology
    (continuousMapPresheafAb A ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 v)) →+ (↑x2 : Type (max u_1 v))) (CC :=
        AddCommGrpCat.carrier))

Tactic:
isSheaf_fpqcTopology_continuousMapPresheaf _

Premises used: ContinuousMap.comp, CategoryTheory.Functor.comp, AlgebraicGeometry.continuousMapPresheaf, AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
Goal:
A : Type v
inst : TopologicalSpace A
inst_1 : AddCommGroup A
inst_2 : IsTopologicalAddGroup A
⊢ Presheaf.IsSheaf Scheme.fpqcTopology
    (continuousMapPresheafAb A ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 v)) →+ (↑x2 : Type (max u_1 v))) (CC :=
        AddCommGrpCat.carrier))

Tactic:
exact isSheaf_fpqcTopology_continuousMapPresheaf _

Premises used: AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
⊢ EssentiallySmall.{u + 1, u, u + 1} X.ProEt

Tactic:
have : EssentiallySmall.{u + 1} X.ProEt := inferInstance
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
this : EssentiallySmall.{u + 1, u, u + 1} X.ProEt
⊢ IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (Sheaf (ProEt.topology X) Ab)

Tactic:
Sheaf.isGrothendieckAbelian_of_essentiallySmall (ProEt.topology X) Ab.{u + 1}

Premises used: AlgebraicGeometry.Scheme.ProEt.topology, CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall, Ab
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
this : EssentiallySmall.{u + 1, u, u + 1} X.ProEt
⊢ IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (Sheaf (ProEt.topology X) Ab)

Tactic:
exact Sheaf.isGrothendieckAbelian_of_essentiallySmall (ProEt.topology X) Ab.{u + 1}
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
ℓ : ℕ
inst : Fact (Nat.Prime ℓ)
inst_1 : IsEmpty.{u + 1} ↥X
⊢ IsZero (X.ellAdicSheaf ℓ)

Tactic:
(Sheaf.isTerminalOfEqTop (ProEt.topology_eq_top_of_isEmpty _) _).isZero

Premises used: CategoryTheory.Limits.IsTerminal.isZero, CategoryTheory.Sheaf.isTerminalOfEqTop, AlgebraicGeometry.Scheme.ProEt.topology_eq_top_of_isEmpty
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
ℓ : ℕ
inst : Fact (Nat.Prime ℓ)
inst_1 : IsEmpty.{u + 1} ↥X
n : ℕ
h : IsZero ((sheafCompose (ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ))
⊢ Subsingleton.{u + 2} (X.EllAdicCohomology ℓ n)

Tactic:
apply Sheaf.subsingleton_H_of_isZero

Premises used: CategoryTheory.Sheaf.subsingleton_H_of_isZero
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
ℓ : ℕ
inst : Fact (Nat.Prime ℓ)
inst_1 : IsEmpty.{u + 1} ↥X
n : ℕ
⊢ IsZero ((sheafCompose (ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ))

Tactic:
Functor.map_isZero _ (isZero_ellAdicSheaf_of_isEmpty _ _)

Premises used: CategoryTheory.Functor.map_isZero, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty
-- Module: Mathlib.AlgebraicGeometry.Sites.ElladicCohomology
Goal:
X : Scheme
ℓ : ℕ
inst : Fact (Nat.Prime ℓ)
inst_1 : IsEmpty.{u + 1} ↥X
n : ℕ
⊢ IsZero ((sheafCompose (ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ))

Tactic:
exact Functor.map_isZero _ (isZero_ellAdicSheaf_of_isEmpty _ _)

Premises used: CategoryTheory.Functor.map_isZero, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
hPQ : IsOpenImmersion ≤ @Etale
⊢ zariskiTopology ≤ etaleTopology

Tactic:
apply grothendieckTopology_monotone

Premises used: AlgebraicGeometry.Scheme.grothendieckTopology_monotone
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ Etale f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Sites.Etale
Goal:
S : Scheme
𝒰 : Cover.{u_1, u} (precoverage @Etale) S
i : 𝒰.I₀
⊢ Etale (𝒰.f i)

Tactic:
𝒰.map_prop i

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop