mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Tactic:
·

Goal state after:
case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
hq : nil.length = nil.length
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ nil = nil

pp: case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
·

Goal state after:
case nil.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
hq : nil.length = nil.length
h : p₁.comp nil = p₂.comp nil
⊢ p₁ = p₂ ∧ nil = nil
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
·

Goal state after:
case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
·

Goal state after:
case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂

Tactic:
·

Goal state after:
case cons.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝¹ c✝ : V
q₁ : Path b b✝¹
f₁ : b✝¹ ⟶ c✝
ih : ∀ {q₂ : Path b b✝¹}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ c✝
hq : (q₁.cons f₁).length = (q₂.cons f₂).length
h : p₁.comp (q₁.cons f₁) = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂.cons f₂
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

pp: case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g

Tactic:
·

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

pp: case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
·

Goal state after:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g

Tactic:
·

Goal state after:
case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
·

Goal state after:
case cons.succ
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
n✝ : ℕ
hp : (p.cons q).length = n✝ + 1 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X

pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
·

Goal state after:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
·

Goal state after:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1

pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1) → p.length ≠ 0

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case inl
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match (Sum.inl val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

pp: case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
·

Goal state after:
case inl
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match (Sum.inl val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
·

Goal state after:
case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b c : V
e : a ⟶ c
p' : Path c b
h : (e.toPath.comp p').length ≠ 0
h_len : (e.toPath.comp p').length = (e.toPath.comp p').length - 1 + 1
hp' : p'.length = (e.toPath.comp p').length - 1
⊢ (e.toPath.comp p').length = p'.length + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1) → p.length ≠ 0

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1) → p.length ≠ 0
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X

pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))

Tactic:
·

Goal state after:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c p' e, p = p'.cons e

pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c p' e, p = p'.cons e
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))

Tactic:
·

Goal state after:
case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map.inl
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inl val✝)))

pp: case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))

Tactic:
·

Goal state after:
case h_map.inl
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inl val✝)))
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))

Tactic:
·

Goal state after:
case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
·

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
·

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure ≤ P.map F

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.map F ≤ (P.strictMap F).isoClosure

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure ≤ P.map F
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.map F ≤ (P.strictMap F).isoClosure

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.map F ≤ (P.strictMap F).isoClosure
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mp
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y → P.map F Y

pp: case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y

Tactic:
·

Goal state after:
case mp
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ (P.ι ⋙ F).essImage Y → P.map F Y
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y

Tactic:
·

Goal state after:
case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ ⊤.map F Y → F.essImage Y

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ F.essImage Y → ⊤.map F Y

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ ⊤.map F Y → F.essImage Y
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ F.essImage Y → ⊤.map F Y

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ F.essImage Y → ⊤.map F Y
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.1 ∧ IsIso f.2

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f

Tactic:
·

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.1 ∧ IsIso f.2
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f

Tactic:
·

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2 → IsIso f
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ ∀ (X : Discrete I), G.obj X = F.obj X

pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ ∀ (X : Discrete I), G.obj X = F.obj X
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : 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

pp: case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1

Tactic:
·

Goal state after:
case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : 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
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1

Tactic:
·

Goal state after:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case mp
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)

pp: case mpr
I : 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), IsIso (f i)) → IsIso f

Tactic:
·

Goal state after:
case mp
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)
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case mpr
I : 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), IsIso (f i)) → IsIso f

Tactic:
·

Goal state after:
case mpr
I : 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), IsIso (f i)) → IsIso f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

pp: case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'

Tactic:
·

Goal state after:
case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'

Tactic:
·

Goal state after:
case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ (∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯) → mk f = mk f'
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → isomorphisms C = ⊤

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ isomorphisms C = ⊤ → IsGroupoid C

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → isomorphisms C = ⊤
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ isomorphisms C = ⊤ → IsGroupoid C

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ isomorphisms C = ⊤ → IsGroupoid C