mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
⊢ e.BoundaryGE j → ∀ (i' : ι'), c'.Rel i' (e.f j) → K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0

Tactic:
hj

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
⊢ ∀ (i' : ι'), c'.Rel i' (e.f j) → K.d i' (e.f j) ≫ (e.homRestrict ψ).f j = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Injective (K.X i)
i' : ι'
⊢ Injective ((K.extend e).X i')

Tactic:
by
  by_cases! hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    exact Injective.of_iso (K.extendXIso e hi).symm inferInstance
  · exact (isZero_extend_X K e i' hi').injective

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.restriction e).pOpcycles j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom =
    (K.restrictionXIso e hj').hom ≫ K.pOpcycles j'

Tactic:
by
  simp [restrictionOpcyclesIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.pOpcycles j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv =
    (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j

Tactic:
by
  simp [restrictionOpcyclesIso]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
⊢ e.BoundaryGE j → ∀ (i' : ι'), c'.Rel i' (e.f j) → K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0

Tactic:
hj

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : e.BoundaryGE j
⊢ ∀ (i' : ι'), c'.Rel i' (e.f j) → K.d i' (e.f j) ≫ (K.restrictionToTruncGE' e).f j = 0
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsStrictlyLE n
⊢ IsIso (K.ιTruncLE n)

Tactic:
dsimp [ιTruncLE]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
h : (embeddingUpIntLE n).BoundaryLE (n - i).natAbs
⊢ False

Tactic:
rw [boundaryLE_embeddingUpIntLE_iff, Int.natAbs_eq_zero] at h

Goal state after:
C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
h : n - i = 0
⊢ False
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
⊢ Functor.Linear R L

Tactic:
by
  let := linear R L W
  constructor
  intro X Y f r
  change L.map (r • f) = ((Linear.toCatCenter R C r).localization L W).app (L.obj X) ≫ L.map f
  simp [← L.map_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
      X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.Exact

Tactic:
by
  let := HasDerivedCategory.standard C
  have := (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₃ _
    (hS.singleTriangle_distinguished) n₀ n₁ (by lia)
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)
  · ext x; apply hom_comp_singleFunctor_map_shift (C := C)
  · ext x
    exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
x : M
⊢ f x = f' x

Tactic:
obtain ⟨y, rfl⟩ := h.bijective.2 x

Goal state after:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
y : relations.Quotient
⊢ f (solution.fromQuotient y) = f' (solution.fromQuotient y)
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
by
  refine forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩ <;>
  convert! hw

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)

Tactic:
by
  ext
  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inr
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : Nonempty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

Tactic:
det_eq_elem_of_subsingleton _ i

Goal state after:
case inr
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA✝ : A.det = 1
B : Matrix n n R
hB✝ : B.det = 1
i : n
hB : B i i = 1
hA : A i i = 1
j : n
hn : Nonempty n
⊢ ↑⟨A, hA✝⟩ i j = ↑⟨B, hB✝⟩ i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ ((scalar n) (↑↑A i i) * ↑↑B) i i = (scalar n) (↑↑A i i) i i * ↑↑B i i

Tactic:
← scalar_eq_coe_self_center B i

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ ((scalar n) (↑↑A i i) * (scalar n) (↑↑B i i)) i i = (scalar n) (↑↑A i i) i i * (scalar n) (↑↑B i i) i i
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ((((fun f ↦ (ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((fun F ↦ ⟨F.toLinearMap ∘ₗ ι Q, ⋯⟩) F)).comp
            (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x =
    ((F.comp (RingCon.mkₐ R (ringCon Q))).toLinearMap ∘ₗ TensorAlgebra.ι R) x

Tactic:
by
          dsimp
          exact (RingCon.liftₐ_mk _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ _)

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b ↦ ((toAddMonoid fun x_1 ↦ ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip b) a') = fun ai ↦
    DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
simp [AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.toAddMonoid]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ x ∈ p

Tactic:
rw [← DirectSum.sum_support_decompose ℳ x]

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) x), ↑(((decompose ℳ) x) i) ∈ p
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ℳ : ι → Submodule R M
inst✝² : Decomposition ℳ
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
i : ι
⊢ f ∘ₗ ↑(decomposeLinearEquiv ℳ).symm ∘ₗ lof R ι (fun i ↦ ↥(ℳ i)) i =
    g ∘ₗ ↑(decomposeLinearEquiv ℳ).symm ∘ₗ lof R ι (fun i ↦ ↥(ℳ i)) i

Tactic:
decomposeLinearEquiv_symm_comp_lof ℳ i,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ℳ : ι → Submodule R M
inst✝² : Decomposition ℳ
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
i : ι
⊢ f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
⊢ B.toQuadraticMap.IsOrtho x y ↔ (B x) y = 0

Tactic:
by
  let : AddCancelMonoid R := { ‹IsCancelAdd R›, (inferInstance : AddCommMonoid R) with }
  simp_rw [isOrtho_def, B.toQuadraticMap_apply, map_add,
    LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)]
  rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (x y : N i),
    ((g fun i_1 ↦ update m i (x + y) (Sum.inl i_1)) fun i' ↦ update m i (x + y) (Sum.inr i')) =
      ((g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')) +
        (g fun i_1 ↦ update m i y (Sum.inl i_1)) fun i' ↦ update m i y (Sum.inr i')

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

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (c : R) (x : N i),
    ((g fun i_1 ↦ update m i (c • x) (Sum.inl i_1)) fun i' ↦ update m i (c • x) (Sum.inr i')) =
      c • (g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')

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

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x = 0

Tactic:
rw [← x.comp_mk₀_id, ← h.retract, ← Ext.mk₀_comp_mk₀, ← Ext.comp_assoc_of_second_deg_zero,
    (x.comp (Ext.mk₀ h.i) (add_zero i)).eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext Y X i
⊢ e = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext Y X (n + k)
⊢ e = 0
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ (cn.sum fun a b ↦ b • (Hom.hom S.f) (v a)) + m' ∈ span R (range u)

Tactic:
rw [hn']

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ (cn.sum fun a b ↦ b • u (Sum.inl a)) + m' ∈ span R (range u)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this✝ : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this : PreservesColimits (tensorLeft F) :=
  { preservesColimitsOfShape := @instMonoidalClosedFunctorType._proof_2 C inst✝ F }
⊢ Closed F

Tactic:
have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)

Goal state after:
C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this✝¹ : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
this✝ : PreservesColimits (tensorLeft F) :=
  { preservesColimitsOfShape := @instMonoidalClosedFunctorType._proof_2 C inst✝ F }
this : (tensorLeft F).IsLeftAdjoint
⊢ Closed F
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
⊢ IsColimit (G.flip.mapCocone₂ c₁ c₂)

Tactic:
refine IsColimit.precomposeInvEquiv E₁ _ ?_

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
⊢ IsColimit ((Cocone.precompose E₁.inv).obj (G.flip.mapCocone₂ c₁ c₂))
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'

Tactic:
· intro h
    constructor
    · intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩
    · intro _ c _ _
      exact ⟨ c, 𝟙 _, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g))

Tactic:
Equiv.apply_symm_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    c.ι.app j ≫ g
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ (R.map φ).hom ≫ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) = c.ι.app j ≫ g

Tactic:
Equiv.apply_symm_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ (R.map φ).hom ≫ c.ι.app j' ≫ g = c.ι.app j ≫ g