mathlib-initiative/mathlib-tactics huggingface dataset:
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
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
← finrank_eq_rank

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
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
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
⊢ finrank K (V ⧸ q) = finrank K ↥p

Tactic:
← add_right_cancel_iff,

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
⊢ finrank K (V ⧸ q) + ?m.63 = finrank K ↥p + ?m.63

K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p q : Subspace K V
f : (V ⧸ p) ≃ₗ[K] ↥q
⊢ ℕ
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
f : End K V
m : ℕ
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
by
  by_cases! h_cases : m < finrank K V
  · rw [← add_tsub_cancel_of_le h_cases.le, add_comm, pow_add]
    apply LinearMap.ker_le_ker_comp
  · rw [ker_pow_eq_ker_pow_finrank_of_le h_cases]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (𝟙_ C ⊗ X) ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C) =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ i.hom ⊗≫ (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y) ⊗≫ i.inv ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
rw [← whisker_exchange, ← whisker_exchange]; monoidal

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))
      (∑ x,
        (TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
          ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K]
            ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
simp only [assoc_symm_tmul]

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))
      (∑ x,
        (Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x ⊗ₜ[K]
          (Basis.ofVectorSpace K V).coord x) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cone F) (j : WalkingParallelPair),
    pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯ ≫ (equalizerCone F).π.app j =
      s.π.app j

Tactic:
rintro c (_ | _) <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor (RingHom.id R) M P Q

Tactic:
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)

Goal state after:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor (RingHom.id R) M P Q
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

Tactic:
exact c.π.app WalkingParallelPair.zero

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

Tactic:
exact c.π.app WalkingParallelPair.zero

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
⊢ x ∈ ↑B.ker

Tactic:
ext y

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
y : M
⊢ (B x) y = 0 y
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
⊢ x = 0

Tactic:
replace hx' : x ∈ W ⊓ ker B := by
    refine ⟨hx, ?_⟩
    ext y
    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
    suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
    exact hx' u hu

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' : x ∈ W ⊓ B.ker
⊢ x = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cocone F) (j : WalkingParallelPair),
    (coequalizerCocone F).ι.app j ≫ pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯ =
      s.ι.app j

Tactic:
rintro c (_ | _) <;> simp

Goal state after:
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)
i : IsIso (coequalizerComparison f g G)
⊢ PreservesColimit (parallelPair f g) G

Tactic:
by
  apply preservesColimit_of_preserves_colimit_cocone (coequalizerIsCoequalizer f g)
  apply (isColimitMapCoconeCoforkEquiv _ _).symm _
  exact
    @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (parallelPair (G.map f) (G.map g))) i

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
h : (B x) x = 0
⊢ B x = 0

Tactic:
ext y

Goal state after:
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
h : (B x) x = 0
y : M
⊢ (B x) y = 0 y
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
rw [← dualMap_injective_iff]; exact (evalEquiv K V₂).toEquiv.injective_comp B.dualMap

Goal state after:
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 Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ (kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯ ≫ b') ≫ b = s.snd ≫ b

Tactic:
rw [KernelFork.ι_ofι] at hb'

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 Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ b = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ (kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯ ≫ b') ≫ b = s.snd ≫ b
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
hf : S.f = 0
⊢ IsIso h.π

Tactic:
have ⟨φ, hφ⟩ := CokernelCofork.IsColimit.desc' h.hπ' (𝟙 _)
    (by rw [← cancel_mono h.i, comp_id, f'_i, zero_comp, hf])
  dsimp at hφ
  exact ⟨φ, hφ, by rw [← cancel_epi h.π, reassoc_of% hφ, comp_id]⟩

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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0

Tactic:
← cancel_mono (ofIsLimitKernelFork S hf c hc).i,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).f' ≫ (ofIsLimitKernelFork S hf c hc).i = 0 ≫ (ofIsLimitKernelFork S hf c hc).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 : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.cyclesIso.inv = S.op.toCycles

Tactic:
← cancel_mono S.op.iCycles,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ (S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.cyclesIso.inv) ≫ S.op.iCycles = S.op.toCycles ≫ S.op.iCycles
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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫
      ↾fun z ↦
        if h : z ∈ Set.range ⇑(ConcreteCategory.hom f) then (ConcreteCategory.hom g) (Classical.choose h) else ⋯.some) =
    g

Tactic:
ext y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
⊢ (ConcreteCategory.hom
          (f ≫
            ↾fun z ↦
              if h : z ∈ Set.range ⇑(ConcreteCategory.hom f) then (ConcreteCategory.hom g) (Classical.choose h)
              else ⋯.some)).toFun
      y =
    (ConcreteCategory.hom g).toFun y
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ Mono S.g

Tactic:
simp only [exact_iff_isZero_homology] at h

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this : S.HasHomology
h : IsZero S.homology
⊢ Mono S.g
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
h : S.Exact
this : S.HasHomology
⊢ Epi S.f

Tactic:
simp only [exact_iff_isZero_homology] at h

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
this : S.HasHomology
h : IsZero S.homology
⊢ Epi S.f
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ g.unop = 0

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.lift g.unop (kernel.ι f.unop) ?refine_1 ≫ kernel.ι g.unop = kernel.ι f.unop

Tactic:
· rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.lift g.unop (kernel.ι f.unop) ⋯ ≫ kernel.ι g.unop = kernel.ι f.unop
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
⊢ (f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h)

Tactic:
intro k₁

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
⊢ (g ⟶ h) → ((sup.obj f).obj g ⟶ h)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : Balanced C
f : X ⟶ Y
inst✝ : Mono f
⊢ Epi f ↔ IsIso f

Tactic:
exact ⟨fun _ ↦ isIso_of_mono_of_epi f, fun _ ↦ inferInstance⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
i : I
m : i ∈ s
⊢ (P i).Factors (s.inf P).arrow

Tactic:
revert i m
  induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
⊢ L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
revert Y₁ Y₂ e

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseLeftKanExtensionAt F Y₁ ↔ L.HasPointwiseLeftKanExtensionAt F Y₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
⊢ L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
revert Y₁ Y₂ e

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
⊢ ∀ {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂), L.HasPointwiseRightKanExtensionAt F Y₁ ↔ L.HasPointwiseRightKanExtensionAt F Y₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))

Tactic:
have : Nonempty (StructuredArrow d (sequentialFunctor J)) :=
      ⟨StructuredArrow.mk (homOfLE g)⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))

Tactic:
obtain ⟨n, (g : d ≤ (sequentialFunctor J).obj n)⟩ := sequentialFunctor_final_aux J d
    have : Nonempty (StructuredArrow d (sequentialFunctor J)) :=
      ⟨StructuredArrow.mk (homOfLE g)⟩
    apply isConnected_of_zigzag
    refine fun i j ↦ ⟨[j], ?_⟩
    simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]
    clear! C
    wlog! h : j.right ≤ i.right
    · exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))
    · right
      exact ⟨StructuredArrow.homMk (homOfLE h) rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.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
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
⊢ PreservesColimit H lim

Tactic:
have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
    have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
    let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
      isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
        (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
        isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ lim.leftUnitor
    exact preservesColimit_of_natIso _ e

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ Subobject (op A) → Subobject (op A.left)

Tactic:
refine Subobject.lift (fun P f hf => Subobject.mk f.unop.left.op) ?_
  intro P Q f g hf hg i hi
  refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj ?_)
  have := congr_arg Quiver.Hom.unop hi
  simpa using! congr_arg CommaMorphism.left this

Goal state after: