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

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

Tactic:
by
  intro X Y f hf
  exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ (μ ⊗ₘ 𝟙 M) ≫ μ

Tactic:
lift_map_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂ ≫ μ) (f₃ ≫ 𝟙 M) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ (𝟙 M ⊗ₘ μ) ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
lift_map_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (f₁ ≫ 𝟙 M) (lift f₂ f₃ ≫ μ) ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ PreservesLimit (Functor.empty C) F

Tactic:
apply preservesLimit_of_preserves_limit_cone isTerminalTensorUnit

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ IsLimit (F.mapCone (asEmptyCone (𝟙_ C)))
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (𝟙 A) ι ≫ (f ⊗ₘ f) ≫ μ = toUnit A ≫ η
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
lift_map_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (𝟙 A ≫ f) (ι ≫ f) ≫ μ = toUnit A ≫ η
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift ι (𝟙 A) ≫ (f ⊗ₘ f) ≫ μ = toUnit A ≫ η
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
lift_map_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (ι ≫ f) (𝟙 A ≫ f) ≫ μ = toUnit A ≫ η
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X✝ : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((yoneda.obj G).map f ≫ ↾fun f ↦ ⅟f) = (↾fun f ↦ ⅟f) ≫ (yoneda.obj G).map f

Tactic:
ext g
      simp only [yoneda_obj_map, TypeCat.Fun.toFun_apply, comp_apply,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, invOf_eq_iff_left]
      rw [← comp_mul, invOf_mul_self, comp_one]

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ Injective ⇑(Dual.eval R M)

Tactic:
intro m m' eq
  simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq
  exact b.ext_elem fun i ↦ eq (b.coord i)

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
⊢ Module.rank K V₁ = Module.rank K ↥(db.coprod eb).ker

Tactic:
apply LinearEquiv.rank_eq

Goal state after:
case e_a
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_20
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
B : LinearMap.BilinMap R M N
⊢ (∀ (x y : M), (B x) y = (B y) x) ↔ B = flip B

Tactic:
simp [LinearMap.ext_iff₂]

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
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (q.leftSection ≫ f) = F.map π ≫ F.map q.rightSection

Tactic:
q.leftSection_top,

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
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (π ≫ q.rightSection) = F.map π ≫ F.map q.rightSection
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
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection

Tactic:
by rw [← F.map_comp, q.leftSection_top, F.map_comp]

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

Goal state before:
pp: case h₀
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.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ ∀ b ∈ vi.support, b ≠ i → (RingHom.id R) (vi b) • (B (v b)) (v i) = 0

pp: case h₁
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.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ i ∉ vi.support → (RingHom.id R) (vi i) • (B (v i)) (v i) = 0

Tactic:
· intro j _hj hij
    replace hij : B (v j) (v i) = 0 := hO hij
    rw [hij, RingHom.id_apply, smul_zero]

Goal state after:
case h₁
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.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ i ∉ vi.support → (RingHom.id R) (vi i) • (B (v i)) (v i) = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

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
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫
        colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
    q ≫ h

Tactic:
slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]

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
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ (q ≫ coequalizer.π f' g') ≫ coequalizer.desc h wh = q ≫ h
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p

Tactic:
refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩
  have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
    simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]
  rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
    Submodule.one_le_finrank_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
hhp : h ≫ p = 0
s : cokernel g ⟶ cokernel (kernel.ι f)
hs : u ≫ s = p
⊢ g = 0

Tactic:
have hs' : p ≫ cokernel.π g ≫ s = p ≫ 𝟙 I := by rw [← Category.assoc, hs, Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
hhp : h ≫ p = 0
s : cokernel g ⟶ cokernel (kernel.ι f)
hs : u ≫ s = p
hs' : p ≫ cokernel.π g ≫ s = p ≫ 𝟙 I
⊢ g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ cokernel.π (diag X) ≫ (asIso (r X)).inv = σ

Tactic:
asIso_inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ cokernel.π (diag X) ≫ inv (r X) = σ
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.fst =
    s.ι ≫ biprod.fst

Tactic:
rw [Fork.ι_ofι, Category.assoc]

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.fst = s.ι ≫ biprod.fst
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι (pullbackToBiproductFork f g)) ≫ biprod.snd =
    s.ι ≫ biprod.snd

Tactic:
rw [Fork.ι_ofι, Category.assoc]

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullbackToBiproduct f g ≫ biprod.snd = s.ι ≫ biprod.snd
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case refine_2
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl

Goal state after:
case refine_2
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ False
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ Nonempty (NormalEpi f)

Tactic:
by
    obtain ⟨hf⟩ := h f
    exact ⟨{
      W := hf.kernelFork.pt
      g := hf.kernelFork.ι
      w := by simp
      isColimit :=
        have : IsIso hf.imageι :=
          KernelFork.IsLimit.isIso_ι _ hf.imageIsKernel (by simp [← cancel_epi f])
        IsColimit.ofIsoColimit hf.imageIsCokernel (Cofork.ext (asIso hf.imageι)) }⟩

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 S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ h₁.i ≫ φ.τ₂ = ψ₂.φK ≫ h₂.i

Tactic:
commi

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ h₁.i ≫ φ.τ₂ = h₁.i ≫ φ.τ₂
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₂
⊢ ψ₁.φQ = ψ₂.φQ

Tactic:
rw [← cancel_epi h₁.p, commp, commp]

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 : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk

Tactic:
by
  rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0

Tactic:
simp only [← cancel_epi φ.τ₁, comp_zero, φ.comm₁₂_assoc, IsIso.hom_inv_id_assoc, h₁.wp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv = (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
by
  rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

Tactic:
leftHomologyMap'_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' φ₂ h₁ h₂ + leftHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    leftHomologyMap' φ₂ h₁ h₂
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesColimit K F

Tactic:
let := preservesCoequalizer_of_preservesCokernels F (K.map Limits.WalkingParallelPairHom.left)
        (K.map Limits.WalkingParallelPairHom.right)
    apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

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✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
by
  constructor
  · intro ⟨hS, _⟩
    exact ⟨hS.fIsKernel⟩
  · intro ⟨hS⟩
    exact ⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : WithTerminal J
⊢ g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app j =
    h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app j

Tactic:
cases j with

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (kernel.lift S.g S.f ⋯)

Tactic:
rw [← this]

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
⊢ [Mono f, kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE

Tactic:
tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
⊢ [Mono f, kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ sSup s ≤ f

Tactic:
fapply le_of_comm
  · refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩
    · refine Sigma.desc ?_
      rintro ⟨g, m⟩
      refine underlying.map (homOfLE (k _ ?_))
      simpa using m
    · ext
      dsimp [smallCoproductDesc]
      simp
  · dsimp [sSup]
    rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
F₁ F₂ : C ⥤ H
α₁ : L.LeftExtension F₁
α₂ : L.LeftExtension F₂
e : F₁ ≅ F₂
e' : StructuredArrow.right α₁ ≅ StructuredArrow.right α₂
h : StructuredArrow.hom α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ StructuredArrow.hom α₂
⊢ StructuredArrow.hom ((L.leftExtensionEquivalenceOfIso₂ e).functor.obj α₁) ≫
      ((whiskeringLeft C D H).obj L).map e'.hom =
    StructuredArrow.hom α₂

Tactic:
by simp [leftExtensionEquivalenceOfIso₂, h]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst : Mono f],
    ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
intro A f hf

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } = s.ι.app j

Tactic:
have : F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
        (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) = s.ι :=
      F'.hom_ext_of_isLeftKanExtension α _ _ (by cat_disch)
    exact congr_app this

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f],
    ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
intro A f hf

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)