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✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctor C a).map ((shiftFunctorCompIsoId C a (-a) ⋯).inv.app (G.obj (F.obj X✝))) ≫
        (shiftFunctor C a).map ((shiftFunctor C (-a)).map ((Functor.commShiftIso G a).inv.app (F.obj X✝))) ≫
          (shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X✝))) ≫
            (Functor.commShiftIso G a).hom.app (F.obj X✝)

Tactic:
rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
    (shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]

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✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId C (-a) a ⋯).hom.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          (𝟭 C).map ((Functor.commShiftIso G a).inv.app (F.obj X✝)) ≫ (Functor.commShiftIso G a).hom.app (F.obj X✝)
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ᵒᵖ
hT₁ : T₁ ∈ distinguishedTriangles C
hT₂ : T₂ ∈ distinguishedTriangles C
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃

Tactic:
mem_distinguishedTriangles_iff

Goal state after:
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ᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
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
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ∀ (i_1 : ℤ), (ComplexShape.up ℤ).Rel i_1 i → L.d i_1 i ≫ Injective.factorThru (𝟙 I) α = 0

Tactic:
rintro j rfl

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
j : ℤ
ι : (singleFunctor C (j + 1)).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE (j + 1)
inst✝ : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I).inv ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I).hom ≫ α
⊢ L.d j (j + 1) ≫ Injective.factorThru (𝟙 I) α = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
⊢ K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥

Tactic:
← Finset.coe_singleton

Goal state after:
K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
⊢ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ ↑{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 solution' : relations.Solution M
h : solution = solution'
g : relations.G
⊢ solution.var g = solution'.var g

Tactic:
h

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution solution' : relations.Solution M
h : solution = solution'
g : relations.G
⊢ solution'.var g = solution'.var g
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
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution M
h : solution = solution'
f : M →ₗ[A] N
⊢ solution.postcomp f = solution'.postcomp f

Tactic:
h

Goal state after:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution M
h : solution = solution'
f : M →ₗ[A] N
⊢ solution'.postcomp f = solution'.postcomp f
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : Fintype ι
⊢ ∑ x, (e.repr (v j)) x • e x = v j

Tactic:
e.sum_repr

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g, f g = ↑0

Tactic:
Nat.cast_zero

Goal state after:
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g, f g = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M → ζ ∈ rootsOfUnity (k * d) M

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ M.det = 0 → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
· contrapose!
    intro h
    have : Function.Injective (Matrix.toLin' M) := by
      simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
    have : M * (LinearEquiv.ofInjectiveEndo _ this).symm.toMatrix' = 1 := by
      refine Matrix.toLin'.injective (LinearMap.ext fun v => ?_)
      rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
      exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v
    exact Matrix.det_ne_zero_of_right_inverse this

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
⊢ (∃ v, v ≠ 0 ∧ v ᵥ* M = 0) ↔ M.det = 0

Tactic:
simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff

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

Goal state before:
pp: case pos
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:
h

Goal state after:
case pos
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 j₀ j₀ ≤ v j₀ * A j₀ j₀
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : mulLeft₃ = mulRight₃
x y z : R
⊢ ((mulLeft₃ x) y) z = ((mulRight₃ x) y) z

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : mulLeft₃ = mulRight₃
x y z : R
⊢ ((mulRight₃ x) y) z = ((mulRight₃ x) y) z
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
by fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
by fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
by fin_cases j <;> tauto

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
by fin_cases j <;> tauto

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

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

Tactic:
h

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
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'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ (toMatrix₂' R) B = (toMatrix₂' R) B'

Tactic:
h

Goal state after:
case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
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'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ (toMatrix₂' R) B' = (toMatrix₂' R) B'
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬(i = 0 ∧ j = 0)
⊢ i ≠ 0 ∨ j ≠ 0

Tactic:
not_and_or

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i = 0 ∨ ¬j = 0
⊢ i ≠ 0 ∨ j ≠ 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ ↑0 ∈ A 0

Tactic:
Nat.cast_zero

Goal state after:
case zero
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
⊢ 0 ∈ A 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case mp
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'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B = B'
⊢ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'

Tactic:
h

Goal state after:
case mp
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'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B = B'
⊢ (toMatrix₂ b₁ b₂) B' = (toMatrix₂ b₁ b₂) B'
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
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ (i + j)

Tactic:
by
    rw [pow_add]
    exact Submodule.mul_mem_mul hp hq

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

Goal state before:
pp: case algebraMap
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
r : R
⊢ involute ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case mem.algebraMap
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
r : R
⊢ P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
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 : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
r : R
⊢ P (reverse ((Algebra.algebraMap R (CliffordAlgebra Q)) r))

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case e_fst.algebraMap
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
r : R
⊢ (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) ((algebraMap R (CliffordAlgebra Q)) r)).1 = (algebraMap R (CliffordAlgebra Q)) r

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((algebraMap R (CliffordAlgebra Q)) r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case mem_mul_mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive ((algebraMap R (CliffordAlgebra Q)) r * b) ⋯

Tactic:
| algebraMap r =>

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
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
← (algebraMap R (ExteriorAlgebra R M)).map_one,

Goal state after:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ (algebraMap R (ExteriorAlgebra R M)) 1
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
⊢ ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
          forget AddMonCat).ColimitTypeRel
      x y →
    colimitSMulAux F r x = colimitSMulAux F r y

Tactic:
h

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
h :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
        forget AddMonCat).ColimitTypeRel
    x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
T : ShortComplex (ModuleCat R)
h : T.Exact
⊢ (T.map (localizedModuleFunctor S)).Exact

Tactic:
rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] at h ⊢
  exact IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
    (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ ((ιMulti R 1) fun x ↦ m₁ + m₂) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂
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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = (ιMulti R 1) (update (fun x ↦ 0) 0 m₁) + (ιMulti R 1) fun x ↦ m₂
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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = (ιMulti R 1) (update (fun x ↦ 0) 0 m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) =
    (ιMulti R 1) (update (fun x ↦ 0) 0 m₁) + (ιMulti R 1) (update (fun x ↦ 0) 0 m₂)
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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ ((ιMulti R 1) fun x ↦ r • m) = r • (ιMulti R 1) fun x ↦ m

Tactic:
h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m
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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m

Tactic:
h

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'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) (update (fun x ↦ 0) 0 m)