mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case pos
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : i = i' ∧ j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

pp: case neg
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
· simp [LinearMap.toMatrix_apply, hij]

Goal state after:
case neg
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : (RingHom.id R) (vi i) • (B (v i)) (v i) = 0
⊢ vi i = 0

Tactic:
cases smul_eq_zero.mp hB
    · assumption
    · specialize h i
      contradiction

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K V₁ ≤ finrank K ↥(LinearMap.ker f) + finrank K ↥p

Tactic:
← finrank_ker_add_one_of_ne_zero hf,

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K ↥(LinearMap.ker f) + 1 ≤ finrank K ↥(LinearMap.ker f) + finrank K ↥p
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
⊢ kernel.ι (prod.lift f g) ≫ g = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ prod.snd

Tactic:
rw [prod.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasCoequalizers C
inst✝² : HasFiniteCoproducts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteCoproducts G
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J G

Tactic:
intro J sJ fJ
    apply preservesColimit_of_preservesCoequalizers_and_coproduct

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f g : X ⟶ Y
huv : pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
⊢ pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f =
    pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ prod.lift (𝟙 X) f ≫ prod.snd

Tactic:
rw [prod.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f g : X ⟶ Y
huv : pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
⊢ pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ prod.lift (𝟙 X) g ≫ prod.snd =
    pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g

Tactic:
rw [prod.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
⊢ g ≫ cokernel.π (coprod.desc f g) = coprod.inr ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g)

Tactic:
rw [coprod.inr_desc_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ coprod.inr ≫ coprod.desc f g ≫ b ≫ s.inr = g ≫ b ≫ s.inr

Tactic:
rw [coprod.inr_desc_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Biproducts

Goal state before:
pp: J : Type w
f : J → AddCommGrpCat
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (x + y)) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y

Tactic:
by
      simp only [Functor.const_obj_obj, map_add]
      rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk

Tactic:
by
  simp only [← cancel_epi h.p, p_comp_opcyclesIso_inv_assoc, p_descOpcycles, p_descQ]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

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
G : D ⥤ C
adj : F ⊣ G
inst✝² : G.Full
inst✝¹ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
⊢ ∃ h, g ≫ h = f

Tactic:
have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits

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
G : D ⥤ C
adj : F ⊣ G
inst✝² : G.Full
inst✝¹ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
⊢ ∃ h, g ≫ h = f
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.PreservesMonomorphisms
X : D
I : InjectivePresentation X
⊢ Mono (G.map I.f)

Tactic:
have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.PreservesMonomorphisms
X : D
I : InjectivePresentation X
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
⊢ Mono (G.map I.f)
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝² : HasZeroObject C
this✝¹ : Mono S.f
this✝ : Epi S.g
hX₃ : IsZero S.X₃
this : Epi S.f
⊢ IsIso S.f

Tactic:
apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝² : HasZeroObject C
this✝¹ : Mono S.f
this✝ : Epi S.g
hX₁ : IsZero S.X₁
this : Mono S.g
⊢ IsIso S.g

Tactic:
apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝⁴ : Mono S₁.f
this✝³ : Mono S₂.f
this✝² : Epi S₁.g
this✝¹ : Epi S₂.g
this✝ : Mono φ.τ₂
this : Epi φ.τ₂
⊢ IsIso φ.τ₂

Tactic:
apply isIso_of_mono_of_epi

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ Function.Surjective ⇑S.abToCycles

Tactic:
rw [S.abLeftHomologyData.exact_iff_epi_f', abLeftHomologyData_f',
    AddCommGrpCat.epi_iff_surjective]

Goal state after:
S : ShortComplex Ab
⊢ Function.Surjective ⇑(ConcreteCategory.hom (AddCommGrpCat.ofHom S.abToCycles)) ↔ Function.Surjective ⇑S.abToCycles
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology

Tactic:
rintro ⟨e⟩
    exact IsZero.of_iso (isZero_zero C) e

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
j : C ⥤ D
inst✝¹ : Coreflective j
A : D
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
this : IsIso (ε.app (j.obj ((coreflector j).obj A)))
⊢ j.essImage A

Tactic:
have : Mono (ε.app A) := by
    refine @mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_
    rw [show ε.app A ≫ section_ _ = _ from (ε.naturality (section_ (ε.app A))).symm]
    apply mono_comp _ (ε.app (j.obj ((coreflector j).obj A)))

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
j : C ⥤ D
inst✝¹ : Coreflective j
A : D
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
this✝ : IsIso (ε.app (j.obj ((coreflector j).obj A)))
this : Mono (ε.app A)
⊢ j.essImage A
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : Epi (imageToKernel S.f S.g ⋯)
⊢ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
apply isIso_of_mono_of_epi

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ Nonempty (Cone F)
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv =
    ((Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv

Tactic:
simp only [Category.assoc, Iso.hom_inv_id]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ 𝟙 (((evaluation C D).obj X).obj (cokernel α)) =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫
      cokernel.π (α.app X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)

Tactic:
rw [YonedaCollection.mk_fst]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
⊢ PreservesLimit H colim

Tactic:
have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
⊢ PreservesLimit H colim
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.PreservesHomology

pp: case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.Additive

Tactic:
· exact preservesHomology_of_preservesMonos_and_cokernels _

Goal state after:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasColimitsOfShape J C
inst✝ : colim.PreservesMonomorphisms
⊢ colim.Additive
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
h₁ : ((uliftYonedaAdjunction L α).homEquiv P (L.obj P)) (𝟙 (L.obj P)) = (uliftYonedaAdjunction L α).unit.app P
⊢ (hom (((uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) }

Tactic:
simp [← h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) [inst : Mono f]
    {q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T}
    (hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f

Tactic:
by
      intro P f hf q hq
      fapply Subobject.mk_eq_mk_of_comm
      · refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
        · exact (Subobject.underlyingIso f.unop.left.op).unop
        · refine (cancel_epi (S.map f.unop.left)).1 ?_
          simpa [← Category.assoc, ← S.map_comp] using hq
      · exact Quiver.Hom.unop_inj (by simp)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv (p ≫ presheafHom φ P ≫ F.op.whiskerLeft (G.map f)) = uliftYonedaEquiv (p ≫ f ≫ presheafHom φ Q)

Tactic:
rw [← assoc p f, uliftYonedaEquiv_ι_presheafHom, ← assoc,
      uliftYonedaEquiv_comp, uliftYonedaEquiv_ι_presheafHom,
      Functor.map_comp]
    dsimp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
s : ∏ᶜ Subtype.val ⟶ ∏ᶜ P.productToFamily A := Pi.lift fun f ↦ Pi.π Subtype.val ⟨f.right.obj, ⋯⟩
⊢ Subobject.underlying.obj ⊥ ⟶ A

Tactic:
exact Subobject.ofLEMk _
      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
Q : Type v
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : Q ≃ₗ[R] M
h : Baer R Q
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] Q
h' : ∀ (x : R) (mem : x ∈ I), g' x = (↑e.symm ∘ₗ g) ⟨x, mem⟩
⊢ ∀ (x : R) (mem : x ∈ I), (↑e ∘ₗ g') x = g ⟨x, mem⟩

Tactic:
simpa [LinearEquiv.eq_symm_apply] using h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑↑n * c) = 0

Tactic:
rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Tactic:
by
  simp only [sub_mem_Ioc_iff_right, sub_self, sub_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : b ^ m < b ^ (n + 1)
i2 : b ^ n < b ^ (m + 1)
⊢ m = n

Tactic:
zpow_lt_zpow_iff_right hb,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m < n + 1
i2 : n < m + 1
⊢ m = n
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℕ
⊢ f (x - n • c) = (-1) ^ n • f x

Tactic:
by
  simpa only [Int.reduceNeg, natCast_zsmul] using! h.sub_zsmul_eq n

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : b ^ m < b ^ (n + 1)
i2 : b ^ n < b ^ (m + 1)
⊢ m = n

Tactic:
zpow_lt_zpow_iff_right hb,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m < n + 1
i2 : n < m + 1
⊢ m = n
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }

Tactic:
rw [count_eq_card_filter_range, Fintype.card_of_subtype]
  simp

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n d : ℕ
hnd : d ∣ n
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
rcases d.eq_zero_or_pos with (rfl | hd0); · simp [eq_zero_of_zero_dvd hnd]
  rcases hnd with ⟨x, rfl⟩
  rw [Nat.mul_div_cancel_left x hd0]
  apply Finset.card_bij fun k _ => d * k
  · simp only [mem_filter, mem_range, and_imp, Coprime]
    refine fun a ha1 ha2 => ⟨by gcongr, ?_⟩
    rw [gcd_mul_left, ha2, mul_one]
  · simp [hd0.ne']
  · simp only [mem_filter, mem_range, exists_prop, and_imp]
    intro b hb1 hb2
    have : d ∣ b := by
      rw [← hb2]
      apply gcd_dvd_right
    rcases this with ⟨q, rfl⟩
    refine ⟨q, ⟨⟨(mul_lt_mul_iff_right₀ hd0).1 hb1, ?_⟩, rfl⟩⟩
    rwa [gcd_mul_left, mul_eq_left hd0.ne'] at hb2

Goal state after: