awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
⊢ MorphismProperty.naturalityProperty α_app = ⊤

Tactic:
exact morphismProperty_eq_top_of_isMultiplicative _ _ α_nat

Premises used: CategoryTheory.Paths.morphismProperty_eq_top_of_isMultiplicative
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
⊢ W.paths (X := X) Path.nil

Tactic:
trivial

Premises used: trivial, CategoryTheory.MorphismProperty.paths
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
f : Y ⟶ Z
hp : W.paths p
hf : W f
⊢ W.paths (p.cons f)

Tactic:
⟨hp, hf⟩

Premises used: CategoryTheory.MorphismProperty.paths, And.intro
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
f : Y ⟶ Z
⊢ W.paths (p.cons f) ↔ W.paths p ∧ W f

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.MorphismProperty.paths
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ W.paths f.toPath

Tactic:
⟨trivial, hf⟩

Premises used: trivial, CategoryTheory.MorphismProperty.paths, And.intro
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ W.paths f.toPath ↔ W f

Tactic:
⟨fun h ↦ h.2, toPath_mem_paths⟩

Premises used: And.right, CategoryTheory.MorphismProperty.toPath_mem_paths, Iff.intro
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩

Premises used: CategoryTheory.MorphismProperty.paths, And.intro, _private.0.CategoryTheory.MorphismProperty.comp_mem_paths_iff.match_1, Iff.intro, Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
refine_3 : W.paths p ∧ W.paths q → ∀ (hp : W.paths p) (hq : W.paths q), W.paths (p.comp q)
⊢ W.paths (p.comp q) ↔ W.paths p ∧ W.paths q

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
h : W.paths (p.comp Path.nil)
⊢ W.paths p

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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.comp q').cons f)

Tactic:
rw [Path.comp_cons] at h

Premises used: Quiver.Path.comp_cons
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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

Tactic:
h' h.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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

Tactic:
exact h' h.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
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
⊢ 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

Premises used: Quiver.Path.comp_cons
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
h : W.paths (p.comp Path.nil)
⊢ W.paths (X := Y) Path.nil

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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 ((p.comp q').cons f)

Tactic:
rw [Path.comp_cons] at h

Premises used: Quiver.Path.comp_cons
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)

Tactic:
⟨h' h.1, h.2⟩

Premises used: CategoryTheory.MorphismProperty.paths, And.right, And.left, And.intro
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)

Tactic:
exact ⟨h' h.1, h.2⟩
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
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)
⊢ W.paths q

Tactic:
induction q with
    | nil => simp
    | cons q' f h' =>
      rw [Path.comp_cons] at h
      exact ⟨h' h.1, h.2⟩

Premises used: Quiver.Path.comp_cons
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
hp : W.paths p
h : W.paths p ∧ W.paths (X := Y) Path.nil
hq : W.paths (X := Y) Path.nil
⊢ W.paths (p.comp Path.nil)

Tactic:
hp

Premises used: Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
hp : W.paths p
h : W.paths p ∧ W.paths (X := Y) Path.nil
hq : W.paths (X := Y) Path.nil
⊢ W.paths (p.comp Path.nil)

Tactic:
exact hp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
hp : W.paths p
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)
h_1 : W.paths p ∧ W.paths (q.cons q')
hq : W.paths (q.cons q')
⊢ W.paths (p.comp (q.cons q'))

Tactic:
⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩

Premises used: CategoryTheory.MorphismProperty.paths, And.right, And.left, And.intro
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
hp : W.paths p
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)
h_1 : W.paths p ∧ W.paths (q.cons q')
hq : W.paths (q.cons q')
⊢ W.paths (p.comp (q.cons q'))

Tactic:
exact ⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)
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'))
⊢ W.paths (p.comp q)

Tactic:
induction q with
    | nil => exact hp
    | cons q q' h => exact ⟨h ⟨hp, hq.1⟩ hq.1, hq.2⟩
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : Paths C
p : X ⟶ Y
q : Y ⟶ Z
⊢ W.paths (p ≫ q) ↔ W.paths p ∧ W.paths q

Tactic:
W.comp_mem_paths_iff

Premises used: CategoryTheory.MorphismProperty.comp_mem_paths_iff
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ Monotone (α := MorphismProperty.{v_1, u_1} C) paths

Tactic:
fun _ _ h _ _ p ↦ p.rec (fun _ ↦ trivial) (fun _ _ hp' hp ↦ ⟨hp' hp.1, h _ hp.2⟩)

Premises used: Monotone, Quiver.Path.rec
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)
revert : ∀ (hp : W.paths p), W (composePath p)
⊢ W (composePath p)

Tactic:
revert hp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
h : W (𝟙 X)
⊢ ∀ (hp : W.paths (X := X) Path.nil), W (X := X) (composePath Path.nil)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
h : W (𝟙 X)
⊢ ∀ (hp : W.paths p), W (composePath p)

Tactic:
exact p.rec (by simpa) fun p f hp hp' ↦ W.comp_mem _ _ (hp hp'.1) hp'.2
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
revert : ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)
⊢ W (composePath p)

Tactic:
revert hp h
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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 (X := X) Path.nil) (h : 0 < Path.length.{u_1, v_1} (V := C) (a := X) Path.nil),
    W (X := X) (composePath Path.nil)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
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))
⊢ ∀ (hp : W.paths p) (h : 0 < p.length), W (composePath p)

Tactic:
refine p.rec (by simp) fun p f hp hp' hp'' ↦ ?_
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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))
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))
⊢ W (composePath (p.cons f))

Tactic:
cases p
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
c : C
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:
simpa [paths] using hp'

Premises used: CategoryTheory.MorphismProperty.paths
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
b c : C
f : b ⟶ c
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
⊢ 0 < (a.cons a_1).length

Tactic:
simp
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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
b c : C
f : b ⟶ c
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:
refine W.comp_mem _ _ (hp hp'.1 (by simp)) hp'.2

Premises used: CategoryTheory.MorphismProperty.comp_mem, And.right, And.left
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsMultiplicative
X Y : C
p : Path.{v_1, u_1} X Y
hp : W.paths p
⊢ W (composePath p)

Tactic:
W.composePath_mem_of_id_mem hp <| W.id_mem X

Premises used: CategoryTheory.MorphismProperty.id_mem, CategoryTheory.MorphismProperty.composePath_mem_of_id_mem
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.IsMultiplicative
⊢ W.paths ≤ W.inverseImage (pathComposition C)

Tactic:
fun _ _ _ ↦ W.composePath_mem

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.MorphismProperty.composePath_mem
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
h : W.paths.strictMap (pathComposition C) x
h_1 : W.paths.strictMap (pathComposition C) x_1
f : X ⟶ Y
hp : W.paths f
f_1 : Y ⟶ Z
hq : W.paths f_1
⊢ W.paths.strictMap (pathComposition C) (X := X) (Y := Z)
    (CategoryStruct.comp (Y := Y) (Functor.map (pathComposition C) f) (Functor.map (pathComposition C) f_1) : X ⟶ Z)

Tactic:
simpa using W.paths.map_mem_strictMap (pathComposition C) _ <| W.paths.comp_mem _ _ hp hq

Premises used: CategoryTheory.MorphismProperty.map_mem_strictMap, CategoryTheory.pathComposition, CategoryTheory.MorphismProperty.paths, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)

Tactic:
le_antisymm ?_ fun _ _ _ ⟨h⟩ ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)
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)
⊢ W.multiplicativeClosure = W.paths.strictMap (pathComposition C)

Tactic:
refine le_antisymm ?_ fun _ _ _ ⟨h⟩ ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
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)

Tactic:
(W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
refine_1 : ∀ (X Y : C) (f : X ⟶ Y) (hf : W f), W.paths.strictMap (pathComposition C) f
⊢ W.multiplicativeClosure ≤ W.paths.strictMap (pathComposition C)

Tactic:
refine (W.multiplicativeClosure_le_iff _).2 fun X Y f hf ↦ ?_

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ W.paths f.toPath

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : W f
⊢ W.paths.strictMap (pathComposition C) f

Tactic:
simpa using W.paths.map_mem_strictMap (pathComposition C) f.toPath (by simpa)

Premises used: CategoryTheory.MorphismProperty.map_mem_strictMap, CategoryTheory.pathComposition, CategoryTheory.MorphismProperty.paths, Quiver.Hom.toPath
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
x x_1 : C
x_2 : x ⟶ x_1
h_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:
composePath_mem _ <| monotone_paths W.le_multiplicativeClosure _ h

Premises used: CategoryTheory.MorphismProperty.monotone_paths, CategoryTheory.MorphismProperty.le_multiplicativeClosure, CategoryTheory.MorphismProperty.composePath_mem
-- Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
x x_1 : C
x_2 : x ⟶ x_1
h_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:
exact composePath_mem _ <| monotone_paths W.le_multiplicativeClosure _ h

Premises used: CategoryTheory.MorphismProperty.monotone_paths, CategoryTheory.MorphismProperty.le_multiplicativeClosure, CategoryTheory.MorphismProperty.composePath_mem
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X : (i : I) → C i
i : I
⊢ Eq.{v₁ + 1} (α := X i ⟶ X i) (𝟙 X i : X i ⟶ X i) (𝟙 (X i) : X i ⟶ X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y Z : (i : I) → C i
f : X ⟶ Y
g : Y ⟶ Z
i : I
⊢ (f ≫ g) i = f i ≫ g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f g : X ⟶ Y
w : ∀ (i : I), f i = g i
⊢ f = g

Tactic:
funext (w ·)

Premises used: funext
-- Module: Mathlib.CategoryTheory.Pi.Basic
Goal:
I : Type w₀
J_1 : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
g : J → I
⊢ (j : J) → Category.{v₁, u₁} (C (g j))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Pi.Basic
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
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 := ⋯, map_comp := ⋯ }
          { 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 := ⋯, map_comp := ⋯ })
        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 := ⋯, map_comp := ⋯ :
            ((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 := ⋯, map_comp := ⋯ :
            ((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)))
⊢ 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')

Tactic:
simp only [comap, Function.comp]

Premises used: Function.comp, CategoryTheory.Pi.comap