mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (Functor.commShiftIso F a).hom.app X✝ ≫
      (shiftFunctor D a).map (F.map (adj.unit.app X✝)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝

Tactic:
← Functor.map_comp,

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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (Functor.commShiftIso F a).hom.app X✝ ≫ (shiftFunctor D a).map (F.map (adj.unit.app X✝) ≫ adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₁).mor₃.op ≫ (shiftFunctor Cᵒᵖ 1).map φ.unop.hom₃.op =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map ((Opposite.unop T₁).mor₃.op ≫ φ.unop.hom₃.op) =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map φ.hom₃.unop).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map (T₂.mor₃.unop ≫ φ.hom₃.unop)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles

Tactic:
exact Pretriangulated.isomorphic_distinguished _ hT₁ _
    ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ T.mor₃ ≫
      (shiftFunctor Cᵒᵖ 1).map ((opShiftFunctorEquivalence C 1).unitIso.hom.app T.obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map ((opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁) =
    T.mor₃

Tactic:
← Functor.map_comp,

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ T.mor₃ ≫
      (shiftFunctor Cᵒᵖ 1).map
        ((opShiftFunctorEquivalence C 1).unitIso.hom.app T.obj₁ ≫
          (opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁) =
    T.mor₃
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 (hS.extClass.postcomp X h),
      g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), 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
    exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h
  · ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫
      (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I).hom ≫ opcyclesMap ι i

Tactic:
← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    ((single C (ComplexShape.up ℤ) i).obj I).pOpcycles i ≫
      (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I).inv ≫
        (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I).hom ≫ opcyclesMap ι i
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, ∑ x_1, w x • A x x_1 • v x_1 = 0
⊢ w = 0

Tactic:
← smul_assoc

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, ∑ x_1, (w x • A x x_1) • v x_1 = 0
⊢ w = 0
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
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
by
  have := contravariant_sequence_exact₂' hS Y n
  rw [ShortComplex.ab_exact_iff] at this
  exact this x₂ hx₂

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 : Matrix n n A
inst✝ : DecidableEq n
⊢ M.SeparatingLeft ↔ M.det ≠ 0

Tactic:
by
  grind [separatingLeft_iff_forall_vecMul_eq_zero, exists_vecMul_eq_zero_iff]

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
this : (α : Type ?u.44) → [Finite α] → Fintype α
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate

Tactic:
rw [nondegenerate_def, nondegenerate_def]

Goal state after:
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
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case neg
n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
· exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
⊢ Q₃ (g (f x)) = Q₁ x

Tactic:
← f.map_app,

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₂ →qᵢ Q₃
f : Q₁ →qᵢ Q₂
x : M₁
⊢ Q₃ (g (f x)) = Q₂ (f x)
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₁ m

Tactic:
← f.map_app,

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₂ (f m)
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
hn : IsEmpty n
⊢ ↥⊥ ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

Tactic:
Fintype.card_eq_zero,

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
hn : IsEmpty n
⊢ ↥⊥ ≃* ↥(rootsOfUnity (max 0 1) R)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ SpecialLinearGroup.transvection h c ∈ commutator SL(2, F)

Tactic:
exact transvection_mem_commutator₁ ha hasq c

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

Goal state before:
pp: case cons
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        (((if ¬True then polarSym2 (⇑Q) (Sym2.map f s(a, a)) else 0) +
            ∑ x ∈ s, if ¬a = x then polarSym2 (⇑Q) (Sym2.map f s(a, x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Tactic:
not_true,

Goal state after:
case cons
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        (((if False then polarSym2 (⇑Q) (Sym2.map f s(a, a)) else 0) +
            ∑ x ∈ s, if ¬a = x then polarSym2 (⇑Q) (Sym2.map f s(a, x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
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
N' : Type u_8
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
B : BilinMap R M N
x y : M
⊢ (B (x + y)) (x + y) = (B x) x + (B y) y + ((B + flip B) x) y

Tactic:
by simp [add_add_add_comm, add_comm]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p : Submodule S R
⊢ 1 ≤ p ^ 0

Tactic:
pow_zero

Goal state after:
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p : Submodule S R
⊢ 1 ≤ 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: 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), P x

Tactic:
intro x
  have : x ∈ ⊤ := Submodule.mem_top (R := R)
  rw [← iSup_ι_range_eq_top] at this
  induction this using Submodule.iSup_induction' with
  | mem i x hx =>
    induction hx using Submodule.pow_induction_on_right' with
    | algebraMap r => exact algebraMap r
    | add _x _y _i _ _ ihx ihy => exact add _ _ ihx ihy
    | mul_mem _i x _hx px m hm =>
      obtain ⟨m, rfl⟩ := hm
      exact mul_ι _ _ px
  | zero => simpa only [map_zero] using algebraMap 0
  | add _x _y _ _ ihx ihy =>
    exact add _ _ ihx ihy

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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) 0)) (tail (update m i (x + y))) =
    (f (update m i x 0)) (tail (update m i x)) + (f (update m i y 0)) (tail (update m i y))

Tactic:
by cases i using Fin.cases <;> simp [Ne.symm]

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₂
f : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
c : R
x : M i
⊢ (f (update m i (c • x) 0)) (tail (update m i (c • x))) = c • (f (update m i x 0)) (tail (update m i x))

Tactic:
by cases i using Fin.cases <;> simp [Ne.symm]

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 : ℕ
v : Fin n.succ → M
⊢ (ιMulti R n.succ) v = (ι R) (v 0) * (ιMulti R n) (Matrix.vecTail v)

Tactic:
simp [ιMulti, Matrix.vecTail]

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
m : M
⊢ toExterior ((ι R) m) = (ExteriorAlgebra.ι R) m

Tactic:
by
  simp [toExterior]

Goal state after:
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, HasInjectiveDimensionLE X n

Tactic:
by_contra!
      simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this
      obtain ⟨n, hn⟩ := this
      rw [← injectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
      exact ENat.natCast_ne_top _ ((WithBot.coe_eq_coe).1 hn)

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
N' : Type u_3
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
r : R
x : M
this :
  (Finsupp.linearCombination R s.var) (Finsupp.single (update m i (r • x)) 1 - r • Finsupp.single (update m i x) 1) = 0
⊢ s.var (update m i (r • x)) = r • s.var (update m i x)

Tactic:
rw [Finsupp.smul_single, smul_eq_mul, mul_one, map_sub,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, sub_eq_zero] at this

Goal state after:
R : Type u
inst✝¹⁰ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
r : R
x : M
this : s.var (update m i (r • x)) = r • s.var (update m i x)
⊢ s.var (update m i (r • x)) = r • s.var (update m i x)
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
this : Small.{max v v', u} R
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
induction n generalizing M N with

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
induction n generalizing M N with

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

Goal state before:
pp: 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 (range v) = ⊤
⊢ Submodule.span R (range (ιMulti_family R n v)) = ⊤

Tactic:
by
  apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))
  rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
  simpa using ιMulti_family_span_fixedDegree_of_span R hv

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

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ s.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s)) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)

Tactic:
← Functor.map_comp,

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ s.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        ((hc Y).lift ((evaluation R Y).mapCone s) ≫ ((evaluation R Y).mapCone c).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)