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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ K.ExactAt j ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j), x₂ ≫ K.d j k = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
rw [K.exactAt_iff' i j k hi hk]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ (K.sc' i j k).Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j), x₂ ≫ K.d j k = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j
Module: Mathlib.Algebra.Homology.Refinements

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
⊢ K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
by
  subst hi hk
  exact (K.sc j).liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements x₂ hx₂

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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ ∑ x, (mk₀ (c.ι i ≫ c.π x)).comp (x✝ x) ⋯ = x✝ i

Tactic:
Finset.sum_eq_single i _ (by simp),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ (mk₀ (c.ι i ≫ c.π i)).comp (x✝ i) ⋯ = x✝ i

C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (mk₀ (c.ι i ≫ c.π b)).comp (x✝ b) ⋯ = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ (inr S.f).f n₀ ≫ (mappingCone S.f).d n₀ n₁) ≫
        (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ =
      0 ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ (inr S.f).f n₀ ≫ (mappingCone S.f).d n₀ n₁) ≫
        (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
inr_f_d,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫
        (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ =
      0 ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
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 : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∑ x, (x✝ x).comp (mk₀ (c.ι x ≫ c.π i)) ⋯ = x✝ i

Tactic:
Finset.sum_eq_single i _ (by simp),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ (x✝ i).comp (mk₀ (c.ι i ≫ c.π i)) ⋯ = x✝ i

C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (x✝ b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0
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
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (F ⋙ G) x✝¹).inv.app (Opposite.unop x✝)).op ≫
      (shiftFunctor (OppositeShift E A) x✝¹).map (𝟙 ((OppositeShift.functor A (F ⋙ G)).obj x✝)) =
    𝟙 ((OppositeShift.functor A (F ⋙ G)).obj ((shiftFunctor (OppositeShift C A) x✝¹).obj x✝)) ≫
      (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom.app x✝

Tactic:
simp only [Functor.map_id, comp_id, id_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
A : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
F : C ⥤ D
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (F ⋙ G) x✝¹).inv.app (Opposite.unop x✝)).op =
    (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom.app x✝
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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ a + b = 0

Tactic:
← add_left_inj a,

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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ a + b + a = 0 + a
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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ b = -a

Tactic:
← add_left_inj a,

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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ b + a = -a + a
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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
X : D
⊢ b = -a

Tactic:
rw [← add_left_inj a, h, neg_add_cancel]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ b = -a

Tactic:
← add_left_inj a,

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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ b + a = -a + a
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
a b : A
h : b + a = 0
inst✝ : F.CommShift A
Y : D
⊢ b = -a

Tactic:
rw [← add_left_inj a, h, neg_add_cancel]

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.SeparatingLeft ∧ M.SeparatingRight ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
separatingLeft_def,

Goal state after:
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
⊢ (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ M.SeparatingRight ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
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✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ Mᵀ.SeparatingLeft ↔ M.SeparatingRight

Tactic:
separatingLeft_def,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (v : n → R), (∀ (w : m → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → v = 0) ↔ M.SeparatingRight
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✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (w : m → R), (∀ (v : n → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → w = 0) ↔ M.SeparatingLeft

Tactic:
separatingLeft_def,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Finite m
inst✝ : Finite n
this✝ : Fintype m
this : Fintype n
⊢ (∀ (w : m → R), (∀ (v : n → R), v ⬝ᵥ Mᵀ *ᵥ w = 0) → w = 0) ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝ : CommMonoid R
ζ : ↥(rootsOfUnity k R)
m : ℕ
⊢ ↑(↑ζ ^ m) = ↑↑ζ ^ m

Tactic:
Units.val_pow_eq_pow_val

Goal state after:
R : Type u_4
k : ℕ
inst✝ : CommMonoid R
ζ : ↥(rootsOfUnity k R)
m : ℕ
⊢ ↑↑ζ ^ m = ↑↑ζ ^ m
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = (algebraMap A K) (0 i)

Tactic:
calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm

Goal state after:
case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i

case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha * diag2 a⁻¹ ⋯ = 1

Tactic:
exact diag2_mul_inv a ha

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
x : CliffordAlgebra Q₁
⊢ (map g) ((map f) x) = x

Tactic:
replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map g) ((map f) x) = x
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
⊢ ⟨⅟2, ⋯⟩ • 1 * 2 = 1

Tactic:
ext m
    dsimp [Submonoid.smul_def]
    rw [← ofNat_smul_eq_nsmul R, invOf_smul_smul (2 : R) m]

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
⊢ (DFinsupp.sum r' fun j rj ↦ 0) = 0

Tactic:
exact DFinsupp.sum_zero

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₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Tactic:
skewAdjointMatricesSubmodule,

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
⊢ A₁ ∈ pairSelfAdjointMatricesSubmodule (-J) J ↔ J.IsSkewAdjoint A₁
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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ 0) = 0

Tactic:
exact DFinsupp.sum_zero

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ 0) = 0

Tactic:
exact DFinsupp.sum_zero

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✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ 0) = 0

Tactic:
exact DFinsupp.sum_zero

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

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
⊢ ⨆ i, ⨆ j, (ι Q).range ^ ↑j = ⨆ i, (ι Q).range ^ ↑i.snd

Tactic:
iSup_sigma

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ i, ⨆ j, (ι Q).range ^ ↑j = ⨆ i, ⨆ j, (ι Q).range ^ ↑⟨i, j⟩.snd
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 : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| (TrivSqZeroExt.sndHom R N ∘ₗ (TrivSqZeroExt.map f).toLinearMap) ∘ₗ toTrivSqZeroExt.toLinearMap

Tactic:
TrivSqZeroExt.sndHom_comp_map

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ toTrivSqZeroExt.toLinearMap
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 = ⊤
⊢ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}) ≤ ⋀[R]^n M

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 = ⊤
⊢ ⋀[R]^n M ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})

Tactic:
· rw [span_le]
    rintro - ⟨y, ⟨y_mem, rfl⟩⟩
    apply ExteriorAlgebra.ιMulti_range R n
    simp

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 = ⊤
⊢ ⋀[R]^n M ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})
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) =
    (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)

Tactic:
map_id

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
⊢ (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app ((F.obj j).obj 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.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X) (G.obj X) (H.obj X)).hom ▷ K.obj X ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ F.obj X ◁ (α_ (G.obj X) (H.obj X) (K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom

Tactic:
rw [pentagon]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
k : J
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)

Tactic:
have : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k) :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _)

Goal state after:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁸ : Category.{v_1, u_1} J
inst✝⁷ : Category.{v_2, u_2} C
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Category.{v_4, u_4} E
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory E
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
k : J
this : tensorLeft F ⋙ (evaluation J C).obj k ≅ (evaluation J C).obj k ⋙ tensorLeft (F.obj k)
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
K : Type u₁
inst✝² : Category.{v₁, u₁} K
inst✝¹ : LocallySmall.{w, v, u} J
inst✝ : InitiallySmall J
X : J
⊢ InitiallySmall (Over X)

Tactic:
have : InitiallySmall.{w} (CostructuredArrow (fromInitialModel.{w} J) X) :=
    initiallySmall_of_essentiallySmall _
  exact initiallySmall_of_initial_of_initiallySmall
    (CostructuredArrow.toOver (fromInitialModel.{w} J) X)

Goal state after: