awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
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))
⊢ P
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      ((Equiv.symm (structuredArrowEquiv W W.Q L) : (a : StructuredArrow (L.obj X) L) → StructuredArrow (W.Q.obj X) W.Q)
        g))

Tactic:
apply induction_structuredArrow' W P'

Premises used: _private.0.CategoryTheory.Localization.induction_structuredArrow'
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
⊢ P (StructuredArrow.mk (𝟙 (L.obj X)))

Tactic:
hP₀
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
h :
  (structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      (StructuredArrow.mk (𝟙 (W.Q.obj X))) =
    StructuredArrow.mk (𝟙 (L.obj X))
⊢ P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))

Tactic:
convert! hP₀
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
⊢ (structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      (StructuredArrow.mk (𝟙 (W.Q.obj X))) =
    StructuredArrow.mk (𝟙 (L.obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ P (StructuredArrow.mk (Y := Y₂) ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₁) → L.obj X ⟶ L.obj Y₁) φ ≫ L.map f))

Tactic:
hP₁ f (homEquiv W W.Q L φ) hφ

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
h :
  Eq (α := StructuredArrow (L.obj X) L)
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
        (StructuredArrow.mk (φ ≫ W.Q.map f)) :
      StructuredArrow (L.obj X) L)
    (StructuredArrow.mk (Y := Y₂) ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₁) → L.obj X ⟶ L.obj Y₁) φ ≫ L.map f) :
      StructuredArrow (L.obj X) L)
⊢ P' (StructuredArrow.mk (φ ≫ W.Q.map f))

Tactic:
convert! hP₁ f (homEquiv W W.Q L φ) hφ

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ Eq (α := StructuredArrow (L.obj X) L)
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
        (StructuredArrow.mk (φ ≫ W.Q.map f)) :
      StructuredArrow (L.obj X) L)
    (StructuredArrow.mk (Y := Y₂) ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₁) → L.obj X ⟶ L.obj Y₁) φ ≫ L.map f) :
      StructuredArrow (L.obj X) L)

Tactic:
simp [homEquiv_comp]

Premises used: CategoryTheory.Localization.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
hw : W w
φ : W.Q.obj X ⟶ W.Q.obj Y₂
hφ : P' (StructuredArrow.mk φ)
⊢ P
    (StructuredArrow.mk (Y := Y₁)
      ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₂) → L.obj X ⟶ L.obj Y₂) φ ≫ (isoOfHom L W w hw).inv))

Tactic:
hP₂ w hw (homEquiv W W.Q L φ) hφ

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
hw : W w
φ : W.Q.obj X ⟶ W.Q.obj Y₂
hφ : P' (StructuredArrow.mk φ)
h :
  Eq (α := StructuredArrow (L.obj X) L)
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
        (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv)) :
      StructuredArrow (L.obj X) L)
    (StructuredArrow.mk (Y := Y₁)
        ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₂) → L.obj X ⟶ L.obj Y₂) φ ≫ (isoOfHom L W w hw).inv) :
      StructuredArrow (L.obj X) L)
⊢ P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))

Tactic:
convert! hP₂ w hw (homEquiv W W.Q L φ) hφ

Premises used: CategoryTheory.Localization.homEquiv, CategoryTheory.MorphismProperty.Q, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : 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 : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
hw : W w
φ : W.Q.obj X ⟶ W.Q.obj Y₂
hφ : P' (StructuredArrow.mk φ)
⊢ Eq (α := StructuredArrow (L.obj X) L)
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
        (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv)) :
      StructuredArrow (L.obj X) L)
    (StructuredArrow.mk (Y := Y₁)
        ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₂) → L.obj X ⟶ L.obj Y₂) φ ≫ (isoOfHom L W w hw).inv) :
      StructuredArrow (L.obj X) L)

Tactic:
simp [homEquiv_comp, homEquiv_isoOfHom_inv]

Premises used: CategoryTheory.Localization.homEquiv_comp, CategoryTheory.Localization.homEquiv_isoOfHom_inv
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
let : P g
⊢ P g

Tactic:
let g' := StructuredArrow.mk (T := L.op) (Y := op g.left) g.hom.op
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
change : P (CostructuredArrow.mk g'.hom.unop)
⊢ P g

Tactic:
change P (CostructuredArrow.mk g'.hom.unop)

Premises used: Quiver.Hom.unop, CategoryTheory.StructuredArrow.hom, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (𝟙 (L.op.obj (op Y)))).hom.unop)

Tactic:
hP₀

Premises used: Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (𝟙 (L.op.obj (op Y)))).hom.unop)

Tactic:
exact hP₀
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
Y₁ Y₂ : Cᵒᵖ
f : Y₁ ⟶ Y₂
φ : L.op.obj (op Y) ⟶ L.op.obj Y₁
hφ : P (CostructuredArrow.mk (StructuredArrow.mk φ).hom.unop)
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (φ ≫ L.op.map f)).hom.unop)

Tactic:
hP₁ f.unop φ.unop hφ

Premises used: Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
Y₁ Y₂ : Cᵒᵖ
f : Y₁ ⟶ Y₂
φ : L.op.obj (op Y) ⟶ L.op.obj Y₁
hφ : P (CostructuredArrow.mk (StructuredArrow.mk φ).hom.unop)
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (φ ≫ L.op.map f)).hom.unop)

Tactic:
exact hP₁ f.unop φ.unop hφ

Premises used: Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
Y₁ Y₂ : Cᵒᵖ
w : Y₁ ⟶ Y₂
hw : W.op w
φ : L.op.obj (op Y) ⟶ L.op.obj Y₂
hφ : P (CostructuredArrow.mk (StructuredArrow.mk φ).hom.unop)
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (φ ≫ (isoOfHom L.op W.op w hw).inv)).hom.unop)

Tactic:
simpa [isoOfHom_op_inv L W w hw] using hP₂ w.unop hw φ.unop hφ

Premises used: Quiver.Hom.unop, CategoryTheory.Localization.isoOfHom_op_inv
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
induction : ∀ (x : StructuredArrow (op (L.obj Y)) L.op), P (CostructuredArrow.mk x.hom.unop)
⊢ P (CostructuredArrow.mk g'.hom.unop)

Tactic:
induction g' using induction_structuredArrow L.op W.op with
  | hP₀ => exact hP₀
  | hP₁ f φ hφ => exact hP₁ f.unop φ.unop hφ
  | hP₂ w hw φ hφ => simpa [isoOfHom_op_inv L W w hw] using hP₂ w.unop hw φ.unop hφ
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
T₁ T₂ : Triangle.{v_2, u_2} D
e : T₂ ≅ T₁
h : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₁
obtain :
  ∀ (T' : Triangle.{v_1, u_1} C) (e' : T₁ ≅ obj L.mapTriangle T')
    (hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂

Tactic:
obtain ⟨T', e', hT'⟩ := h
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
T₁ T₂ : Triangle.{v_2, u_2} D
e : T₂ ≅ T₁
T' : Triangle.{v_1, u_1} C
e' : T₁ ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂

Tactic:
⟨T', e ≪≫ e', hT'⟩

Premises used: Set.Mem, setOf, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Functor.essImageDistTriang
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
T₁ T₂ : Triangle.{v_2, u_2} D
e : T₂ ≅ T₁
T' : Triangle.{v_1, u_1} C
e' : T₁ ≅ obj L.mapTriangle T'
hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂

Tactic:
exact ⟨T', e ≪≫ e', hT'⟩