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

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
⊢ P g

Tactic:
rw [← (structuredArrowEquiv W W.Q L).apply_symm_apply g]

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
⊢ P ((structuredArrowEquiv W W.Q L) ((structuredArrowEquiv W W.Q L).symm g))

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

Tactic:
let P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun g ↦ P (structuredArrowEquiv W W.Q L g)

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
⊢ P g

Proof state:
case hP₁
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
⊢ ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))

Tactic:
intros Y₁ Y₂ f φ hφ

Result:
case hP₁
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ P' (StructuredArrow.mk (φ ≫ W.Q.map f))

Proof state:
case h.e'_1
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
⊢ (structuredArrowEquiv W W.Q L) (StructuredArrow.mk (𝟙 (W.Q.obj X))) = StructuredArrow.mk (𝟙 (L.obj X))

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_1
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g => P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ (structuredArrowEquiv W W.Q L) (StructuredArrow.mk (φ ≫ W.Q.map f)) =
    StructuredArrow.mk ((homEquiv W W.Q L) φ ≫ L.map f)

Tactic:
simp [homEquiv_comp]

Result:
no goals