mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)

Tactic:
NatTrans.id_app,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    𝟙 (((singleFunctors C).functor 0).obj S.X₃) ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ h₁.extClass.comp (Ext.mk₀ f.τ₁) ⋯ = (Ext.mk₀ f.τ₃).comp h₂.extClass ⋯

Tactic:
let := HasDerivedCategory.standard C
  ext
  simpa [ShiftedHom.comp_mk₀, ShiftedHom.mk₀_comp] using! (singleTriangle.map h₁ h₂ f).comm₃

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ 0)).hom.app x✝ ≫ (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app (F.obj x✝) =
    (CommShift.isoZero (PullbackShift.functor φ F) A).hom.app x✝

Tactic:
simp only [F.commShiftIso_zero' (A := B) (φ 0) (by rw [map_zero]), CommShift.isoZero'_hom_app,
      assoc, CommShift.isoZero_hom_app, pullbackShiftFunctorZero'_hom_app, map_comp,
      pullbackShiftFunctorZero'_inv_app]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorZero' (PullbackShift C φ) (φ 0) ⋯).hom.app x✝) ≫
        (shiftFunctorZero' (PullbackShift D φ) (φ 0) ⋯).inv.app (F.obj x✝) ≫
          (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app (F.obj x✝) =
    (PullbackShift.functor φ F).map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      (PullbackShift.functor φ F).map ((shiftFunctorZero' C (φ 0) ⋯).hom.app x✝) ≫
        (shiftFunctorZero' D (φ 0) ⋯).inv.app ((PullbackShift.functor φ F).obj x✝) ≫
          (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app ((PullbackShift.functor φ F).obj x✝)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X =
    (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
      (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
by
  rw [← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,
    assoc, assoc, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app]
  erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]
  rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]

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

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        G.map (f₁.hom.app ((shiftFunctor C a).obj X)) ≫
          f₂.hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫ (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))

Tactic:
rw [← reassoc_of% this, ← cancel_mono ((shiftFunctorAdd C a b).hom.app _),
    assoc, assoc, assoc, assoc, assoc, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C a ⋙ shiftFunctor C b).obj (G.obj (F.obj X)))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (opEquiv c).symm (f.comp g h) = ((opEquiv b).symm g).comp ((opEquiv a).symm f) ⋯

Tactic:
by
  rw [opEquiv_symm_apply, opEquiv_symm_apply,
    opShiftFunctorEquivalence_add_unitIso_inv_app_eq _ _ _ _ (show a + b = c by lia), comp, comp]
  dsimp
  rw [assoc, assoc, assoc, assoc, ← Functor.map_comp, ← unop_comp_assoc,
    Iso.inv_hom_id_app]
  dsimp
  rw [assoc, id_comp, Functor.map_comp, ← NatTrans.naturality_assoc,
    ← NatTrans.naturality, opEquiv_symm_apply]
  dsimp
  rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc,
    ← Functor.map_comp_assoc]
  rw [← unop_comp_assoc]
  erw [← NatTrans.naturality]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z • e.hom) ≫ (↑z⁻¹ • e.inv) = 𝟙 X

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ (↑z⁻¹ • e.inv) ≫ (↑z • e.hom) = 𝟙 Y

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]
        simp

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_1.hy
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := ⋯
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ 1 ∈ Set.range ⇑f.toHomUnits

Tactic:
· exact ⟨1, f.toHomUnits.map_one⟩

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
⊢ val '' ↑(rootsOfUnity k R) = {z | z ^ k = 1}

Tactic:
ext x
  exact ⟨fun ⟨y,hy1,hy2⟩ => by rw [← hy2]; exact (mem_rootsOfUnity' k y).mp hy1,
    fun h ↦ ⟨(rootsOfUnity.mkOfPowEq x h), ⟨Subtype.coe_prop (rootsOfUnity.mkOfPowEq x h), rfl⟩⟩⟩

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi ↦ (b₂'.repr y).sum fun j yj ↦ xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y

Tactic:
conv_rhs => rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]
  simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smul₂, map_smul]

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
by
  obtain ⟨r : R, hr : scalar n r = A⟩ := mem_range_scalar_of_commute_transvectionStruct fun t ↦
    Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩
  simp [← congr_fun₂ hr i i, ← hr]

Goal state after:
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 b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * (ι Q) b + (ι Q) b * (ι Q) a = 0

Tactic:
by
  rw [ι_mul_ι_add_swap, h.polar_eq_zero]
  simp

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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
mulHom_of_of

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) ((of A i) xi)) ((of A 0) GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
mulHom_of_of

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ (of A (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ (of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = ((mulHom A) ((of A bi) bx)) ((of A ai) ax)

Tactic:
mulHom_of_of

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ (of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = (of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ (toLinearMap₂ b₂ b₂) J' ∘ₗ (toLin b₁ b₂) A = ((toLinearMap₂ b₁ b₁) J).compl₂ ((toLin b₂ b₁) A') ↔
    J.IsAdjointPair J' A A'

Tactic:
simp_rw [h, LinearMap.toMatrix₂_comp b₂ b₂, LinearMap.toMatrix₂_compl₂ b₁ b₁,
    LinearMap.toMatrix_toLin, LinearMap.toMatrix₂_toLinearMap₂]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ Aᵀ * J' = J * A' ↔ J.IsAdjointPair J' A A'
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
⊢ (((associatedHom R) Q) (w j • v j)) (w j • v j) = (((associatedHom R) Q) (v j)) (v j) • (w j * w j)

Tactic:
rw [map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul,
      smul_eq_mul, Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]

Goal state after:
ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
⊢ w j * (w j * ⅟2 • (Q (v j + v j) - Q (v j) - Q (v j))) = ⅟2 • (Q (v j + v j) - Q (v j) - Q (v j)) * (w j * w j)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ y✝ : CliffordAlgebra 0
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
hy :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) y✝ = g ((liftAlternating f) y✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) (x✝ + y✝) = g ((liftAlternating f) (x✝ + y✝))

Tactic:
rw [map_add, map_add, map_add, hx, hy]

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 : C
⊢ Injective X ↔ HasInjectiveDimensionLT X 1

Tactic:
let := HasExt.standard C
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ injective_iff_subsingleton_ext_one.2
    (HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

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

Goal state before:
pp: case h
ι : 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₂ := ⋯
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)
⊢ ((Finsupp.mapDomain Sum.inl cn).sum fun i a ↦ a • u i) = cn.sum fun a b ↦ b • u (Sum.inl a)

Tactic:
Finsupp.sum_mapDomain_index_inj Sum.inl_injective

Goal state after:
case h
ι : 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)) = cn.sum fun a b ↦ b • u (Sum.inl a)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
n : ℕ
hn : ↑n = ⊤
⊢ False

Tactic:
exact ENat.natCast_ne_top _ ((WithBot.coe_eq_coe).1 hn)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ f r * 1 = f r

Tactic:
mul_one

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ f r = f r
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ snd A I ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)

Tactic:
by
    have : snd A I = uncurry (t.to _) := by
      rw [← curry_eq_iff]
      apply t.hom_ext
    rw [this, ← uncurry_natural_right, ← eq_curry_iff]
    apply t.hom_ext

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R f)) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv

Tactic:
colimit.ι_desc_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    ((Cocone.precompose (F.whiskerLeft (restriction R f))).obj
              (colimit.cocone (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))).ι.app
        j ≫
      (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
⊢ IsFilteredOrEmpty (StructuredArrow d F)

Tactic:
refine ⟨fun f g => ?_, fun f g η μ => ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ Z x x, True

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ (freeYoneda R).IsSeparating

Tactic:
intro M

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ ∀ ⦃Y : PresheafOfModules R⦄ (f g : M ⟶ Y),
    (∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f = h ≫ g) → f = g
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
⊢ colimit G ≅ colimit (curry.obj G ⋙ colim)

Tactic:
haveI : Limits.HasColimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasColimit_of_iso i.symm

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasColimit (uncurry.obj (curry.obj G))
⊢ colimit G ≅ colimit (curry.obj G ⋙ colim)