mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
              λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝¹).hom).toBialgHom'))
        1)
      x✝ =
    (((TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝¹.carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        1)
      x✝
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
              ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : HopfAlgCat R
x✝ : x✝¹.carrier
⊢ (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝¹).hom).toBialgHom'))
        x✝)
      1 =
    (((TensorProduct.mk R x✝¹.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
          ((fun x ↦ ↑x)
            (((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
                  ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom.toBialgHom'))
        x✝)
      1
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → Epi f
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk = 𝟙 (S₁.sc' h₁ i j k hij hjk hk)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₁ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₂ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk).τ₃ = (𝟙 (S₁.sc' h₁ i j k hij hjk hk)).τ₃
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝ : (free R).obj X ⟶ M
⊢ (fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝) = x✝

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : (free R).obj X ⟶ M
x✝ : X
⊢ (ConcreteCategory.hom
        ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝¹)))
      (freeMk x✝) =
    (ConcreteCategory.hom x✝¹) (freeMk x✝)
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ (∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0

Tactic:
· rintro ⟨A', π, hπ, x, fac⟩
    simp [← cancel_epi π, reassoc_of% fac, condition]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝ : X ⟶ ↑M
⊢ (fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) x✝) = x✝

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
x✝¹ : X ⟶ ↑M
x✝ : X
⊢ (ConcreteCategory.hom
          ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x))
            ((fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) x✝¹))).toFun
      x✝ =
    (ConcreteCategory.hom x✝¹).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
⊢ freeHomEquiv.symm (f ≫ g) = (free R).map f ≫ freeHomEquiv.symm g

Tactic:
ext

Goal state after:
R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
x✝ : X
⊢ (ConcreteCategory.hom (freeHomEquiv.symm (f ≫ g))) (freeMk x✝) =
    (ConcreteCategory.hom ((free R).map f ≫ freeHomEquiv.symm g)) (freeMk x✝)
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk = 𝟙 (S₂.sc' h₂ i j k hij hjk hk)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₁ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₂ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk).τ₃ = (𝟙 (S₂.sc' h₂ i j k hij hjk hk)).τ₃
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g : Y ⟶ (forget (ModuleCat R)).obj M
⊢ freeHomEquiv.symm (f ≫ g) = (free R).map f ≫ freeHomEquiv.symm g

Tactic:
ext; simp [freeHomEquiv]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ ↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit) = 𝟙 (𝟙_ (ModuleCat R))

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
⊢ (Hom.hom (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit))) 1 = (Hom.hom (𝟙 (𝟙_ (ModuleCat R)))) 1
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₁ = (𝟙 (S₁.sc h₁ i hi)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₂ = (𝟙 (S₁.sc h₁ i hi)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi).τ₃ = (𝟙 (S₁.sc h₁ i hi)).τ₃
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₁ = (𝟙 (S₂.sc h₂ i hi)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₂ = (𝟙 (S₂.sc h₂ i hi)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ (scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi).τ₃ = (𝟙 (S₂.sc h₂ i hi)).τ₃
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex ↔
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.IsComplex →
    S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
⊢ S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0 →
    S.IsComplex
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ S.Exact ↔ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ S.Exact → (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
⊢ (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact → S.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact ↔ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact → S.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor

Goal state after:
case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δ₀.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.δ₀.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact ↔ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact → S.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor

Goal state after:
case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ S.δlast.Exact

case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ S.δlast.Exact

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h₁ : S.δlast.Exact
h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (equivPullbackObj hc) x = (equivPullbackObj hc) y

Tactic:
ext

Goal state after:
case fst
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).1 = (↑((equivPullbackObj hc) y)).1

case snd
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (↑((equivPullbackObj hc) x)).2 = (↑((equivPullbackObj hc) y)).2
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = ↾fun p ↦ (↑p).1

Tactic:
ext

Goal state after:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
x✝ : PullbackObj f g
⊢ (hom ((pullbackIsoPullback f g).inv ≫ pullback.fst f g)).toFun x✝ = (hom (↾fun p ↦ (↑p).1)).toFun x✝
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = ↾fun p ↦ (↑p).2

Tactic:
ext

Goal state after:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
x✝ : PullbackObj f g
⊢ (hom ((pullbackIsoPullback f g).inv ≫ pullback.snd f g)).toFun x✝ = (hom (↾fun p ↦ (↑p).2)).toFun x✝
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
⊢ _root_.Prod.fst '' Subtype.val '' Set.univ = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
ext

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this : ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)
x✝ : (fun X ↦ X) X
⊢ x✝ ∈ _root_.Prod.fst '' Subtype.val '' Set.univ ↔ x✝ ∈ ⇑(hom f) ⁻¹' Set.range ⇑(hom g)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (h.isLimit.conePointUniqueUpToIso
          ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
      x₁ =
    (h.isLimit.conePointUniqueUpToIso
          ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
      y₁

Tactic:
ext

Goal state after:
case fst
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).1 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).1

case snd
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          x₁)).2 =
    (↑((h.isLimit.conePointUniqueUpToIso
              ((pullbackCone r b).isLimitAux (fun s ↦ ↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ⋯ ⋯ ⋯)).toEquiv
          y₁)).2