mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ P) fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
introv R h hQ H

Goal state after:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
⊢ P (algebraMap R S)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝⁵ : Category.{v', u'} J
J' : Type u''
inst✝⁴ : Category.{v'', u''} J'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.Small.{w, v_1, u_1} (P.strictLimitsOfShape J)

Tactic:
refine small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasLimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_
  rintro ⟨_, ⟨F, hF⟩⟩
  exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ m =
    ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
        (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }))

Tactic:
by
    apply BinaryCofan.IsColimit.hom_ext t₂
    · rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.1]
      apply w ⟨0⟩
    · rw [(BinaryCofan.IsColimit.desc' t₂ _ _).2.2]
      apply t₁.uniq ⟨_, _⟩
      rintro ⟨j⟩
      dsimp only [Discrete.natTrans_app]
      rw [← w ⟨j.succ⟩]
      dsimp only [extendCofan_ι_app]
      rw [Fin.cases_succ, assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderLimitsOfShape Jᵒᵖ
⊢ Q.unop.IsClosedUnderColimitsOfShape J

Tactic:
by
  rwa [← isClosedUnderLimitsOfShape_op_iff_unop]

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
inst✝ : BraidedCategory C
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ } =
    (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom

Tactic:
ext; simp [snd_def]; congr

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
n : ℕ
g : M ⟶ N
inst✝ : IsMonHom g
⊢ (f ^ n) ≫ g = (f ≫ g) ^ n

Tactic:
by
  induction n <;> simp [pow_succ, MonObj.mul_comp, *]

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

Goal state before:
pp: C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
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
E✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} E✝
inst✝³ : CartesianMonoidalCategory E✝
G✝ : D ⥤ E✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (pair A B) F
⊢ IsIso (prodComparison F A B)

Tactic:
rw [← prodComparisonIso_hom]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ curry (uncurry ((ihom A).map g)) = curry ((ihom.ev A).app Y ≫ g)

Tactic:
curry_uncurry,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = curry ((ihom.ev A).app Y ≫ g)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = curry (uncurry (𝟙 ((ihom A).obj Y))) ≫ (ihom A).map g

Tactic:
curry_uncurry,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = 𝟙 ((ihom A).obj Y) ≫ (ihom A).map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ curry (uncurry (f ≫ (pre g).app X)) = curry (g ▷ Y ≫ uncurry f)

Tactic:
curry_uncurry,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ f ≫ (pre g).app X = curry (g ▷ Y ≫ uncurry f)
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : DivisionSemiring R
inst✝ : Module R M
f : M →ₗ[R] R
hf : f ≠ 0
z : R
y : M
hy : f y ≠ 0
⊢ f ((z * (f y)⁻¹) • y) = z

Tactic:
simp [hy]

Goal state after:
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 : ι
this : DecidableEq ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i

Tactic:
rw [← coe_dualBasis, linearCombination_dualBasis]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : max ℵ₀ (lift.{v, u} #K) ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
max_le_iff

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Module.rank K (ι → K) = #(ι → K)
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✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank K ↥(p ⊓ K ∙ v) = 0

Tactic:
Submodule.finrank_eq_zero,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ p ⊓ 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
p : ExactPairing X Y
⊢ rightDualIso p p = Iso.refl Y

Tactic:
ext
  simp only [rightDualIso, Iso.refl_hom, @rightAdjointMate_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
simp only [LinearMap.lTensor_tmul, coevaluation_apply_one]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K]
          ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i)) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
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:
by
  simp_rw [isOrthoᵢ_def]
  constructor <;> exact fun h i j hij ↦ h j i hij.symm

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingLeft

Tactic:
refine ⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩
  rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]
  rwa [← separatingLeft_iff_ker_eq_bot]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
y : M
⊢ (B x) y = 0 y

Tactic:
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by
      rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
⊢ (B x) (u + v) = 0 (u + v)
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.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingLeft

Tactic:
intro m hB
  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
  rw [LinearEquiv.map_eq_zero_iff]
  ext i
  rw [Finsupp.zero_apply]
  specialize hB (v i)
  simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂,
           map_smulₛₗ₂] at hB
  rw [Finset.sum_eq_single i] at hB
  · cases smul_eq_zero.mp hB
    · assumption
    · specialize h i
      contradiction
  · intro j _hj hij
    replace hij : B (v j) (v i) = 0 := hO hij
    rw [hij, RingHom.id_apply, smul_zero]
  · intro hi
    replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
    rw [hi, RingHom.id_apply, zero_smul]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
⊢ m = ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)

Tactic:
have : Epi (ofHom f.hom.range.mkQ) :=
      (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)

Goal state after:
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Cofork f 0
m : (cokernelCocone f).pt ⟶ s.pt
h : Cofork.π (cokernelCocone f) ≫ m = s.π
this : Epi (↟(Hom.hom f).range.mkQ)
⊢ m = ↟((Hom.hom f).range.liftQ (Hom.hom s.π) ⋯)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).ker = ⊥

Tactic:
dualPairing_eq

Goal state after:
case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (↑W.quotAnnihilatorEquiv).ker = ⊥
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
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ f' ≫ Arrow.Hom.right e.inv ≫ g = 0

Tactic:
have := Arrow.w e.inv

Goal state after:
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'
this : Arrow.Hom.left e.inv ≫ (Arrow.mk f).hom = (Arrow.mk f').hom ≫ Arrow.Hom.right e.inv
⊢ f' ≫ Arrow.Hom.right e.inv ≫ g = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: 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
⊢ s.ι ≫ biprod.desc f (-g) = 0

Tactic:
KernelFork.condition s

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range
⊢ False

Tactic:
rw [leftCoset_eq_iff, mul_one] at r

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.leftHomologyIso.hom ≫ homologyMap φ = leftHomologyMap φ ≫ S₂.leftHomologyIso.hom

Tactic:
by
  simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using!
    LeftHomologyData.leftHomologyIso_inv_naturality φ S₁.leftHomologyData S₂.leftHomologyData

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
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.opcyclesIso.hom ≫ S.leftHomologyData.f'.op = S.op.fromOpcycles

Tactic:
← cancel_epi S.op.pOpcycles,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.op.pOpcycles ≫ S.leftHomologyData.op.opcyclesIso.hom ≫ S.leftHomologyData.f'.op = S.op.pOpcycles ≫ S.op.fromOpcycles
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 : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)

Tactic:
by
  apply Cofork.IsColimit.hom_ext (hₗ.map F).hπ
  apply Fork.IsLimit.hom_ext (hᵣ.map F).hι
  trans F.map (hₗ.i ≫ hᵣ.p)
  · simp [← Functor.map_comp]
  trans (hₗ.map F).π ≫ ShortComplex.leftRightHomologyComparison'
    (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι
  · rw [ShortComplex.π_leftRightHomologyComparison'_ι]; simp
  · simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ NormalMono i

Tactic:
refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₁.mapCone (KernelFork.ofι i ⋯))

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₂.mapCone (KernelFork.ofι i ⋯))

case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ IsLimit (π₃.mapCone (KernelFork.ofι i ⋯))
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.Full
inst✝ : F.Faithful
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
⊢ ∃ f', f' ≫ g = f

Tactic:
rcases (@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.Full
inst✝ : F.Faithful
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ ∃ f', f' ≫ g = f
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f

Tactic:
rcases hI.factors (F.map f ≫ adj.counit.app _) (F.map g) with ⟨w,h⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ ∃ h, g ≫ h = f
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
A : D
h : j.essImage A
⊢ IsIso ((coreflectorAdjunction j).counit.app A)

Tactic:
rwa [isIso_counit_app_iff_mem_essImage]

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

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
⊢ S.RightHomologyData

Tactic:
have hg' : g' = 𝟙 _ := by simp [g']

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
⊢ S.RightHomologyData
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject X
⊢ (map e.inv).obj ((map e.hom).obj g) = g

Tactic:
← map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject X
⊢ (map (e.hom ≫ e.inv)).obj g = g
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject Y
⊢ (map e.hom).obj ((map e.inv).obj g) = g

Tactic:
← map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject Y
⊢ (map (e.inv ≫ e.hom)).obj g = g
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : S.Exact
⊢ IsColimit (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)

Tactic:
by
  rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
  refine CokernelCofork.IsColimit.ofπ _ _
    (fun u hu => cokernel.desc (kernel.ι S.g) u
      (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
    (by simp) ?_
  intro _ _ _ _ hm
  ext
  rw [hm, cokernel.π_desc]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
⊢ f₁ ⊓ f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

Tactic:
convert! inf_eq_map_pullback' (representative.obj f₁) f₂

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
⊢ min f₁ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
have := preservesEpimorphisms_of_map_exact _ hL

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
this : L.PreservesEpimorphisms
⊢ PreservesColimit (parallelPair f 0) L
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)

Tactic:
obtain ⟨pt, ⟨π⟩⟩ := h F
    exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩

Goal state after: