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 : CompatibilityCounit adj e₁ e₂
X : C
this :
  F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
rw [this, dsimp% e₁.hom.naturality_assoc, ← Functor.map_comp, left_triangle_components]

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 : CompatibilityCounit adj e₁ e₂
X : C
this :
  F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X = e₁.hom.app X ≫ (shiftFunctor D a).map (𝟙 (F.obj X))
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝³ : Category.{v_2, u_4} D
inst✝² : HasShift D B
F : C ⥤ D
inst✝¹ : F.CommShift B
G : C ⥤ D
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ ((Functor.commShiftIso (𝟭 (PullbackShift C φ)) x✝¹).hom ≫
          Functor.whiskerRight (PullbackShift.natIsoId C φ).hom (shiftFunctor (PullbackShift C φ) x✝¹)).app
      x✝ =
    ((shiftFunctor (PullbackShift C φ) x✝¹).whiskerLeft (PullbackShift.natIsoId C φ).hom ≫
          (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x✝¹).hom).app
      x✝

Tactic:
simp [PullbackShift.natIsoId, Functor.commShiftPullback_iso_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }

Tactic:
rw [mul_comm]

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ b • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ a • 𝟙 X, naturality := ⋯ }
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := ⋯
α : K.X i ⟶ P := ⋯
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π).f i = (𝟙 ((singleFunctor C i).obj P)).f i

Tactic:
rw [comp_f, mkHomFromSingle_f, assoc, id_f, this, Projective.factorThru_comp_assoc,
        id_comp, Iso.hom_inv_id]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ 𝟙 (((single C (ComplexShape.up ℤ) i).obj P).X i) = 𝟙 (((singleFunctor C i).obj P).X i)
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ k = 1

Tactic:
rw [mem_rootsOfUnity]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
⊢ ((toLin b b) (A * A⁻¹)) x = x

Tactic:
Matrix.mul_nonsing_inv _ hA,

Goal state after:
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
⊢ ((toLin b b) 1) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

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

Tactic:
rintro ⟨v, hv, mul_eq⟩

Goal state after:
case mp
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
⊢ M.det = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mp
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, v ≠ 0 ∧ M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

Tactic:
rintro ⟨v, hv, mul_eq⟩

Goal state after:
case mp
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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
⊢ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr
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, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
rintro ⟨v, hv, mul_eq⟩

Goal state after:
case mpr
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
⊢ ∃ v, v ≠ 0 ∧ M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
R✝ : Type v
inst✝⁵ : CommRing R✝
S : Type u_1
T : Type u_2
inst✝⁴ : CommRing S
inst✝³ : CommRing T
f : R✝ →+* S
R : Type u_3
m : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : GL n R
y : GL m R
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) ↑x⁻¹ ↑y⁻¹ * kroneckerMap (fun x1 x2 ↦ x1 * x2) ↑x ↑y = 1

Tactic:
by simp only [← mul_kronecker_mul, Units.inv_mul, one_kronecker_one]

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
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑(A * A⁻¹) = LinearMap.id

Tactic:
mul_inv_cancel,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑1 = LinearMap.id
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁) m = ((map (f.comp g)).toLinearMap ∘ₗ ι Q₁) m

