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

Goal state before:
pp: case tmul
R : Type u_1
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
z : M ⊗[R] N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) z

Tactic:
induction z

Goal state after:
case tmul.zero
R : Type u_1
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
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) 0

case tmul.tmul
R : Type u_1
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
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ ⊗ₜ[R] y✝)

case tmul.add
R : Type u_1
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
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) x✝
a✝ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) y✝
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ + y✝)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
⊢ g = 0

Tactic:
let h := hu.g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
⊢ g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
⊢ g = 0

Tactic:
let h := hu.g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
⊢ g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (0 - a - b) = b + a

Tactic:
conv_lhs =>
    congr
    next => skip
    rw [← neg_def, neg_sub]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - 0 - (-b - a) = b + a
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv

Tactic:
← cancel_mono e₂.hom,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ (e₁.inv ≫ S₁.f) ≫ e₂.hom = (S₂.f ≫ e₂.inv) ≫ e₂.hom
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    ext
    simp

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b1 b2 : ↑B
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    ext
    simp

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
⊢ g ≠ h

Tactic:
intro r
  apply fromCoset_ne_of_nin_range _ hx
  replace r :=
    DFunLike.congr_fun (DFunLike.congr_fun r x) (fromCoset ⟨f.hom.range, ⟨1, one_leftCoset _⟩⟩)
  simpa [g_apply_fromCoset, «h», tau, g_apply_infinity] using r

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasZeroMorphisms C
K X Y : C
i : K ⟶ X
f : X ⟶ Y
w : i ≫ f = 0
h : IsLimit (KernelFork.ofι i w)
Z'✝ : Cᵒᵖ
x : op X ⟶ Z'✝
hx : f.op ≫ x = 0
b : op K ⟶ Z'✝
hb : i.op ≫ b = x
⊢ b.unop ≫ Fork.ι (KernelFork.ofι i w) = (h.lift (KernelFork.ofι x.unop ⋯)).op.unop ≫ Fork.ι (KernelFork.ofι i w)

Tactic:
by
      simpa only [Quiver.Hom.unop_op, Fork.IsLimit.lift_ι] using! Quiver.Hom.op_inj hb

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = leftRightHomologyComparison' h.left h.right

Tactic:
leftRightHomologyComparison'_eq

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
⊢ h.iso.hom = h.iso.hom
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯) =
    (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯)

Tactic:
trans F.map (hₗ.i ≫ hᵣ.p)

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
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯) =
    F.map (hₗ.i ≫ hᵣ.p)

C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) =
    (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : S.g ≫ s.s = S.g ≫ s'.s
⊢ s = s'

Tactic:
cancel_epi S.g

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : s.s = s'.s
⊢ s = s'
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
W'✝ : C
x : W'✝ ⟶ S.X₂
x✝ : x ≫ S.g = 0
b : W'✝ ⟶ S.X₁
hb : b ≫ S.f = x
⊢ b = x ≫ s.r

Tactic:
simp only [← hb, assoc, f_r, comp_id]

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

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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
⊢ S.RightHomologyData

Tactic:
have hι : IsLimit (KernelFork.ofι 0 wι) := KernelFork.IsLimit.ofMonoOfIsZero _
      (by rw [hg']; dsimp; infer_instance) (isZero_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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
hι : IsLimit (KernelFork.ofι 0 wι)
⊢ S.RightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
by
    have eq := e.inv.τ₂ ≫= s.id =≫ e.hom.τ₂
    rw [id_comp, ← comp_τ₂, e.inv_hom_id, id_τ₂] at eq
    rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
X : Subobject B
h₁ : mk f ≤ mk g
h₂ : mk g ≤ X
⊢ ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X ⋯

Tactic:
by
  simp only [ofMkLE, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
    assoc, Iso.hom_inv_id_assoc]
  congr 1

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g

Tactic:
· intro ⟨hS, _⟩
    exact ⟨hS.gIsCokernel⟩

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ ((MonoOver.forget Y).obj a).hom) ≫ h =
    pullback.snd ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ k

Tactic:
rw [← pullback.condition, assoc]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
exact ⟨Subobject.ofLE _ _ h.ge, by ext; simp, by ext; simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
have eq₂ := IsColimit.comp_coconePointUniqueUpToIso_hom (cokernelIsCokernel S.f) hf (.one)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
eq₂ :
  (Cofork.ofπ (cokernel.π S.f) ⋯).ι.app WalkingParallelPair.one ≫
      ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom =
    cf.ι.app WalkingParallelPair.one
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α → F''.IsRightKanExtension α'

Tactic:
intro
    exact isRightKanExtension_of_iso e α α' comm

Goal state after:
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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).fst = yoneda.map f ≫ p.fst

Tactic:
by
  simp [map₂]

Goal state after:
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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)

Tactic:
YonedaCollection.map₂_fst f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (yoneda.map f ≫ p.fst))
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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).snd = (ConcreteCategory.hom (F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom ⋯))) p.snd

Tactic:
by
  simp [map₂]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
⊢ HasKernel f

Tactic:
by
      have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by
        simpa using NatIso.naturality_1 i f
      rw [← this]
      have : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
      apply Limits.hasKernel_iso_comp

Goal state after:
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))), naturality := ⋯ }

Tactic:
ext X x
    simp only [functorToRepresentables_obj, coconeOfRepresentable_pt, Functor.const_obj_obj,
      coconeOfRepresentable_ι_app, Functor.leftOp_obj, CategoryOfElements.π_obj, op_unop,
      TypeCat.Fun.toFun_apply, hom_ofHom, TypeCat.Fun.coe_mk] at hm ⊢
    rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app zero ≫ f (Classical.arbitrary J) = l ≫ s.π.app zero ≫ f (Classical.arbitrary J)

Tactic:
reassoc_of% h

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ l ≫ s.ι ≫ f (Classical.arbitrary J) = l ≫ s.π.app zero ≫ f (Classical.arbitrary J)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Tactic:
· simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
      ofLE_arrow, factorThru_arrow]

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk :
  (ConcreteCategory.hom (S.X₃.map e₁)) ((ConcreteCategory.hom (S.g.app j)) y) = (ConcreteCategory.hom (S.X₃.map e₂)) 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply]
      at hk

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case fst
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).1 = (p, q).1

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget CommGrpCat.{u}) G H) (p, q)

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else ⋯.choose) ^ n✝ = a

Tactic:
by
    dsimp only
    rw [dif_neg hn]
    exact (H hn a).choose_spec

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

Goal state before:
pp: k : ℤ
⊢ (2 * k + 1).negOnePow = -1

Tactic:
simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

Goal state after:
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:
count_eq_card_filter_range,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) = Fintype.card { k // k < n ∧ p k }
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
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
rw [ExtensionOfMaxAdjoin.extensionToFun_wd (y := y) i f h (a + b) _ _ eq1,
          LinearPMap.map_add, map_add]

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
a b : ↥(supExtensionOfMaxSingleton i f y)
eq1 :
  ↑a + ↑b =
    ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
      (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
        ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i b) +
      ((ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) +
        (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i b)) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = count p a

Tactic:
count_eq_card_filter_range,

Goal state after:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = {x ∈ Finset.range a | p x}.card
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ Even (φ n)

Tactic:
rw [← ZMod.card_units_eq_totient, even_iff_two_dvd, this]
    exact orderOf_dvd_card

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

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

Tactic:
simp [eq_zero_of_zero_dvd hnd]

Goal state after: