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

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
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendCyclesIso e hj').hom ≫ K.iCycles j = (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom

Tactic:
rw [← cancel_epi (K.extendCyclesIso e hj').inv, Iso.inv_hom_id_assoc]
  dsimp [extendCyclesIso, iCycles]
  rw [assoc, ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc]
  dsimp
  rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]

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

Goal state before:
pp: case pos
ι : 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'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))

Tactic:
(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff

Goal state after:
case pos
ι : 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'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ IsIso (truncGE.rightHomologyMapData K e hj' ⋯ ⋯ hj).φH
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case neg
ι : 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'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (K.truncGE e).ExactAt i'

pp: case neg
ι : 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'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ K.ExactAt i'

Tactic:
all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

Goal state before:
pp: case left
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Injective (fromSum e₁ e₂)

Tactic:
rintro (i₁ | i₂) (j₁ | j₂) h

Goal state after:
case left.inl.inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inl i₁ = Sum.inl j₁

case left.inl.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inl i₁ = Sum.inr j₂

case left.inr.inl
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ : ι₂
j₁ : ι₁
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inl j₁)
⊢ Sum.inr i₂ = Sum.inl j₁

case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inr i₂ = Sum.inr j₂
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : 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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ IsZero ((K.truncGE e).X i')

Tactic:
· exact (K.truncGE e).isZero_X_of_isStrictlySupported e _ (by simpa using hi'')

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

Goal state before:
pp: case neg
ι : 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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (L.truncGE e).ExactAt i'

pp: case neg.hK
ι : 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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

Goal state after:
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 : CochainComplex C ℤ
n : ℤ
⊢ K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → IsZero (K.X i)

Tactic:
by
  constructor
  · intro _ i hi
    exact K.isZero_of_isStrictlyLE n i hi
  · intro h
    refine IsStrictlySupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntLE_iff] at hi
    exact h i hi

Goal state after:
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (LocalizerMorphism.id W).homMap L₂ L₁ ((LocalizerMorphism.id W).homMap L₁ L₂ f) = f

Tactic:
by
    rw [LocalizerMorphism.homMap_homMap]
    apply LocalizerMorphism.id_homMap

Goal state after:
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y Z : C
g : L₂.obj X ⟶ L₂.obj Y
⊢ (LocalizerMorphism.id W).homMap L₁ L₂ ((LocalizerMorphism.id W).homMap L₂ L₁ g) = g

Tactic:
by
    rw [LocalizerMorphism.homMap_homMap]
    apply LocalizerMorphism.id_homMap

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

Tactic:
apply (SmallHom.equiv W₂ W₂.Q).injective
  simp [Φ.equiv_smallHomMap W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) (CatCommSq.iso _ _ _ _),
    SmallHom.equiv_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α : Ext X Y n
⊢ α.hom + (-α).hom = α.hom + -α.hom

