mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ (mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0).Exact

Tactic:
· refine exact_of_δ₀ (hR₂.exact 0).exact_toComposableArrows (exact_of_δ₀ ?_ ?_)
    · refine exact₂_mk _ (by simp) ?_
      rwa [ShortComplex.exact_iff_epi _ (by simp)]
    · refine exact₂_mk _ (by simp) ?_
      rw [ShortComplex.exact_iff_epi _ (by simp)]
      infer_instance

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
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
⊢ Module R (X ⟶ Y)

Tactic:
exact
  { one_smul := fun a => by
      simp only [smulOfRingMorphism_smul_eq,
        Functor.id_obj, map_one, End.one_def, NatTrans.id_app, id_comp]
    mul_smul := fun a b f => by
      simp only [smulOfRingMorphism_smul_eq', Functor.id_obj, map_mul, End.mul_def,
        NatTrans.comp_app, assoc]
    smul_zero := fun a => by
      simp only [smulOfRingMorphism_smul_eq, comp_zero]
    zero_smul := fun a => by
      simp only [smulOfRingMorphism_smul_eq, map_zero,
        zero_app, zero_comp]
    smul_add := fun a b => by
      simp [smulOfRingMorphism_smul_eq]
    add_smul := fun a b f => by
      simp [smulOfRingMorphism_smul_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
φ : R →+* CatCenter C
X✝ Y✝ : C
this : (X Y : C) → Module R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
simp only [smulOfRingMorphism_smul_eq', assoc]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
⊢ G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)

Tactic:
have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: case succ
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
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))

Goal state after:
case succ
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
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := Y, X₂ := Injective.under Y, X₃ := cokernel (Injective.ι Y), f := Injective.ι Y,
    g := cokernel.π (Injective.ι Y), zero := ⋯ }
⊢ Small.{w, max u v} (Ext X Y (n + 1))
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.Nondegenerate ↔
    (∀ (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:
nondegenerate_iff,

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

Tactic:
nondegenerate_iff,

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
⊢ M.SeparatingLeft ∧ M.SeparatingRight ↔ (∀ (v : m → R), v ᵥ* M = 0 → v = 0) ∧ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑(ζ ^ m) = ↑↑ζ ^ m_1

Tactic:
← zpow_mod_orderOf,

Goal state after:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑(ζ ^ (m % ↑(orderOf ζ))) = ↑↑ζ ^ m_1
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
⊢ ∀ (m : M₂), Q₁ ((↑f.symm).toFun m) = Q₂ m

Tactic:
by intro m; rw [← f.map_app]; congr; exact f.toLinearEquiv.apply_symm_apply m

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
by rwa [det_fin_two] at hm

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

Goal state before:
pp: case cons
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
t : TransvectionStruct ι F
L : List (TransvectionStruct ι F)
ih : P (List.map TransvectionStruct.toSpecialLinearGroup L).prod
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup (t :: L)).prod

Tactic:
rw [List.map_cons, List.prod_cons, t.toSpecialLinearGroup_def]
      exact hmul _ _ (htransvec t.i t.j t.hij t.c) ih

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
⊢ SpecialLinearGroup.transvection ⋯ c ∈ commutator SL(2, F)

Tactic:
have (b c' : F) (hc : c' = b * (a ^ 2 - 1)) :
      ⁅diag2 a⁻¹ (inv_ne_zero ha), SpecialLinearGroup.transvection one_ne_zero b⁆ =
      (SpecialLinearGroup.transvection one_ne_zero c' : SL(2, F)) := by
    rw [commutatorElement_def, diag2_inv a⁻¹ (inv_ne_zero ha),
      SpecialLinearGroup.transvection_inv one_ne_zero b]
    refine Subtype.ext <| Matrix.ext fun i j ↦ ?_
    fin_cases i <;> fin_cases j <;>
    simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, inv_inv, mul_add, add_mul,
      mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
      mul_sub_one, ← sub_eq_add_neg]
  rw [← this (c / (a ^ 2 - 1)) c (div_mul_cancel₀ c (sub_ne_zero_of_ne hasq)).symm]
  exact Subgroup.commutator_mem_commutator (Subgroup.mem_top _) (Subgroup.mem_top _)

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

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) (a * ↑b)) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
x : ι × ι
hx : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
hm : m ≤ x.1
hn : n ≤ x.2
⊢ x.1 + x.2 = k

Tactic:
by simp_all

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ (Multiset.map Prod.fst s).prod n = 0

Tactic:
have := listProd_apply_eq_zero' (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
  simpa [← Multiset.prod_coe, ← Multiset.map_coe]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).reverse.prod = List.foldl (fun m n ↦ (f n) m) n l

Tactic:
← List.map_reverse,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l.reverse).prod = List.foldl (fun m n ↦ (f n) m) n l
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem
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
i : { n // ↑n = i' }
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ ↑i
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, ⋯⟩

Tactic:
obtain ⟨i, rfl⟩ := i

Goal state after:
case mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
hx : x ∈ (ι Q).range ^ ↑⟨i, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
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' : ZMod 2
x' : ↥(evenOdd Q i')
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑x' = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') x'