Tactic:
dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid N₂
inst✝¹³ : Module R N₂
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ ((toLinearMap₂'Aux σ₁ σ₂ M) x) y = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j

Tactic:
toLinearMap₂'Aux,

Goal state after:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid N₂
inst✝¹³ : Module R N₂
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ ((mk₂'ₛₗ σ₁ σ₂ (fun v w ↦ ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> M i j) ⋯ ⋯ ⋯ ⋯) x) y =
    ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ polar f x y = polar f y x

Tactic:
rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ((mulHom A) ((of A ai) ax)) ((of A bi) bx) = ((mulHom A) ((of A bi) bx)) ((of A ai) ax)

Tactic:
mulHom_of_of,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ (of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = ((mulHom A) ((of A bi) bx)) ((of A ai) ax)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (toAddMonoid f) ((of A xi) xv * (of A yi) yv) = (toAddMonoid f) ((of A xi) xv) * (toAddMonoid f) ((of A yi) yv)

Tactic:
simp_rw [of_mul_of, toAddMonoid_of]

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (f (xi + yi)) (GradedMonoid.GMul.mul xv yv) = (f xi) xv * (f yi) yv
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: 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'
⊢ ((toLinearMap₂' R) J).IsAdjointPair ((toLinearMap₂' R) J') ⇑(toLin' A) ⇑(toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
by
  rw [isAdjointPair_iff_comp_eq_compl₂]
  have h :
    ∀ B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R,
      B = B' ↔ LinearMap.toMatrix₂' R B = LinearMap.toMatrix₂' R B' := by
    intro B B'
    constructor <;> intro h
    · rw [h]
    · exact (LinearMap.toMatrix₂' R).injective h
  simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂,
    LinearMap.toMatrix'_toLin', LinearMap.toMatrix'_toLinearMap₂']
  rfl

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 : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ f (snoc m (x + y)) = f (snoc m x) + f (snoc m y)

Tactic:
simp_rw [f.snoc_add]

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) = ∑ i, Q (v i) • (w i * w i)

Tactic:
refine sum_congr rfl fun j hj => ?_

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ Nontrivial ↑(powersetCard α n) ↔ 0 < n ∧ n < Nat.card α

Tactic:
by
  rw [← Finite.one_lt_card_iff_nontrivial, powersetCard.card, Nat.one_lt_iff_ne_zero_and_ne_one,
    ne_eq, Nat.choose_eq_zero_iff, ne_eq, Nat.choose_eq_one_iff]
  grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ x₂ = 0

Tactic:
obtain ⟨x₃, rfl⟩ := Ext.covariant_sequence_exact₂ _ hS x₂
    (Ext.eq_zero_of_hasInjectiveDimensionLT _ n hi)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext Y S.X₁ i
⊢ x₃.comp (Ext.mk₀ S.f) ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
e : X ≅ Y
⊢ sInf {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i} =
    sInf {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i}

Tactic:
congr! 5

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
e : X ≅ Y
x✝ : WithBot ℕ∞
a✝¹ : ℕ
a✝ : x✝ < ↑a✝¹
⊢ HasInjectiveDimensionLT X a✝¹ ↔ HasInjectiveDimensionLT Y a✝¹
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n g) ((map n f) x✝) = x✝

Tactic:
by rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]

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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]
    rintro - ⟨f, ⟨f_range, rfl⟩⟩
    rw [Set.mem_ofPred] at f_range
    obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range
    exact ιMulti_family_span_fixedDegree_aux R v α

Goal state after:
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X

Tactic:
← hm

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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (c.ι.app j ≫ m).app X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ snd A I ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)

Tactic:
rw [this, ← uncurry_natural_right, ← eq_curry_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ t.to (A ⟹ I) ≫ (ihom A).map (t.to (A ⊗ I)) = curry (𝟙 (A ⊗ I))
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
c d : C
⊢ ∀ (j₁ j₂ : C) (x : j₁ ⟶ j₂),
    (ConcreteCategory.hom (colimit.ι (constPUnitFunctor C) j₁)) PUnit.unit =
      (ConcreteCategory.hom (colimit.ι (constPUnitFunctor C) j₂)) PUnit.unit

Tactic:
exact fun c d f => colimit_sound f rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
rw [← ModuleCat.mono_iff_injective]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Mono (f.app 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 (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)

Tactic:
let c := limit.cone (uncurry.obj F)
  let P : IsLimit c := limit.isLimit _
  let G := DiagramOfCones.mkOfHasLimits F
  let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _
  have Q' := coneOfConeUncurryIsLimit Q P
  have Q'' := limit.isLimit (F ⋙ lim)
  exact IsLimit.conePointUniqueUpToIso Q' Q''

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom = (ρ_ X✝).hom ≫ x✝

Tactic:
ext1; apply rightUnitor_naturality

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f R ⊓ Sieve.pullback f S ∈ J Y

Tactic:
R.pullback_eq_top_of_mem hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ J X
sj : S ∈ J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), ⊥ ∈ J X
⊢ J = ⊤

Tactic:
rw [_root_.eq_top_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), ⊥ ∈ J X
⊢ ⊤ ≤ J
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : CreatesLimitsOfShape WalkingCospan F
inst✝ : J.HasPullbacks
X Y : C
R : Presieve Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
⊢ R.HasPullbacks f

Tactic:
refine ⟨fun {Z g} hg ↦ ?_⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝¹ : CreatesLimitsOfShape WalkingCospan F
inst✝ : J.HasPullbacks
X Y : C
R : Presieve Y
f : X ⟶ Y
hR : R ∈ (comap F J).coverings Y
Z : C
g : Z ⟶ Y
hg : R g
⊢ HasPullback g f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
I' : Type u_2
X' : I' → C
Y : C
h✝ : Set.range X ⊆ Set.range X'
Z : C
f : Z ⟶ Y
i : I
g : Z ⟶ X i
i' : I'
h : X' i' = X i
⊢ (ofObjects X' Y).arrows f

Tactic:
exact ⟨i', ⟨h ▸ g⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P R → IsSeparatedFor P (generate R).arrows

Tactic:
intro h x t₁ t₂ ht₁ ht₂

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P (generate R).arrows → IsSeparatedFor P R

Tactic:
intro h x t₁ t₂ ht₁ ht₂

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