awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
⊢ P f ↔ ⊤ f
have h : P f → ⊤ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : MorphismProperty (Paths V)
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
X Y : Paths V
f : X ⟶ Y
h : P f → ⊤ f
⊢ P f ↔ ⊤ f
have h₁ : ⊤ f → P f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
V : Type u₁
inst_1 : Quiver.{v₁, u₁} V
F G : Paths V ⥤ C
α_app : (v : V) → F.obj v ⟶ G.obj v
α_nat : ∀ {X Y : V} (f : X ⟶ Y), F.map f.toPath ≫ α_app Y = α_app X ≫ G.map f.toPath
⊢ ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), F.map f ≫ α_app Y = α_app X ≫ G.map f
have apply : MorphismProperty.naturalityProperty α_app = ⊤
Tactic: apply MorphismProperty.of_eq_top
      (P := MorphismProperty.naturalityProperty (F₁ := F) α_app)
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
⊢ W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
have refine_1 : ∀ (h : W.paths (p.comp q)), W.paths p
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
refine_1 : ∀ (h : W.paths (p.comp q)), W.paths p
⊢ W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
have refine_2 : ∀ (h : W.paths (p.comp q)), W.paths q
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
refine_1 : ∀ (h : W.paths (p.comp q)), W.paths p
refine_2 : ∀ (h : W.paths (p.comp q)), W.paths q
⊢ W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
have refine_3 : W.paths p ∧ W.paths q → ∀ (hp : W.paths p) (hq : W.paths q), W.paths (p.comp q)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
b c : C
q' : Path.{v_1, u_1} Y b
f : b ⟶ c
h' : ∀ (h : W.paths (p.comp q')), W.paths p
h : W.paths (p.comp (q'.cons f))
⊢ W.paths p
have h₁ : W.paths ((p.comp q').cons f)
Tactic: rw [Path.comp_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths (p.comp q)
⊢ W.paths p
have refine_1 : ∀ (h : W.paths (p.comp Path.nil)), W.paths p
Tactic: induction q with
    | nil => simpa using h
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact h' h.1
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths (p.comp q)
refine_1 : ∀ (h : W.paths (p.comp Path.nil)), W.paths p
⊢ W.paths p
have refine_1₁ : ∀ {b c : C} (q' : Path.{v_1, u_1} Y b) (f : b ⟶ c) (h' : ∀ (h : W.paths (p.comp q')), W.paths p)
  (h : W.paths (p.comp (q'.cons f))), W.paths p
Tactic: induction q with
    | nil => simpa using h
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact h' h.1
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
b c : C
q' : Path.{v_1, u_1} Y b
f : b ⟶ c
h' : ∀ (h : W.paths (p.comp q')), W.paths q'
h : W.paths (p.comp (q'.cons f))
⊢ W.paths (q'.cons f)
have h₁ : W.paths ((p.comp q').cons f)
Tactic: rw [Path.comp_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths (p.comp q)
⊢ W.paths q
have refine_2 : ∀ (h : W.paths (p.comp Path.nil)), W.paths (X := Y) Path.nil
Tactic: induction q with
    | nil => simp
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact ⟨h' h.1, h.2⟩
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths (p.comp q)
refine_2 : ∀ (h : W.paths (p.comp Path.nil)), W.paths (X := Y) Path.nil
⊢ W.paths q
have refine_2₁ : ∀ {b c : C} (q' : Path.{v_1, u_1} Y b) (f : b ⟶ c) (h' : ∀ (h : W.paths (p.comp q')), W.paths q')
  (h : W.paths (p.comp (q'.cons f))), W.paths (q'.cons f)
Tactic: induction q with
    | nil => simp
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact ⟨h' h.1, h.2⟩
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)
have refine_3 : W.paths p ∧ W.paths (X := Y) Path.nil → ∀ (hq : W.paths (X := Y) Path.nil), W.paths (p.comp Path.nil)
Tactic: induction q with
    | nil => exact hp
    | cons q q' h => exact ⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩
Cleared hypotheses: q, h, hq
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
p : Path.{v_1, u_1} X Y
q : Path.{v_1, u_1} Y Z
h : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
refine_3 : W.paths p ∧ W.paths (X := Y) Path.nil → ∀ (hq : W.paths (X := Y) Path.nil), W.paths (p.comp Path.nil)
⊢ W.paths (p.comp q)
have refine_3₁ : ∀ {b c : C} (q : Path.{v_1, u_1} Y b) (q' : b ⟶ c) (h : W.paths p ∧ W.paths q → ∀ (hq : W.paths q), W.paths (p.comp q)),
  W.paths p ∧ W.paths (q.cons q') → ∀ (hq : W.paths (q.cons q')), W.paths (p.comp (q.cons q'))
Tactic: induction q with
    | nil => exact hp
    | cons q q' h => exact ⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩
Cleared hypotheses: q, h, hq
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsStableUnderComposition
X Y : C
p : Path.{v_1, u_1} X Y
hp : W.paths p
h : W (𝟙 X)
⊢ W (composePath p)
have revert : ∀ (hp : W.paths p), W (composePath p)
Tactic: revert hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsStableUnderComposition
X Y : C
p : Path.{v_1, u_1} X Y
hp : W.paths p
h : 0 < p.length
⊢ W (composePath p)
have revert : ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)
Tactic: revert hp h
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsStableUnderComposition
X Y : C
p : Path.{v_1, u_1} X Y
⊢ ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)
have refine : ∀ {b c : C} (p : Path.{v_1, u_1} X b) (f : b ⟶ c) (hp : ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p))
  (hp' : W.paths (p.cons f)) (hp'' : 0 < (p.cons f).length), W (composePath (p.cons f))
Tactic: refine p.rec (by simp) fun p f hp hp' hp'' ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsStableUnderComposition
X Y : C
p_1 : Path.{v_1, u_1} X Y
b c : C
p : Path.{v_1, u_1} X b
f : b ⟶ c
hp : ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)
hp' : W.paths (p.cons f)
hp'' : 0 < (p.cons f).length
⊢ W (composePath (p.cons f))
have nil : ∀ (f : X ⟶ c)
  (hp :
    ∀ (hp : W.paths (X := X) Path.nil) (h : 0 < Path.length.{u_1, v_1} (V := C) (a := X) Path.nil),
      W (X := X) (composePath Path.nil))
  (hp' : W.paths (Path.cons Path.nil f)) (hp'' : 0 < (Path.cons Path.nil f).length),
  W (composePath (Path.cons Path.nil f))
Tactic: cases p
Cleared hypotheses: b, p, f, hp, hp', hp''
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsStableUnderComposition
X Y : C
p_1 : Path.{v_1, u_1} X Y
b c : C
p : Path.{v_1, u_1} X b
f : b ⟶ c
hp : ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)
hp' : W.paths (p.cons f)
hp'' : 0 < (p.cons f).length
nil :
  ∀ (f : X ⟶ c)
    (hp :
      ∀ (hp : W.paths (X := X) Path.nil) (h : 0 < Path.length.{u_1, v_1} (V := C) (a := X) Path.nil),
        W (X := X) (composePath Path.nil))
    (hp' : W.paths (Path.cons Path.nil f)) (hp'' : 0 < (Path.cons Path.nil f).length),
    W (composePath (Path.cons Path.nil f))
⊢ W (composePath (p.cons f))
have cons : ∀ {b_1 : C} (a : Path.{v_1, u_1} X b_1) (a_1 : b_1 ⟶ b)
  (hp : ∀ (hp : W.paths (a.cons a_1)) (h : 0 < (a.cons a_1).length), W (composePath (a.cons a_1)))
  (hp' : W.paths ((a.cons a_1).cons f)) (hp'' : 0 < ((a.cons a_1).cons f).length), W (composePath ((a.cons a_1).cons f))
Tactic: cases p
Cleared hypotheses: p, hp, hp', hp''
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
⊢ W.multiplicativeClosure = W.paths.strictMap (pathComposition C)
have refine_1 : W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)
Tactic: refine le_antisymm ?_ fun _ _ _ ⟨h⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
refine_1 : W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)
⊢ W.multiplicativeClosure = W.paths.strictMap (pathComposition C)
have refine_2 : ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
  W.paths.strictMap (pathComposition C) x_2 →
    ∀ (f : x ⟶ x_1) (h : W.paths f),
      W.multiplicativeClosure (X := x) (Y := x_1)
        (Functor.map (pathComposition C) f : Functor.obj (pathComposition C) x ⟶ Functor.obj (pathComposition C) x_1)
Tactic: refine le_antisymm ?_ fun _ _ _ ⟨h⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)
have refine_1 : ∀ (X Y : C) (f : X ⟶ Y) (hf : W f), W.paths.strictMap (pathComposition C) f
Tactic: refine (W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ Eq (α := obj (comap C g ⋙ comap (C ∘ g) f) X ⟶ obj (comap C (g ∘ f)) Y)
    (map (comap C g ⋙ comap (C ∘ g) f) f' ≫ fun (b : K) ↦ 𝟙 (Y (g (f b))))
    ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫ map (comap C (g ∘ f)) f')
have simp : Eq (α :=
  Quiver.Hom (V := (j : K) → C (g (f j)))
    (obj
      (comp (D := (j : J) → C (g j))
        { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
          map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry }
        { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
          map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry })
      X)
    fun (i : K) ↦ Y (g (f i)))
  (map
      (comp (D := (j : J) → C (g j))
        { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
          map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry :
          ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
        { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
          map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry :
          ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
      f' ≫
    fun (b : K) ↦ 𝟙 (Y (g (f b))))
  (CategoryStruct.comp (Y := fun (i : K) ↦ X (g (f i))) (fun (b : K) ↦ 𝟙 (X (g (f b)))) fun (i : K) ↦ f' (g (f i)))
Tactic: simp only [comap, Function.comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ Eq (α := obj (comap C (g ∘ f)) X ⟶ obj (comap C g ⋙ comap (C ∘ g) f) Y)
    (map (comap C (g ∘ f)) f' ≫ fun (b : K) ↦ 𝟙 (Y (g (f b))))
    ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫ map (comap C g ⋙ comap (C ∘ g) f) f')
have simp : Eq (α :=
  Quiver.Hom (V := (j : K) → C (g (f j))) (fun (i : K) ↦ X (g (f i)))
    (obj
      (comp (D := (j : J) → C (g j))
        { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
          map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry }
        { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
          map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry })
      Y))
  (CategoryStruct.comp (Y := fun (i : K) ↦ Y (g (f i))) (fun (i : K) ↦ f' (g (f i))) fun (b : K) ↦ 𝟙 (Y (g (f b))))
  ((fun (b : K) ↦ 𝟙 (X (g (f b)))) ≫
    map
      (comp (D := (j : J) → C (g j))
        { obj := fun (f : (i : I) → C i) (i : J) ↦ f (g i),
          map := fun {X Y : (i : I) → C i} (α : X ⟶ Y) (i : J) ↦ α (g i), map_id := sorry, map_comp := sorry :
          ((i : I) → C i) ⥤ ((j : J) → C (g j)) }
        { obj := fun (f_1 : (i : J) → C (g i)) (i : K) ↦ f_1 (f i),
          map := fun {X Y : (i : J) → C (g i)} (α : X ⟶ Y) (i : K) ↦ α (f i), map_id := sorry, map_comp := sorry :
          ((i : J) → C (g i)) ⥤ ((j : K) → C (g (f j))) })
      f')
Tactic: simp only [comap, Function.comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)
have rw : (f.hom ≫ f.inv) i = 𝟙 (X i)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.hom ≫ f.inv) i = 𝟙 (X i)
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)
have rw₁ : Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 X i : X i ⟶ X i) (𝟙 (X i) : X i ⟶ X i)
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.hom ≫ f.inv) i = 𝟙 (X i)
rw₁ : Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 X i : X i ⟶ X i) (𝟙 (X i) : X i ⟶ X i)
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)
have rw₂ : Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 (X i)) (𝟙 (X i))
Tactic: rw [← comp_apply, Iso.hom_inv_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)
have rw : (f.inv ≫ f.hom) i = 𝟙 (Y i)
Tactic: rw [← comp_apply, Iso.inv_hom_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.inv ≫ f.hom) i = 𝟙 (Y i)
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)
have rw₁ : Eq.{v₁ + 1} (α := Y i ⟶ Y i) (𝟙 Y i : Y i ⟶ Y i) (𝟙 (Y i) : Y i ⟶ Y i)
Tactic: rw [← comp_apply, Iso.inv_hom_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
rw : (f.inv ≫ f.hom) i = 𝟙 (Y i)
rw₁ : Eq.{v₁ + 1} (α := Y i ⟶ Y i) (𝟙 Y i : Y i ⟶ Y i) (𝟙 (Y i) : Y i ⟶ Y i)
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)
have rw₂ : Eq.{v₁ + 1} (α := Y i ⟶ Y i) (𝟙 (Y i)) (𝟙 (Y i))
Tactic: rw [← comp_apply, Iso.inv_hom_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
⊢ Eq.{v₁ + 1} (α := x i ⟶ x' i) (eqToHom h i : x i ⟶ x' i) (eqToHom ⋯ : x i ⟶ x' i)
have subst : Eq.{v₁ + 1} (α := x i ⟶ x i) (eqToHom sorry i : x i ⟶ x i) (eqToHom sorry : x i ⟶ x i)
Tactic: subst h
Cleared hypotheses: x', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f = f'
have h_map : autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom sorry ≫ f'.map f_1 ≫ eqToHom sorry) ext._auto_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
h_map : autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1
⊢ f = f'
have h_obj : ∀ (X : A), f.obj X = f'.obj X
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
⊢ f.obj X = f'.obj X
have h_obj : ∀ (i : I), f.obj X i = f'.obj X i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (hypothesis)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
i : I
⊢ f.obj X i = f'.obj X i
have h₁ : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
Tactic: specialize h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (hypothesis)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.obj X i = f'.obj X i
have this : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X
Tactic: have := congr_obj h X
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯
have h_map : ∀ (i : I), f.map g i = (eqToHom sorry ≫ f'.map g ≫ eqToHom sorry) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (hypothesis)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
⊢ f.map g i = (eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯) i
have h₁ : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
Tactic: specialize h i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (hypothesis)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst_1 : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h_1 : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.map g i = (eqToHom ⋯ ≫ f'.map g ≫ eqToHom ⋯) i
have this : (f ⋙ Pi.eval C i).map g = eqToHom sorry ≫ (f' ⋙ Pi.eval C i).map g ≫ eqToHom sorry
Tactic: have := congr_hom h g
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst_1 : (i : I) → Category.{v₂, u₂} (D i)
F_1 G_1 : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) (D i)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x x_1 : E
f : x ⟶ x_1
⊢ (F.map f ≫ fun (i : I) ↦ (τ i).app x_1) = (fun (i : I) ↦ (τ i).app x) ≫ G.map f
have w : ∀ (i : I), Eq.{v₁ + 1} ((F.map f ≫ fun (i : I) ↦ (τ i).app x_1) i) (((fun (i : I) ↦ (τ i).app x) ≫ G.map f) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)
have mp : IsIso f → ∀ (i : I), IsIso (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
mp : IsIso f → ∀ (i : I), IsIso (f i)
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)
have mpr : (∀ (i : I), IsIso (f i)) → IsIso f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
⊢ Equivalence.{v₁, v₁, u₁, u₁} (C i) (C j)
have subst : Equivalence.{v₁, v₁, u₁, u₁} (C i) (C i)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
⊢ Eq (α := ((i : I) → C i) ⥤ C j) (eval C i ⋙ Equivalence.functor (eqToEquivalence C h)) (eval C j)
have subst : Eq (α := ((i : I) → C i) ⥤ C i) (eval C i ⋙ Equivalence.functor (eqToEquivalence C sorry)) (eval C i)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Basic (goal)
Goal:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' j' : J
h : i' = j'
⊢ Eq (α := Functor.{v₁, v₁, u₁, u₁} (C (f i')) (C (f j'))) (Equivalence.functor (eqToEquivalence C ⋯))
    (Equivalence.functor (eqToEquivalence (fun (i' : J) ↦ C (f i')) h))
have subst : Eq (α := Functor.{v₁, v₁, u₁, u₁} (C (f i')) (C (f i'))) (Equivalence.functor (eqToEquivalence C sorry))
  (Equivalence.functor (eqToEquivalence (fun (i' : J) ↦ C (f i')) sorry))
Tactic: subst h
Cleared hypotheses: j', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Pi.Monoidal (goal)
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
inst_1 : (i : I) → MonoidalCategory.{v₁, u₁} (C i)
A B X Y : (i : I) → C i
f : A ⟶ B
g : X ⟶ Y
⊢ Eq (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y) (f ⊗ₘ g) (f ▷ X ≫ B ◁ g)
have w : ∀ (i : I),
  Eq.{v₁ + 1} (α := tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
    ((f ⊗ₘ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
    ((f ▷ X ≫ B ◁ g) i : tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) A X i ⟶ tensorObj (𝒞 := pi.{w₁, v₁, u₁} C) B Y i)
Tactic: ext i