mathlib-initiative/mathlib-tactics huggingface dataset:
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 ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    a ≫ (S.f.f n₁ + (inl S.f).v n₁ n₀ ⋯ ≫ (snd S.f).v n₀ n₀ ⋯ ≫ S.X₂.d n₀ n₁) + b ≫ S.X₂.d n₀ n₁ = 0
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:
inl_v_snd_v_assoc,

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 ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ (S.f.f n₁ + 0 ≫ S.X₂.d n₀ n₁) + b ≫ S.X₂.d n₀ n₁ = 0
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.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
b₃ : B
h₃ : b₃ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
      (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃).inv.app X

Tactic:
obtain rfl : b₃ = φ a₁ + φ a₂ := by rw [h₃, φ.map_add]

Goal state after:
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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
      (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.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
inst✝ : F.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F 0) (Functor.CommShift.isoZero G A)

Tactic:
rw [F.commShiftIso_zero]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ (inverse C ⋙ functor C).obj T ≅ (𝟭 (Triangle Cᵒᵖ)).obj T

Tactic:
by
    refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
    · simp
    · simp
    · dsimp
      rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
        opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
        Iso.hom_inv_id_app, Functor.map_id]
      simp only [Functor.id_obj, comp_id]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1

Tactic:
← hxy

Goal state after:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n

Tactic:
intro n hn

Goal state after:
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ⇑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ #{a | a ^ n = 1} ≤ n
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
⊢ Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N

Tactic:
rintro _ ⟨ζ, h, rfl⟩
  simp_all only [← map_pow, mem_rootsOfUnity, SetLike.mem_coe, map_one]

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this : Function.Injective ⇑(toLin' M)
v : n → K
⊢ (toLin' (M * toMatrix' ↑(LinearEquiv.ofInjectiveEndo (toLin' M) this).symm)) v = (toLin' 1) v

Tactic:
rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]

Goal state after:
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
this : Function.Injective ⇑(toLin' M)
v : n → K
⊢ (toLin' M) (↑(LinearEquiv.ofInjectiveEndo (toLin' M) this).symm v) = LinearMap.id v
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
A : GL n R
⊢ (↑A).det * (↑A⁻¹).det = 1

Tactic:
by rw [← det_mul, A.mul_inv, det_one]

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

Goal state before:
pp: 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, ∑ i, A i j ≤ 0

Tactic:
· obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
      refine ⟨j₀, ?_⟩
      rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
      rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
      refine Finset.sum_le_sum (fun i hi => ?_)
      by_cases h : i = j₀
      · rw [h]
      · exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

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

Goal state before:
pp: case inr.refine_2
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ (scalar n) (↑A i i) = ↑A

pp: case inr.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B

Tactic:
· exact scalar_eq_self_of_mem_center h i

Goal state after:
case inr.refine_3
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
r : R
left✝ : r ^ Fintype.card n = 1
hr : (scalar n) r = ↑A
B : SpecialLinearGroup n R
⊢ B * A = A * B
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
by
  ext m; exact map_apply_ι _ m

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.ofFn r).prod ∈ A (List.ofFn i).sum

Tactic:
rw [List.ofFn_eq_map, List.ofFn_eq_map]

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = v x✝¹ * ∑ x, M x✝¹ x * w x

Tactic:
Finset.mul_sum

Goal state after:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = ∑ i, v x✝¹ * (M x✝¹ i * w i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ i ∈ Finset.cons a s ha, Q (f i) + ∑ ij ∈ (Finset.cons a s ha).sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
| cons a s ha ih =>

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

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (∑ i ∈ Finset.cons a s ha, f i) =
    ∑ ij ∈ (Finset.cons a s ha).sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ Finset.cons a s ha, Q (f i)

Tactic:
| cons a s ha ih =>

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

Goal state before:
pp: case ι
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ reverse (involute ((ι Q) x✝)) = involute (reverse ((ι Q) x✝))

Tactic:
| ι =>

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

Goal state before:
pp: R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
⊢ (toMatrix b Q).IsSymm

Tactic:
by
  ext i j
  rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]

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.map reverse (ι Q).range = (ι Q).range

Tactic:
rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp,
    ← Submodule.map_comp]

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 (↑(MulOpposite.opLinearEquiv R).symm ∘ₗ ↑(MulOpposite.opLinearEquiv R)) (ι Q).range = (ι Q).range
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑s).Nontrivial ↔ 1 < n

Tactic:
rw [← coe_coe, Finset.nontrivial_coe, ← one_lt_card_iff_nontrivial, card_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
⊢ f.currySum.uncurrySum = f

Tactic:
ext
  simp only [uncurrySum_apply, currySum_apply]
  congr
  ext (_ | _) <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case e_5.e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
x✝ : Fin k
⊢ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((s.orderEmbOfFin hk) x✝) = x

Tactic:
Finset.piecewise_eq_of_mem

Goal state after:
case e_5.e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
x✝ : Fin k
⊢ x = x

case e_5.e_6.hi
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
x✝ : Fin k
⊢ (s.orderEmbOfFin hk) x✝ ∈ s
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✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)

Goal state after:
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
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ f (x.pred hx).succ = f (y.pred ⋯).succ
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case bot
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ⊥
⊢ ⊥ ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n

Tactic:
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
    exact ⟨0, by simp [← injectiveDimension_le_iff, hd]⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ limMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
      (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    (limMap (F.whiskerLeft (restriction R f)) ≫
        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          (limMap (F.whiskerLeft (restriction R g)) ≫
            (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
          (limit (F ⋙ evaluation R Z))

Tactic:
dsimp
    rw [← cancel_mono (preservesLimitIso _ _).hom, assoc, assoc, assoc, assoc, Iso.inv_hom_id,
      comp_id]
    apply limit.hom_ext
    intro j
    simp only [Functor.map_comp, assoc, ← Functor.assoc, preservesLimitIso_hom_π,
      ← ModuleCat.restrictScalarsComp'App_inv_naturality]
    rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, assoc, preservesLimitIso_inv_π]
    simp

Goal state after:
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
⊢ (ConcreteCategory.hom (colimit.ι (constPUnitFunctor C) c)) PUnit.unit =
    (ConcreteCategory.hom (colimit.ι (constPUnitFunctor C) d)) PUnit.unit

Tactic:
apply constant_of_preserves_morphisms (colimit.ι (constPUnitFunctor C) · PUnit.unit)

Goal state after:
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
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)

Tactic:
rw [← Cocone.w cR f]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (R.map f ≫ cR.ι.app Y)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ f.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj X')) ≫ F.map g =
    f.hom ≫ F.partialLeftAdjointHomEquiv g

Tactic:
← partialLeftAdjointHomEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ f.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj X') ≫ g) = f.hom ≫ F.partialLeftAdjointHomEquiv g
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ g.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj X')) ≫ F.map (F.partialLeftAdjointHomEquiv.symm f) =
    g.hom ≫ f

Tactic:
← partialLeftAdjointHomEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ g.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj X') ≫ F.partialLeftAdjointHomEquiv.symm f) =
    g.hom ≫ f
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : F.PartialLeftAdjointSource
⊢ F.partialLeftAdjointMap (𝟙 X) = 𝟙 (F.partialLeftAdjointObj X)

Tactic:
apply F.partialLeftAdjointHomEquiv.injective
    simp [partialLeftAdjointHomEquiv_map]

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
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (ρ_ (M.obj Y)).inv))
      ((ModuleCat.Hom.hom (M.map f)) m) =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      ((ModuleCat.Hom.hom (ρ_ (M.obj X)).inv) m)

Tactic:
rightUnitor_inv_apply,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (M.map f)) m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] 1 =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      ((ModuleCat.Hom.hom (ρ_ (M.obj X)).inv) m)
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
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (M.map f)) m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] 1 =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      ((ModuleCat.Hom.hom (ρ_ (M.obj X)).inv) m)

Tactic:
rightUnitor_inv_apply,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (M.map f)) m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] 1 =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] 1)
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
⊢ Sieve.pullback i S ∈ J X ↔ S ∈ J Y

Tactic:
by
  refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
  convert! J.pullback_stable (inv i) H
  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsEmpty C
J : GrothendieckTopology C
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsEmpty C
J : GrothendieckTopology C
⊢ ∀ (X : C), ⊥ ∈ J X