mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
Y' : C
r : Y' ⟶ Y
t : (Triangle.mk g s h).obj₁ ⟶ (shiftFunctor C 1).obj Y'
mem' : Triangle.mk r q t ∈ distinguishedTriangles
⊢ r ≫ f₁ = r ≫ f₂

Tactic:
· have eq := comp_distTriang_mor_zero₁₂ _ mem'
      dsimp at eq
      rw [← sub_eq_zero, ← comp_sub, hq, reassoc_of% eq, zero_comp]

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

Goal state before:
pp: case inr.inl
ι : 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
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') = 0

pp: case inr.inr
ι : 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
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
· rw [extend.d_none_eq_zero' K _ _ hj']

Goal state after:
case inr.inr
ι : 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
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
by_cases hij : c.Rel i j
  · obtain rfl := c.next_eq' hij
    exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv
  · rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]

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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsGE n
⊢ QuasiIso (K.πTruncGE n)

Tactic:
by
  rw [quasiIso_πTruncGE_iff]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (equiv W W.Q) ((mk W f).comp (mk W g)) = (equiv W W.Q) (mk W (f ≫ g))

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y Y
α : SmallHom W X Y
⊢ (equiv W W.Q) (α.comp (mk W (𝟙 Y))) = (equiv W W.Q) α

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X X
α : SmallHom W X Y
⊢ (equiv W W.Q) ((mk W (𝟙 X)).comp α) = (equiv W W.Q) α

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y X
inst✝ : HasSmallLocalizedHom W Y Y
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk W f).comp (mkInv f hf)) = (equiv W W.Q) (mk W (𝟙 Y))

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝² : HasSmallLocalizedHom W X X
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y X
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mkInv f hf).comp (mk W f)) = (equiv W W.Q) (mk W (𝟙 X))

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y Y
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk₀ W m₀ hm₀ f).comp (mk₀Inv m₀ hm₀ f hf) ⋯) = (equiv W W.Q) (mk₀ W m₀ hm₀ (𝟙 Y))

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M X X
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk₀Inv m₀ hm₀ f hf).comp (mk₀ W m₀ hm₀ f) ⋯) = (equiv W W.Q) (mk₀ W m₀ hm₀ (𝟙 X))

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
X Y : C
inst✝² : HasSmallLocalizedShiftedHom W M X Y
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ (equiv W W.Q) (α.comp (mk₀ W m₀ hm₀ (𝟙 Y)) ⋯) = (equiv W W.Q) α

Tactic:
by simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
W : MorphismProperty C
M : Type w'
inst✝⁵ : AddMonoid M
inst✝⁴ : HasShift C M
X Y : C
inst✝³ : HasSmallLocalizedShiftedHom W M X Y
inst✝² : HasSmallLocalizedShiftedHom W M X X
inst✝¹ : HasSmallLocalizedShiftedHom W M Y Y
inst✝ : W.IsCompatibleWithShift M
m : M
α : SmallShiftedHom W X Y m
m₀ : M
hm₀ : m₀ = 0
⊢ (equiv W W.Q) ((mk₀ W m₀ hm₀ (𝟙 X)).comp α ⋯) = (equiv W W.Q) α

Tactic:
by simp [equiv_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃

Tactic:
simp [singleδ, e, ← Functor.map_comp, CochainComplex.singleFunctors]

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

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
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
F : C ⥤ D
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (OppositeShift C A)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoId C A).hom (shiftFunctor (OppositeShift C A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoId C A).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x✝).hom

Tactic:
by
    ext
    dsimp [OppositeShift.natIsoId, Functor.commShiftOp_iso_eq]
    simp only [Functor.commShiftIso_id_hom_app, Functor.map_id,
      comp_id, Functor.commShiftIso_id_inv_app, CategoryTheory.op_id, id_comp]
    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₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
      (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
        (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
          (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X),

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₃
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).inv.app X ≫
      (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X =
    (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).inv.app X ≫
      (pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
        (shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X ≫
          (pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X) ≫
            (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)
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
⊢ f = f'

Tactic:
by
    ext x
    obtain ⟨y, rfl⟩ := h.bijective.2 x
    exact DFunLike.congr_fun this y

Goal state after:
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.Nondegenerate ↔ (∀ (v : m → R), v ᵥ* M = 0 → v = 0) ∧ ∀ (v : n → R), M *ᵥ v = 0 → v = 0

Tactic:
by
  rw [nondegenerate_iff, separatingLeft_iff_forall_vecMul_eq_zero,
    separatingRight_iff_forall_mulVec_eq_zero]

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) y

Tactic:
← b₂.linearCombination_repr y

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) ((Finsupp.linearCombination S ⇑b₂) (b₂.repr y))
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) * (x * y) - x * (ι Q) b * ((ι Q) a * y) =
    -(x * (ι Q) b * ((ι Q) a * y))

Tactic:
h.polar_eq_zero,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) 0 * (x * y) - x * (ι Q) b * ((ι Q) a * y) = -(x * (ι Q) b * ((ι Q) a * y))
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 : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Submodule.map ((lift Q) ⟨f, cond⟩).toLinearMap (ι Q).range = f.range

Tactic:
← LinearMap.range_comp,

Goal state after:
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 : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ (((lift Q) ⟨f, cond⟩).toLinearMap ∘ₗ ι Q).range = f.range
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
Q : QuadraticMap R N' N
f : M →ₗ[R] N'
x y : M
⊢ ((Q.comp f).polarBilin x) y = ((compl₁₂ Q.polarBilin f f) x) y

Tactic:
simp [polar]

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✝¹⁰ : AddCommGroup N
inst✝⁹ : Module R M
inst✝⁸ : Module R N
N' : Type u_8
inst✝⁷ : AddCommGroup N'
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra S R
inst✝⁴ : Module S N
inst✝³ : Module S N'
inst✝² : IsScalarTower S R N
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
f : N →ₗ[S] N'
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑(f.compQuadraticMap' Q)) x y = f (polar (⇑Q) x y)

Tactic:
simp [polar]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule (-J) J ↔ J.IsSkewAdjoint A₁

Tactic:
mem_pairSelfAdjointMatricesSubmodule

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ ↑(MulOpposite.opLinearEquiv R)) (ι Q).range = (ι Q).range

Tactic:
exact Submodule.map_id _

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case mem.mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
⊢ P (x * m)

Tactic:
obtain ⟨m, rfl⟩ := hm

Goal state after:
case mem.mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ (ι Q).range ^ _i
px : P x
m : M
⊢ P (x * (ι Q) m)
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
⊢ basisRepr Q v = weightedSumSquares R fun i ↦ Q (v i)

Tactic:
ext w

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
⊢ (basisRepr Q v) w = (weightedSumSquares R fun i ↦ Q (v i)) w
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case zero
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
i : Fin 0
⊢ (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
exact i.elim0

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Submodule.span R (Set.range ⇑(ιMulti R n)) = ⋀[R]^n M

Tactic:
refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range ⇑(ιMulti R n))
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

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

Tactic:
obtain _ | i := i

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
hi : 1 ≤ 0
e : Ext Y X 0
⊢ e = 0

case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext Y X (i + 1)
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
⊢ HasInjectiveDimensionLT S.X₂ n

Tactic:
by
  let := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y x₂
  obtain ⟨x₃, rfl⟩ := Ext.covariant_sequence_exact₂ _ hS x₂
    (Ext.eq_zero_of_hasInjectiveDimensionLT _ n hi)
  rw [x₃.eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

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

Goal state before:
pp: case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasInjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑0

Tactic:
exact ⟨⊥, fun _ _ ↦ hasInjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
⊢ ⇑(map n f) ∘ ιMulti_family R n v = ιMulti_family R n (⇑f ∘ v)

Tactic:
ext ⟨s, hs⟩

Goal state after:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s ∈ powersetCard I n
⊢ ↑((⇑(map n f) ∘ ιMulti_family R n v) ⟨s, hs⟩) = ↑(ιMulti_family R n (⇑f ∘ v) ⟨s, hs⟩)
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M : ModuleCat R
S : Submonoid R
⊢ IsLocalizedModule S (M.localizedModuleMkLinearMap S)

Tactic:
by
  dsimp only [localizedModuleMkLinearMap]
  infer_instance

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
⊢ (ConcreteCategory.hom
        (((extendRestrictScalarsAdj f).homEquiv (𝟙_ (ModuleCat R)) (𝟙_ (ModuleCat S))) (η (extendScalars f))))
      r =
    f r

Tactic:
rw [extendRestrictScalarsAdj_homEquiv_apply, extendScalars_η]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ (ConcreteCategory.hom (↟↑(AlgebraTensorModule.rid R S S))) (1 ⊗ₜ[R] r) = f r
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ s ≫ IsFiltered.coeqHom s s' = s' ≫ IsFiltered.coeqHom s s'

Tactic:
rw [IsFiltered.coeq_condition]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: 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
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
let s₂ : D ≌ AsSmall.{max u₁ v₁ u₂ v₂} D := AsSmall.equiv

Goal state after:
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
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
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
X : C × C
⊢ IsFiltered (StructuredArrow X (Functor.diag C))

Tactic:
by
  have : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) := by
    rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
    infer_instance
  apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _

Goal state after: