awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat)
fc gc : Y.presheaf ⟶ obj (pushforward C f) X.presheaf
h' :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Eq (α :=
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base
                  (InducedCategory.Hom.hom
                    { hom := { base := f, c := fc : X.Hom Y.toPresheafedSpace } :
                      InducedCategory.Hom (D := PresheafedSpace.{v, u, v} C) (F := toPresheafedSpace) X Y })) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x) ⟶
        X.presheaf.stalk x)
      (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) x)
      (CategoryStruct.comp (Y :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom { hom := { base := f, c := gc } })) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x))
        (Iso.hom (Y.presheaf.stalkCongr ⋯))
        (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := gc } }) x))
⊢ Eq.{v + 1} (α := X ⟶ Y) { hom := { base := f, c := fc } } { hom := { base := f, c := gc } }
have e_hom : fc = gc
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat)
fc gc : Y.presheaf ⟶ obj (pushforward C f) X.presheaf
h' :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Eq (α :=
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base
                  (InducedCategory.Hom.hom
                    { hom := { base := f, c := fc : X.Hom Y.toPresheafedSpace } :
                      InducedCategory.Hom (D := PresheafedSpace.{v, u, v} C) (F := toPresheafedSpace) X Y })) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x) ⟶
        X.presheaf.stalk x)
      (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) x)
      (CategoryStruct.comp (Y :=
        Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom { hom := { base := f, c := gc } })) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x))
        (Iso.hom (Y.presheaf.stalkCongr ⋯))
        (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := gc } }) x))
⊢ fc = gc
have e_hom : ∀ (U : Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) (s : CC (Y.presheaf.obj (op U))),
  Eq (α := CC ((obj (pushforward C f) X.presheaf).obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (fc.app (op U)) :
          (a : CC (Y.presheaf.obj (op U))) → CC (((pushforward C f).obj X.presheaf).obj (op U)))
        s :
      CC ((obj (pushforward C f) X.presheaf).obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (gc.app (op U)) :
          (a : CC (Y.presheaf.obj (op U))) → CC (((pushforward C f).obj X.presheaf).obj (op U)))
        s :
      CC ((obj (pushforward C f) X.presheaf).obj (op U)))
Tactic: ext U s
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Injective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Epi (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ Mono f
have right_cancellation : ∀ {Z : SheafedSpace.{u, v, v} C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Injective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Epi (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
⊢ ∀ (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
have right_cancellation : ∀ (g : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
  (gc : X.presheaf ⟶ obj (pushforward C g) Z.presheaf) (h : Z ⟶ X),
  { hom := { base := g, c := gc } } ≫ f = h ≫ f → { hom := { base := g, c := gc } } = h
Tactic: ⟨g, gc⟩
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Injective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Epi (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)
gc : X.presheaf ⟶ obj (pushforward C g) Z.presheaf
⊢ ∀ (h : Z ⟶ X), { hom := { base := g, c := gc } } ≫ f = h ≫ f → { hom := { base := g, c := gc } } = h
have right_cancellation : ∀ (h : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat))
  (hc : X.presheaf ⟶ obj (pushforward C h) Z.presheaf),
  Eq (α := Z ⟶ Y) ({ hom := { base := g, c := gc } } ≫ f) ({ hom := { base := h, c := hc } } ≫ f) →
    Eq.{v + 1} (α := Z ⟶ X) { hom := { base := g, c := gc } } { hom := { base := h, c := hc } }
Tactic: ⟨h, hc⟩
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Injective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Epi (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)
gc : X.presheaf ⟶ obj (pushforward C g) Z.presheaf
h : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)
hc : X.presheaf ⟶ obj (pushforward C h) Z.presheaf
e : Eq (α := Z ⟶ Y) ({ hom := { base := g, c := gc } } ≫ f) ({ hom := { base := h, c := hc } } ≫ f)
⊢ Eq.{v + 1} (α := Z ⟶ X) { hom := { base := g, c := gc } } { hom := { base := h, c := hc } }
have right_cancellation : ∀ (hc : X.presheaf ⟶ obj (pushforward C g) Z.presheaf)
  (e : Eq (α := Z ⟶ Y) ({ hom := { base := g, c := gc } } ≫ f) ({ hom := { base := g, c := hc } } ≫ f)),
  Eq.{v + 1} (α := Z ⟶ X) { hom := { base := g, c := gc } } { hom := { base := g, c := hc } }
Tactic: obtain rfl : g = h := ConcreteCategory.hom_ext _ _ fun x ↦ h₁ congr(($e).hom.base x)
Cleared hypotheses: h, hc, e
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ Epi f
have left_cancellation : ∀ {Z : SheafedSpace.{u, v, v} C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
⊢ ∀ (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
have left_cancellation : ∀ (g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat))
  (gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf) (h : Y ⟶ Z),
  f ≫ { hom := { base := g, c := gc } } = f ≫ h → { hom := { base := g, c := gc } } = h
Tactic: ⟨g, gc⟩
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf
⊢ ∀ (h : Y ⟶ Z), f ≫ { hom := { base := g, c := gc } } = f ≫ h → { hom := { base := g, c := gc } } = h
have left_cancellation : ∀ (h : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat))
  (hc : Z.presheaf ⟶ obj (pushforward C h) Y.presheaf),
  Eq (α := X ⟶ Z) (f ≫ { hom := { base := g, c := gc } }) (f ≫ { hom := { base := h, c := hc } }) →
    Eq.{v + 1} (α := Y ⟶ Z) { hom := { base := g, c := gc } } { hom := { base := h, c := hc } }
Tactic: ⟨h, hc⟩
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.SheafedSpace (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf
h : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
hc : Z.presheaf ⟶ obj (pushforward C h) Y.presheaf
e : Eq (α := X ⟶ Z) (f ≫ { hom := { base := g, c := gc } }) (f ≫ { hom := { base := h, c := hc } })
⊢ Eq.{v + 1} (α := Y ⟶ Z) { hom := { base := g, c := gc } } { hom := { base := h, c := hc } }
have e₁ : Eq (α := X.toPresheafedSpace ⟶ Z.toPresheafedSpace) (InducedCategory.Hom.hom (f ≫ { hom := { base := g, c := gc } }))
  (InducedCategory.Hom.hom (f ≫ { hom := { base := h, c := hc } }))
Tactic: apply_fun InducedCategory.Hom.hom at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
m : G
x : ι ↪ α
⊢ { toFun := f.toFun ∘ (m • x).toFun, inj' := ⋯ : ι ↪ β } = σ m • { toFun := f.toFun ∘ x.toFun, inj' := ⋯ : ι ↪ β }
have h : ∀ (x_1 : ι),
  Eq.{u_4 + 1} (α := β) (({ toFun := f.toFun ∘ (m • x).toFun, inj' := sorry : ι ↪ β } : (a : ι) → β) x_1 : β)
    ((σ m • { toFun := f.toFun ∘ x.toFun, inj' := sorry : ι ↪ β } : (a : ι) → β) x_1 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : ι ↪ α
hxy :
  Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
    ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β)
⊢ a₁ = a₂
have h : ∀ (x : ι), Eq.{u_2 + 1} (α := α) ((a₁ : (a : ι) → α) x : α) ((a₂ : (a : ι) → α) x : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : ι ↪ α
hxy :
  Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
    ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β)
x : ι
⊢ Eq.{u_2 + 1} (α := α) ((a₁ : (a : ι) → α) x : α) ((a₂ : (a : ι) → α) x : α)
have h : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) ((a₁ : (a : ι) → α) x : α) : β)
  ((f : (a : α) → β) ((a₂ : (a : ι) → α) x : α) : β)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Bijective (α := ι ↪ α) (β := ι ↪ β) (⇑(Injective.mulActionHom_embedding ι ⋯) : (a : ι ↪ α) → ι ↪ β)
have refine : Surjective (α := ι ↪ α) (β := ι ↪ β) (⇑(Injective.mulActionHom_embedding ι sorry) : (a : ι ↪ α) → ι ↪ β)
Tactic: refine ⟨hf.injective.mulActionHom_embedding_isInjective, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
⊢ ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) a = y
have obtain : ∀ (g : β → α),
  LeftInverse g (⇑f : (a : α) → β) →
    ∀ (hfg : RightInverse g (⇑f : (a : α) → β)),
      ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι sorry : (a : ι ↪ α) → ι ↪ β) a = y
Tactic: obtain ⟨g, _, hfg⟩ := Function.bijective_iff_has_inverse.mp hf
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultipleTransitivity (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
⊢ ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) a = y
have h : (Injective.mulActionHom_embedding ι sorry : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := sorry } = y
Tactic: use ⟨g ∘ y, hfg.injective.comp (EmbeddingLike.injective y)⟩