Tactic:
← add_hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α : Ext X Y n
⊢ (α + -α).hom = α.hom + -α.hom
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 φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).hom.app X =
    (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorZero_inv_app, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
  rfl

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₃
⊢ b₁ + b₂ = b₃

Tactic:
by rw [h₁, h₂, h₃, ← h, φ.map_add]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ 𝟙 (G.obj (L.obj (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
⊢ ∀ (x : ι → M), e.toMatrix (c • x) = (RingHom.id R) c • e.toMatrix x

Tactic:
v

Goal state after:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
⊢ e.toMatrix (c • v) = (RingHom.id R) c • e.toMatrix v
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
L M N : C
g : M ⟶ N
hg : Epi g
⊢ Function.Injective ⇑((mk₀ g).precomp L ⋯)

Tactic:
by
  rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]
  intro x hx
  obtain ⟨f, rfl⟩ := Ext.addEquiv₀.symm.surjective x
  simpa [← cancel_epi g] using hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

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
f : R →+* S
g : GL n R
⊢ (map f) g⁻¹ * (map f) g = 1

Tactic:
simp only [map_inv, inv_mul_cancel]

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate

Tactic:
simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_left h

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

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
t : A
h : t ≠ 0
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate

Tactic:
by
  have := Fintype.ofFinite
  rw [nondegenerate_def, nondegenerate_def]
  simp [smul_mulVec, mul_eq_zero_iff_left h]

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 : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x y : TensorAlgebra R M
h : Rel Q x y
⊢ (RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom) x y

Tactic:
induction h

Goal state after:
case of
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 : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x y : TensorAlgebra R M
m✝ : M
⊢ (RingCon.ker ((TensorAlgebra.lift R) ↑f).toRingHom) ((TensorAlgebra.ι R) m✝ * (TensorAlgebra.ι R) m✝)
    ((algebraMap R (TensorAlgebra R M)) (Q m✝))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ ↑(transvection hij b) *ᵥ Pi.single i 1 = Pi.single i 1

Tactic:
rw [transvection_coe]
  simp [-mulVec_single, add_mulVec, single_mulVec_eq, hij]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
| (B (l (Pi.single i 1))) (r (Pi.single j 1))

Tactic:
← LinearMap.sum_repr_mul_repr_mul (Pi.basisFun R n) (Pi.basisFun R m) (l _) (r _)

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
| ((Pi.basisFun R n).repr (l (Pi.single i 1))).sum fun i xi ↦
    ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
      xi •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f (x + y)) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y

Tactic:
simp_rw [f.map_add]; exact h (f x) (f y)

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
⊢ 2 • (associatedHom S) Q = Q.polarBilin

Tactic:
ext
  dsimp [associated_apply]
  rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
    polar]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = ↑r * ↑(r' j)

Tactic:
by
  classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    simp_rw [DFinsupp.sum, H, Finset.sum_ite_eq']
    split_ifs with h
    · rfl
    rw [DFinsupp.notMem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Function.Injective ⇑(Hom.hom S.f)

Tactic:
← mono_iff_injective

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Mono S.f
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ (⇑(ExteriorAlgebra.ι R) '' s) ^ n ⊆ ↑(span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}))

Tactic:
rintro x hx

Goal state after:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
x : ExteriorAlgebra R M
hx : x ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ x ∈ ↑(span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
← ιMulti_span_fixedDegree_of_span_eq_top R n M hv,

Goal state after:
case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ Submodule.span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | Set.range a ⊆ Set.range v}) ≤
    Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))
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)
X : Cᵒᵖ
j : J
⊢ (F.obj j).map (𝟙 X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv

Tactic:
ModuleCat.restrictScalarsId'App_inv_naturality,

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)
X : Cᵒᵖ
j : J
⊢ (F.obj j).map (𝟙 X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ ((F.obj j).obj X)).inv ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom (μ (restrictScalars f) M₁ M₂)) (m₁ ⊗ₜ[R] m₂) = m₁ ⊗ₜ[S] m₂

Tactic:
dsimp [Adjunction.rightAdjointLaxMonoidal_μ]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom
        (((extendRestrictScalarsAdj f).homEquiv ((restrictScalars f).obj M₁ ⊗ (restrictScalars f).obj M₂) (M₁ ⊗ M₂))
          (δ (extendScalars f) ((restrictScalars f).obj M₁) ((restrictScalars f).obj M₂) ≫
            ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂))))
      (m₁ ⊗ₜ[R] m₂) =
    m₁ ⊗ₜ[S] m₂
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)
⊢ IsFiltered (StructuredArrow d F)

Tactic:
suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk

Goal state after:
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)
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ (ObjectProperty.ι fun x ↦ x ∈ s).Initial

Tactic:
refine Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
i : J
⊢ ∃ c, Nonempty ((ObjectProperty.ι fun x ↦ x ∈ s).obj c ⟶ i)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
ext X m

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
X : Cᵒᵖ
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (g₁.app X)) m = (ModuleCat.Hom.hom (g₂.app X)) m