awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Hom.base (pullback.snd (D.f i j) (D.f i k)) = (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base
⊢ Eq (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t' k i j).base) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
have this₁ : Eq.{v + 1} (α := C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v)))
  ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
    (Hom.base (pullback.snd (D.f i j) (D.f i k))))
  ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
    (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base)
Tactic: replace this := congr_arg (TopCat.Hom.hom ·) this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq.{v + 1} (α := C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v)))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (Hom.base (pullback.snd (D.f i j) (D.f i k))))
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base)
⊢ Eq (α := Set (↑(↑(D.V (k, i)) : TopCat) : Type v))
    (Set.preimage (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat)) (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ''
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
    (Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(pullback (D.f k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t' k i j).base) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
        (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))))
have this₁ : Eq.{v + 1} (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
  ((fun (x : C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v))) ↦ x.toFun)
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (Hom.base (pullback.snd (D.f i j) (D.f i k)))))
  ((fun (x : C((↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v), (↑(↑(D.V (i, k)) : TopCat) : Type v))) ↦ x.toFun)
    ((fun (x : (↑(pullback (D.f i j) (D.f i k)) : TopCat).Hom (↑(D.V (i, k)) : TopCat)) ↦ x.hom)
      (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base))
Tactic: replace this := congr_arg (ContinuousMap.toFun ·) this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
⊢ Function.Injective (α := (↑(↑(D.V (k, i)) : TopCat) : Type v)) (β := (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t k i).base) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
have w : ∀ (x : (↑(↑(D.V (k, i)) : TopCat) : Type v)),
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
Tactic: refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
have w : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        ((D.t k i).base ≫ (D.t i k).base) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t k i).base ≫ (D.t i k).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
have w₁ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (D.t k i ≫ D.t i k).base :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t k i).base ≫ (D.t i k).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t k i ≫ D.t i k).base :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
have w₂ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (Hom.base (𝟙 (D.V (k, i)))) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t k i).base ≫ (D.t i k).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t k i ≫ D.t i k).base :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Hom.base (𝟙 (D.V (k, i)))) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
have w₃ : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
        (𝟙 (↑(D.V (k, i)) : TopCat)) :
      (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
    x =
  x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
x : (↑(↑(D.V (k, i)) : TopCat) : Type v)
w :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          ((D.t k i).base ≫ (D.t i k).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t k i ≫ D.t i k).base :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Hom.base (𝟙 (D.V (k, i)))) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
w₃ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (𝟙 (↑(D.V (k, i)) : TopCat)) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      x =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t i k).base :
        (a : (↑(↑(D.V (i, k)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (D.t k i).base :
            (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
          x :
        (↑(↑(D.V (i, k)) : TopCat) : Type v)) =
    x
have w₄ : x = x
Tactic: rw [← ConcreteCategory.comp_apply, ← comp_base, D.t_inv, id_base, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
this :
  Eq (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (⇑(TopCat.Hom.hom (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
    (Function.comp (β := (↑(↑(D.V (k, i)) : TopCat) : Type v))
      (⇑(TopCat.Hom.hom (D.t k i).base) :
        (a : (↑(↑(D.V (k, i)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
      (Function.comp (β := (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
          (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
        (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
          (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
            (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))))
⊢ Eq (α := Set (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
    ((⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
        (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) ''
      (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.t' k i j).base) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
          (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) ⁻¹'
      (↑U : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))
have w : Eq (α :=
  (x : Set (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
    Set (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
  (Set.image
    (⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) :
      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)))
  (Set.preimage
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.t' k i j).base) :
      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
        (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)))
Tactic: refine congr_fun ?_ _