mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
          ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
      colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor =
    (colimMap
          (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom) ≫
        colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor) ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
        colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor

Tactic:
by
    ext d
    simp only [Functor.comp_obj, Grothendieck.ιNatTrans, ι_colimMap_assoc, NatTrans.comp_app,
      whiskerRight_app, Functor.associator_hom_app, Category.comp_id, colimit.ι_pre, Category.assoc,
      colimit.ι_pre_assoc]
    rw [← Category.assoc, ← G.map_comp]
    conv_rhs => rw [← colimit.eqToHom_comp_ι (Grothendieck.ι F Z ⋙ G)
      (j := (F.map (f ≫ g)).toFunctor.obj d) (by simp)]
    rw [← Category.assoc, ← eqToHom_map G (by simp), ← G.map_comp, Grothendieck.eqToHom_eq]
    congr 2
    fapply Grothendieck.ext
    · simp only [eqToHom_refl, Category.assoc, Grothendieck.comp_base,
        Category.comp_id]
    · simp only [Grothendieck.ι_obj, eqToHom_refl,
        Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber, Functor.map_id]
      conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]
      conv_rhs => rw [eqToHom_trans, eqToHom_trans]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
⊢ (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
(iterate 2 apply colimit.hom_ext; intro); simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
b : IsTerminal (((evaluation Dᵒᵖ (Type v)).obj (op d)).obj (colimit (F ⋙ yoneda))) :=
  IsTerminal.isTerminalObj ((evaluation Dᵒᵖ (Type v)).obj (op d)) (colimit (F ⋙ yoneda)) h
⊢ IsTerminal (colimit (F ⋙ coyoneda.obj (op d)))

Tactic:
exact b.ofIso <| preservesColimitIso ((evaluation _ _).obj (Opposite.op d)) (F ⋙ yoneda)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j : C
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j

Tactic:
by
  -- This point is that this would be true if we took `lift (F.obj j)` to just be `j`
  -- and `homToLift (F.obj j)` to be `𝟙 (F.obj j)`.
  apply induction F fun X k => s.π.app X ≫ G.map k = (s.π.app j :)
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← s.w f]
    rw [← w] at h
    simpa using h
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← s.w f] at h
    rw [← w]
    simpa using h
  · exact s.w (𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝² : HasPullback f₁ f₂
inst✝¹ : HasPullback f₃ f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit
    (PullbackCone.mk
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)

Tactic:
apply topSquareIsPullback _ rfl (pullbackIsPullback f₁ f₂)
  simpa [PullbackCone.pasteVert] using PullbackCone.mkSelfIsLimit (pullbackIsPullback _ _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ IsColimit
    (PushoutCocone.mk
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
apply rightSquareIsPushout _ rfl (pushoutIsPushout _ _)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ IsColimit
    ((PushoutCocone.mk (pushout.inl g₁ g₂) (pushout.inr g₁ g₂) ⋯).pasteHoriz
      (PushoutCocone.mk
        (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
          (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P

Tactic:
by
  rwa [← isStableUnderBaseChange_iff_pullbacks_le]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₁₂ : S ⟶ X
v₂₂ : S ⟶ Y
g : Y ⟶ X
hv₁₂ : v₁₂ = v₂₂ ≫ g
inst✝¹ : HasPushout v₁₂ f
inst✝ : HasPushout v₂₂ f
H : P g
⊢ v₂₂ ≫ g ≫ pushout.inl v₁₂ f = f ≫ pushout.inr v₁₂ f

Tactic:
simp [pushout.condition, ← reassoc_of% hv₁₂]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ coproducts.{w, v, u} W f

Tactic:
by
  rw [coproducts_iff]
  refine ⟨Shrink J, ?_⟩
  rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z) = fst W Y ⊗ₘ fst X Z

Tactic:
ext <;> simp [tensorδ]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z) = snd W Y ⊗ₘ snd X Z

Tactic:
ext <;> simp [tensorδ]

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ (α_ S T U).hom ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑(T ⊗ U))).hom ≫ (α_ T U S).hom =
    (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom ▷ U ≫
      (α_ T S U).hom ≫ T ◁ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom

Tactic:
by ext : 1; dsimp; ext <;> rfl

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ (α_ S T U).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑(S ⊗ T) ↑U)).hom ≫ (α_ U S T).inv =
    S ◁ (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom ≫
      (α_ S U T).inv ≫ (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom ▷ T

Tactic:
by ext : 1; dsimp; ext <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Parametrized

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
⊢ adj₂.homEquiv ((adj₂.adj Y₁).counit.app X₃) ≫ (G.map f.op).app X₃ =
    adj₂.homEquiv ((F.obj X₁).map ((G.map f.op).app X₃) ≫ (adj₂.adj X₁).counit.app X₃)

Tactic:
homEquiv_naturality_two

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
⊢ adj₂.homEquiv ((adj₂.adj Y₁).counit.app X₃) ≫ (G.map f.op).app X₃ =
    (G.map f.op).app X₃ ≫ adj₂.homEquiv ((adj₂.adj X₁).counit.app X₃)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i

Tactic:
have := Classical.decEq ι
  rw [← coe_dualBasis, linearCombination_dualBasis]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ + finrank K ↥(U ⊓ W) = finrank K V

Tactic:
h.disjoint.eq_bot,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ + finrank K ↥⊥ = finrank K V
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ η_ (ᘁY) Y ≫ (ᘁf) ▷ Y = η_ (ᘁX) X ≫ ᘁX ◁ f

Tactic:
apply_fun (tensorRightHomEquiv _ (ᘁY) Y _).symm
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v

Tactic:
simp_rw [isOrthoᵢ_def]
  constructor <;> exact fun h i j hij ↦ h j i hij.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)

Tactic:
by
  classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
m✝ : t.asCofork.pt ⟶ s.pt
hm : t.asCofork.π ≫ m✝ = s.π
⊢ m✝ = t.rightSection ≫ s.π

Tactic:
by
      simp [← hm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (f ≫ q.rightRetraction) = F.map q.leftRetraction ≫ F.map ι

Tactic:
q.top_rightRetraction,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (q.leftRetraction ≫ ι) = F.map q.leftRetraction ≫ F.map ι
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.flip.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.flip.SeparatingLeft

Tactic:
refine IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.flip.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
i : n
⊢ (B.flip (v i)) (v i) ≠ 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ W ≤ W.dualAnnihilator.subtype.flip.ker

Tactic:
intro w hw
    ext ⟨φ, hφ⟩
    exact (mem_dualAnnihilator φ).mp hφ w hw

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α β : Type u_4} (a : α ≃ β),
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

pp: case h_empty
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ (W : PEmpty.{u_4 + 1} → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

pp: case h_option
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α : Type u_4} [Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
· intro α β h hyp W
    rw [← h.iInf_comp, hyp _, ← h.iSup_comp]

Goal state after:
case h_empty
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ (W : PEmpty.{u_4 + 1} → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

case h_option
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α : Type u_4} [Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case h_option
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α : Type u_4} [Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
· intro α _ h W
    rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0

Tactic:
by
    have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hf.w]
    simp [reassoc']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (Cone.postcompose
          (parallelPair.ext (Arrow.rightFunc.mapIso e) (Iso.refl ((parallelPair g 0).obj WalkingParallelPair.one)) ⋯
              ⋯).hom).obj
      (KernelFork.ofι f ⋯) ≅
    KernelFork.ofι f' ⋯

Tactic:
· exact Fork.ext (Arrow.leftFunc.mapIso e)

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
w : Dual R N ⊗[R] Dual R M
z : M ⊗[R] N
⊢ ((dualDistrib R N M) w) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) w)) z

Tactic:
induction w

Goal state after:
case zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
z : M ⊗[R] N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) z

case tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
z : M ⊗[R] N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) z

case add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
z : M ⊗[R] N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) z
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) z
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) z
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ n = w
⊢ u = v

Tactic:
Cofork.π_ofπ,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 ≫ n = w
⊢ u = v
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g

Tactic:
Cofork.π_ofπ,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = σ ≫ g
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fun x ↦ β⁻¹ • x) ((fun x ↦ β • x) x) = x

Tactic:
by
        dsimp only
        rw [← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ ∀ (a b : HomologyMapData φ h₁ h₂), a = b

Tactic:
rintro ⟨left₁, right₁⟩ ⟨left₂, right₂⟩
  simp only [mk.injEq, eq_iff_true_of_subsingleton, and_self]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ h.cyclesIso.hom ≫ h.i = S.iCycles

Tactic:
by
  dsimp [iCycles, LeftHomologyData.cyclesIso]
  simp only [cyclesMap'_i, id_τ₂, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

Tactic:
have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]
    have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ]
    cases ψ₁
    cases ψ₂
    congr

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁴ : S₁.HasRightHomology
inst✝³ : S₂.HasRightHomology
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap φ)

Tactic:
dsimp only [rightHomologyMap]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j

Tactic:
by
    ext
    · apply IsColimit.fac h₁
    · apply IsColimit.fac h₂
    · apply IsColimit.fac h₃

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
⊢ Injective X

Tactic:
refine Injective.mk (fun {A B} f e _ ↦ ?_)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
A B : C
f : A ⟶ X
e : A ⟶ B
x✝ : Mono e
⊢ ∃ h, e ≫ h = f
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Epi (e.hom.τ₂ ≫ S₂.g)
⊢ Epi S₂.g

Tactic:
exact epi_of_epi e.hom.τ₂ _

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ S.Exact

Tactic:
(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ S.iCycles = 0

Tactic:
← cancel_epi S.toCycles,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ S.toCycles ≫ S.iCycles = S.toCycles ≫ 0