Tactic:
obtain ⟨x', hx'⟩ := x'
  dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
  induction hx' using Submodule.iSup_induction' with
  | mem i x hx =>
    obtain ⟨i, rfl⟩ := i
    dsimp only [Subtype.coe_mk] at hx
    induction hx using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
    | add x y i hx hy ihx ihy =>
      rw [map_add, ihx, ihy, ← map_add]
      rfl
    | mem_mul m hm i x hx ih =>
      obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
      refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
        dsimp only [GradedMonoid.mk, Subtype.coe_mk]
      · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
      rfl
  | zero =>
    rw [map_zero]
    apply Eq.symm
    apply DFinsupp.single_eq_zero.mpr; rfl
  | add x y hx hy ihx ihy =>
    rw [map_add, ihx, ihy, ← map_add]; rfl

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
⊢ M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)

Tactic:
by apply GradedAlgebra.ι Q

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

Goal state before:

Tactic:
⨆ (i : ZMod 2) (j : { n : ℕ // ↑n = i }), LinearMap.range (ι Q) ^ (j : ℕ) =
        ⨆ i : Σ i : ZMod 2, { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (i.2 : ℕ) := by
      rw [iSup_sigma]
    _ = ⨆ i : ℕ, LinearMap.range (ι Q) ^ i :=
      Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl

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

Goal state before:
pp: case h
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hfg : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ (hom (F.map f)) ⟨x.fst, r • x.snd⟩.snd = (hom (F.map g)) ⟨y.fst, r • y.snd⟩.snd

Tactic:
simp [hfg]

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

Goal state before:
pp: case succ
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 + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext Y S.X₁ (i + 1)
⊢ x₃ = 0

Tactic:
· obtain ⟨x₁, rfl⟩ := Ext.covariant_sequence_exact₁ _ hS x₃
      (Ext.eq_zero_of_hasInjectiveDimensionLT _ (n + 1) hi) rfl
    rw [x₁.eq_zero_of_hasInjectiveDimensionLT n (by lia), Ext.zero_comp]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
| Submodule.span R (range ⇑(ιMulti R n))

Tactic:
← Set.image_univ

Goal state after:
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
hf : Surjective ⇑f
| Submodule.span R (⇑(ιMulti R n) '' univ)
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat R
f : X ⟶ Y
g : Y ⟶ Z
x✝ : ↑(X.localizedModule S)
⊢ (Hom.hom (localizedModuleMap S (f ≫ g))) x✝ = (Hom.hom (localizedModuleMap S f ≫ localizedModuleMap S g)) x✝

Tactic:
simp [IsLocalizedModule.map_comp' S _ (Y.localizedModuleMkLinearMap S)]

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 D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsCofilteredOrEmpty C

Tactic:
suffices IsFilteredOrEmpty Cᵒᵖ from isCofilteredOrEmpty_of_isFilteredOrEmpty_op _

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsFilteredOrEmpty Cᵒᵖ
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)

pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
· intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)

pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'

Tactic:
· intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'
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)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)

Tactic:
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
  haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimit_of_iso i
  trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
  · apply HasLimit.isoOfNatIso i
  · exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C₁
inst✝ : Category.{v_3, u_3} C₂
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₀₂ : C₀ ⥤ C₂
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₂₀ : C₂ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂) (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv = e₀₁₂.hom

Tactic:
by
  dsimp only [leftAdjointCompIso]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G : Subfunctor F✝
U✝ V✝ : C
x✝¹ : U✝ ⟶ V✝
x✝ : F✝.obj U✝
h : x✝ ∈ G.obj U✝
⊢ x✝ ∈ ⇑(hom (F✝.map x✝¹)) ⁻¹' (F.obj V✝ ⊔ G.obj V✝)

Tactic:
exact Or.inr (G.map _ h)

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₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)) (m : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) (a • m) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n =
      a • (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n

Tactic:
by intro a m₁ m₂; dsimp; erw [M₁.map_smul]; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ ⊥.Covers S f ↔ S.arrows f

Tactic:
covers_iff,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ Sieve.pullback f S ∈ ⊥ Y ↔ S.arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)

Tactic:
funext W

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
⊢ pullbackArrows f (singleton g) = singleton (pullback.snd g f)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
x : { x // (hom g) x = (hom h) x }
⊢ (hom (↾Subtype.val ≫ g)).toFun x = (hom (↾Subtype.val ≫ h)).toFun x

Tactic:
exact x.prop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = Exists.choose ⋯

Tactic:
intro s Fs HFs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
⊢ Fs = Exists.choose ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S.arrows f ∧ R.arrows f → ∀ (g : Z ⟶ Y), S.arrows (g ≫ f) ∧ R.arrows (g ≫ f)

Tactic:
by
    rintro _ _ _ ⟨h₁, h₂⟩ g
    simp [h₁, h₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩)) z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext
  rintro ⟨⟨Y, Z, g, f, hf⟩⟩
  apply h

Goal state after: