-- Mathlib/CategoryTheory/Localization/StructuredArrow.lean
private lemma induction_structuredArrow'
    (hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X))))
    (hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
      P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f)))
    (hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
      P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv)))
    (g : StructuredArrow (W.Q.obj X) W.Q) : P g

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
⊢ P g

Tactic:
suffices ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀),
    P (StructuredArrow.mk ((Quotient.functor (relations W)).map f)) by
  obtain ⟨Y, g, rfl⟩ := g.mk_surjective
  obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g
  exact this g

Result:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
⊢ ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))

Proof state:
case nil
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
Y₀ : Paths (LocQuiver W)
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map Quiver.Path.nil))

Tactic:
exact hP₀

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
⊢ P g

Tactic:
let X₀ : Paths (LocQuiver W) := ⟨X⟩

Result:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
⊢ P g

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
⊢ ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))

Tactic:
intro Y₀ f

Result:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
Y₀ : Paths (LocQuiver W)
f : X₀ ⟶ Y₀
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))

Proof state:
case intro.intro.intro
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := { obj := X }
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g : Paths.of.obj { obj := X } ⟶ Paths.of.obj { obj := Y }
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))

Tactic:
exact this g

Result:
no goals

Proof state:
case cons.inl
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g✝ : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
Y₀ b✝ c✝ : Paths (LocQuiver W)
f : Quiver.Path X₀ b✝
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
g : b✝.obj ⟶ c✝.obj
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inl g))))

Tactic:
exact hP₁ g _ hf

Result:
no goals

Proof state:
case cons.inr.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
Y₀ b✝ c✝ : Paths (LocQuiver W)
f : Quiver.Path X₀ b✝
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
w : c✝.obj ⟶ b✝.obj
hw : W w
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inr ⟨w, hw⟩))))

Tactic:
simpa only [← Construction.wInv_eq_isoOfHom_inv w hw] using hP₂ w hw _ hf

Result:
no goals