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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)

Tactic:
← cancel_mono (e₂.hom.app _)

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✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y ≫ e₂.hom.app Y =
    ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)) ≫
      e₂.hom.app Y
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
    ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫ (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
    (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
| zero =>

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
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
⊢ Q.map g ≫ inv (Q.map ι) = 0

Tactic:
have h₂ : g ≫ retraction ι = 0 := by
    apply HomologicalComplex.to_single_hom_ext
    apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
h₂ : g ≫ retraction ι = 0
⊢ Q.map g ≫ inv (Q.map ι) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite

Goal state before:
pp: case zero
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
M : ModuleCat R
inst✝¹ : Module.Finite R ↑M
N : ModuleCat R
inst✝ : Module.Finite R ↑N
⊢ Module.Finite R (Ext N M 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
| zero =>

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix ⇑(Pi.basisFun R ι) * A = of fun i j ↦ (b.repr (A.col j)) i

Tactic:
classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Nat.card ↥(rootsOfUnity k R) ≤ k

Tactic:
by
  classical
  calc
    Nat.card (rootsOfUnity k R) = Nat.card { x // x ∈ nthRoots k (1 : R) } :=
      Nat.card_congr (rootsOfUnityEquivNthRoots R k)
    _ = Fintype.card { x // x ∈ nthRoots k (1 : R) } := Nat.card_eq_fintype_card
    _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
    _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
    _ ≤ k := card_nthRoots k 1

Goal state after:
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
i : n
A : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A)) = ↑↑A

Tactic:
obtain ⟨r, _, hr⟩ := mem_center_iff.mp A.property

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
i : n
A : ↥(center (SpecialLinearGroup n R))
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑↑A
⊢ ↑↑((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A)) = ↑↑A
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 1 0 * ↑A 0 1 = 1

Tactic:
· simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
· simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 0 1 * ↑A 1 0 = 1

Tactic:
· simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
· simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
⊢ i1 ∈ ↑{i | i ≠ i₀} →
    ∀ ⦃y : ι⦄,
      y ∈ ↑{i | i ≠ i₀} → i1 ≠ y → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 y

Tactic:
hi1

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
⊢ ∀ ⦃y : ι⦄,
    y ∈ ↑{i | i ≠ i₀} → i1 ≠ y → Function.onFun Commute (fun i ↦ if hi : i ≠ i₀ then diag2n hi (D i) ⋯ else 1) i1 y
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ∃ L L' D,
    ∃ (hD : (diagonal D).det = 1),
      M =
        (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
          (List.map TransvectionStruct.toSpecialLinearGroup L').prod

Tactic:
refine ⟨L, L', D, by simpa [hM] using M.2, Subtype.ext <| ?_⟩

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ↑M =
    ↑((List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, ⋯⟩ *
        (List.map TransvectionStruct.toSpecialLinearGroup L').prod)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case zero
⊢ ↑(T ^ 0) = !![1, 0; 0, 1]

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ ∑ x, ∑ x_1, σ₁ ((Finsupp.single i 1) x) •> (Finsupp.single j 1) x_1 •> M x x_1 = M i j

Tactic:
Finset.sum_eq_single_of_mem i (by simp) fun k _ hk ↦ by simp [hk],

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m N₂
i : n
j : m
⊢ ∑ x, σ₁ ((Finsupp.single i 1) i) •> (Finsupp.single j 1) x •> M i x = M i j
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (A i)
inst✝⁵ : (i : ι) → Module R (A i)
inst✝⁴ : AddMonoid ι
inst✝³ : GSemiring A
inst✝² : Semiring B
inst✝¹ : GAlgebra R A
inst✝ : Algebra R B
s : R
x y : GradedMonoid A
⊢ s • x • y = x • s • y

Tactic:
by
    dsimp
    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]

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

Goal state before:
pp: case zero
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
⊢ (of A i) a ^ 0 = (of A (0 • i)) (GradedMonoid.GMonoid.gnpow 0 a)

Tactic:
| zero =>

Goal state after:
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✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
x y : M
⊢ (⇑f * ⇑g) (x + y) =
    (⇑f * ⇑g) x + (⇑f * ⇑g) y + (((LinearMap.mul R A).compl₁₂ f g + (LinearMap.mul R A).flip.compl₁₂ g f) x) y

Tactic:
simp only [Pi.mul_apply, map_add, left_distrib, right_distrib, LinearMap.add_apply,
        LinearMap.compl₁₂_apply, LinearMap.mul_apply', LinearMap.flip_apply]
      abel_nf

Goal state after:
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:
| zero =>

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

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

Tactic:
simp only [associated_apply, sub_eq_add_neg, add_assoc, add_comm, add_left_comm]

Goal state after:
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.comap involute.toLinearMap (ι Q).range = (ι Q).range

Tactic:
← submodule_map_involute_eq_comap,

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
⊢ Submodule.map involute.toLinearMap (ι Q).range = (ι Q).range
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
n : ZMod 2
⊢ Submodule.comap involute.toLinearMap (evenOdd Q n) = evenOdd Q n

Tactic:
← submodule_map_involute_eq_comap,

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
n : ZMod 2
⊢ Submodule.map involute.toLinearMap (evenOdd Q n) = evenOdd Q n
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case zero
K : Type v
inst✝³ : Field K
hK : Invertible 2
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
| 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
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : i ≤ n
x : ι
⊢ i + x = n ↔ x = n - i

Tactic:
by rw [eq_tsub_iff_add_eq_of_le h, add_comm]

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

Goal state before:
pp: case zero
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 0

Tactic:
| zero =>

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

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

Tactic:
| zero =>

Goal state after:
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
w : ι → R
⊢ ∑ x, (((associatedHom R) Q) (∑ i, w i • v i)) (w x • v x) = (weightedSumSquares R fun i ↦ Q (v i)) w

Tactic:
weightedSumSquares_apply

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
⊢ ∑ x, (((associatedHom R) Q) (∑ i, w i • v i)) (w x • v x) = ∑ i, Q (v i) • (w i * w i)
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
⊢ ∀ (a : α), ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b

Tactic:
intro a

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
a : α
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b
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:
| zero =>

Goal state after:
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✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
x y : Fin 0
hfxy : f x = f y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
| zero =>

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 n : ℕ
a : Fin m → M
b : Fin n → M
⊢ (List.ofFn fun i ↦ (ι R) (a i)).prod * (List.ofFn fun i ↦ (ι R) (b i)).prod =
    (List.ofFn (⇑(ι R) ∘ Fin.append a b)).prod

Tactic:
← List.map_ofFn,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ (List.ofFn fun i ↦ (ι R) (a i)).prod * (List.ofFn fun i ↦ (ι R) (b i)).prod =
    (List.map (⇑(ι R)) (List.ofFn (Fin.append a b))).prod
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case zero
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f 0) v

Tactic:
| zero =>

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

Goal state before:
pp: case pos
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ (v ∘ ⇑(ofFinEmbEquiv.symm s)) (i.castLT hi) =
    v
      ↑((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
          (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm (Fin.castAdd n (i.castLT hi)))))

Tactic:
finSumFinEquiv_symm_apply_castAdd

Goal state after:
case pos
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ (v ∘ ⇑(ofFinEmbEquiv.symm s)) (i.castLT hi) =
    v
      ↑((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
          (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (Sum.inl (i.castLT hi))))
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + 0
⊢ e = 0

Tactic:
| zero =>

Goal state after:
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 = ⊤
⊢ Submodule.map (ExteriorAlgebra.ι R) ⊤ ^ n ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})

Tactic:
← hs,

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 = ⊤
⊢ Submodule.map (ExteriorAlgebra.ι R) (span R s) ^ n ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
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
⊢ HasInjectiveDimensionLE M 0 ↔ HasInjectiveDimensionLE N 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ (Λ.chainComplexMap (𝟙 X)).f 0 = (𝟙 (Λ.chainComplex X)).f 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case zero
A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
⊢ (Λ.chainComplexMap 0).f 0 = HomologicalComplex.Hom.f 0 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: case zero
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ (Λ.chainComplexMap (f ≫ g)).f 0 = (Λ.chainComplexMap f ≫ Λ.chainComplexMap g).f 0

Tactic:
| zero =>

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
⊢ r • 1 = f r

Tactic:
rw [RingHom.smul_toAlgebra, mul_one]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
F : Discrete WalkingPair ⥤ C ⥤ Type u
⊢ PreservesLimit F colim

Tactic:
apply preservesLimit_of_iso_diagram colim (diagramIsoPair F).symm

Goal state after:
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✝ : IsCofilteredOrEmpty C
X : C × C
⊢ IsCofiltered (CostructuredArrow (Functor.diag C) X)

Tactic:
have : ∀ Y, IsCofiltered (CostructuredArrow (Over.forget X.1) Y) := by
    rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
    infer_instance

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
X : C × C
this : ∀ (Y : C), IsCofiltered (CostructuredArrow (Over.forget X.1) Y)
⊢ IsCofiltered (CostructuredArrow (Functor.diag C) X)
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit (uncurry.obj (curry.obj G)) ≅ limit (curry.obj G ⋙ lim)

Tactic:
exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)

Goal state after: