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

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ : ShortComplex C
⊢ mapToComposableArrows (𝟙 S₁) = 𝟙 S₁.toComposableArrows

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
ψ : S₂ ⟶ S₃
⊢ mapToComposableArrows (φ ≫ ψ) = mapToComposableArrows φ ≫ mapToComposableArrows ψ

Tactic:
by

Goal state after:
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
hS : S.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ S.map' i j ⋯ ⋯ ≫ S.map' j k ⋯ hk = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ π ≫ a = x₁ ≫ S.f

Tactic:
by

Goal state after:
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₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
by

Goal state after:
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
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ (a ≫ S.iCycles) ≫ S.g = 0

Tactic:
by

Goal state after:
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 0
i : ℕ
hi : i + 2 ≤ 0
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
by

Goal state after:
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
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ π ≫ a = x₁ ≫ S.toCycles

Tactic:
by

Goal state after:
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
⊢ S.Exact ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
by

Goal state after:
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 1
i : ℕ
hi : i + 2 ≤ 1
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
by

Goal state after:
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
hS : S.Exact
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
by

Goal state after:
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
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ (z ≫ S.iCycles) ≫ S.g = 0

Tactic:
by

Goal state after:
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
hS : S.Exact
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ (S.sc' ⋯ i j k hij hjk hk).Exact

Tactic:
by

Goal state after:
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
γ : A ⟶ S.homology
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
by

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
f : X ⟶ ↑M
x : X
⊢ (ConcreteCategory.hom (freeDesc f)) (freeMk x) = (ConcreteCategory.hom f) x

Tactic:
by

Goal state after:
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
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ Cofork.π c ≫ (Iso.refl c.pt).hom =
    Cofork.π (CokernelCofork.ofπ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.g ⋯)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : Type u
f : X ⟶ Y
x : X
⊢ (ConcreteCategory.hom ((free R).map f)) (freeMk x) = freeMk ((ConcreteCategory.hom f) x)

Tactic:
by

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✝ : (free R).obj X ⟶ M
⊢ (fun ψ ↦ freeDesc (↾⇑(ConcreteCategory.hom ψ))) ((fun φ ↦ ↾fun x ↦ (ConcreteCategory.hom φ) (freeMk x)) x✝) = x✝

Tactic:
by

Goal state after:
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
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
by

Goal state after:
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:
by

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:
by

Goal state after:
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
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ (x₂ - x₂') ≫ S.g = 0

Tactic:
by

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
⊢ (adj R).homEquiv X M = freeHomEquiv

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
this :
  S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔ S.liftCycles (x₂ - x₂') ⋯ ≫ S.homologyπ = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
by

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:
by

Goal state after:
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:
by

Goal state after:
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
x₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
by

Goal state after:
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
z₂ : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
z₂ : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
z₂ : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = x₁ ≫ S.toCycles

Tactic:
by

Goal state after:
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 0
i : ℕ
hi : i + 2 ≤ 0
⊢ (S.sc ⋯ i hi).Exact

Tactic:
by

Goal state after:
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
z₂ z₂' : A ⟶ S.cycles
⊢ (z₂ ≫ S.iCycles) ≫ S.g = 0

Tactic:
by

Goal state after:
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
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ = S.liftCycles (z₂ ≫ S.iCycles) ⋯

Tactic:
by

Goal state after:
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 1
i : ℕ
hi : i + 2 ≤ 1
⊢ (S.sc ⋯ i hi).Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (εIso R).inv) (freeMk x) = 1

Tactic:
by

Goal state after:
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
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ (z₂' ≫ S.iCycles) ≫ S.g = 0

Tactic:
by

Goal state after:
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
h : S.IsComplex
⊢ 0 + 2 ≤ 2

Tactic:
by

Goal state after:
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
z₂' : A ⟶ S.cycles
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ z₂' = S.liftCycles (z₂' ≫ S.iCycles) ⋯

Tactic:
by

Goal state after:
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
h :
  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
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

Tactic:
by

Goal state after:
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
z₂ z₂' : A ⟶ S.cycles
⊢ z₂ ≫ S.homologyπ = z₂' ≫ S.homologyπ ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = π ≫ z₂' + x₁ ≫ S.toCycles

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μIso R X Y).hom) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

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

Tactic:
by

Goal state after:
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
h : S.Exact
⊢ 0 + 2 ≤ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (μIso R X Y).inv) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
by

Goal state after:
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
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

Tactic:
by

Goal state after:
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₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
this : S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
f : X ⟶ Y
X' : Type u
⊢ (free R).map f ▷ (free R).obj X' ≫ (μIso R Y X').hom = (μIso R X X').hom ≫ (free R).map (f ▷ X')

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y X' : Type u
f : X ⟶ Y
⊢ (free R).obj X' ◁ (free R).map f ≫ (μIso R X' Y).hom = (μIso R X' X).hom ≫ (free R).map (X' ◁ f)

Tactic:
by

Goal state after:
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₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ 𝟙 A ≫ x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f

Tactic:
by

Goal state after:
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.Exact
⊢ 0 + 2 ≤ n + 2

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
      (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom

Tactic:
by

Goal state after:
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)
hS : S.Exact
⊢ S.δ₀.Exact

Tactic:
by

Goal state after:
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
⊢ S.Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (λ_ ((free R).obj X)).hom = (εIso R).hom ▷ (free R).obj X ≫ (μIso R (𝟙_ (Type u)) X).hom ≫ (free R).map (λ_ X).hom

Tactic:
by

Goal state after:
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.Exact
⊢ n + 2 ≤ n + 2

Tactic:
by

Goal state after:
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₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ S₁.g = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : Type u
⊢ (ρ_ ((free R).obj X)).hom = (free R).obj X ◁ (εIso R).hom ≫ (μIso R X (𝟙_ (Type u))).hom ≫ (free R).map (ρ_ X).hom

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (η (free R))) (freeMk x) = 1

Tactic:
by

Goal state after:
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:
by

Goal state after: