mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
this : v ∈ ⊤
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v

Tactic:
← (isCompl_ker_of_disjoint_of_ne_bot hf hpf hp).sup_eq_top,

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
v : V₁
this : v ∈ LinearMap.ker f ⊔ p
⊢ ∃ y ∈ LinearMap.ker f, ∃ z ∈ p, y + z = v
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Surjective ⇑f ∧ Function.Injective ⇑f ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
and_comm

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
← dualMap_injective_iff

Goal state after:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₂
⊢ Injective ⇑B.flip ↔ Injective ⇑B.dualMap
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Surjective ⇑B ∧ Injective ⇑B ↔ Injective ⇑B ∧ Surjective ⇑B

Tactic:
and_comm

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
⊢ ⊤ ≤ span K (Set.range fun x ↦ id ↑x)

Tactic:
by
    simpa using hli.span_extend_eq_span <| Set.subset_univ _

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

Goal state before:
pp: A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' f.range
⊢ (QuotientGroup.mk' f.range).ker = ker 1

Tactic:
rw [h]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b1 b2 : ↑B
⊢ { toFun := fun x ↦ (b1 * b2) • x, invFun := fun x ↦ (b1 * b2)⁻¹ • x, left_inv := ⋯, right_inv := ⋯ } =
    { toFun := fun x ↦ b1 • x, invFun := fun x ↦ b1⁻¹ • x, left_inv := ⋯, right_inv := ⋯ } *
      { toFun := fun x ↦ b2 • x, invFun := fun x ↦ b2⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }

Tactic:
ext
    simp [mul_smul]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
⊢ QuasiIso φ'

Tactic:
let α : S₃ ⟶ S₁ := e.inv.left
  let β : S₂ ⟶ S₄ := e.hom.right
  suffices φ' = α ≫ φ ≫ β by
    rw [this]
    infer_instance
  simp only [α, β, Arrow.w_mk_right_assoc, Arrow.mk_hom,
    ← Arrow.comp_right, e.inv_hom_id, Arrow.id_right, comp_id]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ z ≫ homologyMap φ = 𝟙 S₂.homology

Tactic:
rw [← cancel_epi S₂.homologyπ, reassoc_of% hz, homologyπ_naturality,
      IsIso.inv_hom_id_assoc, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b c : S₁ ⟶ S₂
⊢ a + b + c = a + (b + c)

Tactic:
by ext <;> apply add_assoc

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ IsColimit (CokernelCofork.ofπ π ⋯)

Tactic:
by
    refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsCokernel
    · exact parallelPair.ext (Iso.refl _) (S.isoCyclesOfIsLimit hkf)
    · exact Cofork.ext (isoHomology S hkf hcc fac) (by simp [Cofork.π])

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0

Tactic:
zero_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀ + 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact → S₂.Exact

Tactic:
rintro ⟨h₁, z₁⟩
    exact ⟨HomologyData.ofEpiOfIsIsoOfMono φ h₁, z₁⟩

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact

Tactic:
rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h

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
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.leftHomologyData.H = 0
⊢ (S.map F).Exact
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mpr
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range

Tactic:
rw [h]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ S.Exact

Tactic:
(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        inferInstance (isZero_zero C))).exact_iff

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
a✝ : Mono S.g
⊢ IsZero
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι 0 ⋯) ⋯ ⋯)).left.H
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
| _ a b
   => 

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)
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 ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

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 (IsLimit (KernelFork.ofι S.f ⋯)) → S.Exact ∧ Mono S.f

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

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 (IsLimit (KernelFork.ofι S.f ⋯)) → S.Exact ∧ Mono S.f
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h

Tactic:
by
  dsimp [factorThruKernelSubobject]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X ≫ (L.colimitIsoColimitGrothendieck G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
      { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) }

Tactic:
by
  rw [← Iso.eq_comp_inv]
  exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

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
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
rw [h]

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
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g))

Tactic:
rw [h]

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 : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (yonedaEquiv.symm (yonedaEquiv s)))

Tactic:
rw [Equiv.symm_apply_apply]

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 : C
p q : YonedaCollection F X
h : p.fst = q.fst
⊢ op (CostructuredArrow.mk q.fst) = op (CostructuredArrow.mk p.fst)

Tactic:
rw [h]

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 : C
s : yoneda.obj X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s

Tactic:
simpa [YonedaCollection.yonedaEquivFst_eq] using p.app_val

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (L ⋙ L.pointwiseRightKanExtension F).map f ≫
      limit.π (StructuredArrow.proj (L.obj X₂) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f

Tactic:
by
    simp only [comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]
    rw [comp_id]
    let φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) :=
      StructuredArrow.homMk f
    exact (limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
⊢ HasExactColimitsOfShape J D

Tactic:
refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesLimit K colim
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
⊢ HasExactLimitsOfShape J D

Tactic:
refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesColimit K lim
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
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map f ≫
      WalkingParallelFamily.casesOn j ι (ι ≫ f✝ (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f✝ (Classical.arbitrary J)) ≫ (parallelFamily f✝).map f

Tactic:
obtain - | k := f
        · simp
        · simp [w (Classical.arbitrary J) k]

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
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f✝ j₁ ≫ π = f✝ j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ (parallelFamily f✝).map f ≫ WalkingParallelFamily.casesOn j (f✝ (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn i (f✝ (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map f

Tactic:
obtain - | k := f
        · simp
        · simp [w (Classical.arbitrary J) k]

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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
by
  conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op g.unop.left]
  rw [← unop_comp]
  simp only [Subobject.ofMkLEMk_comp, Quiver.Hom.unop_op]

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

Goal state before:
pp: 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
⊢ HasInitial C

Tactic:
have := hasProductsOfShape_of_small C (Subtype P)

Goal state after:
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
⊢ HasInitial C
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D

Tactic:
have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj (op G)).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

Tactic:
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
    exact hf h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₁ = F i₂

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) →
    Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
rintro ⟨h⟩
      rw [← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,
        ← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]
      dsimp [binaryCoproductCocone]
      refine
        ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩
      rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp]
      dsimp
      rw [Set.range_comp _ Sum.inr, ← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
      simp

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

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) (n • m) = g ⟨n • m, hn⟩

Tactic:
rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a b m n✝ p : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
⊢ motive (k + 2)

Tactic:
letI p := (k + 2).minFac

Goal state after:
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
⊢ motive (k + 2)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inl
m n : ℕ
h : φ m = 1
⊢ (φ m).Coprime (φ n)

Tactic:
rw [h]

Goal state after:
case mpr.inl
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime (φ n)

Tactic:
rw [h]

Goal state after:
case mpr.inr
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
← prod_factorization_pow_eq_self hn

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) * ∏ p ∈ n.primeFactors, p =
    (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)

Tactic:
rw [← one_mul (_ ^ _ : ℕ)]

Goal state after:
case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 1 * (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2)! * (c ^ 2 + 1) ^ (c ^ 2 + d' + d + 1)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Tactic:
by
  rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
⊢ univᶜ ∈ T

Tactic:
simp [empty_mem]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Set β
h : Set β → Filter γ
hg : Monotone g
hh : Monotone h
⊢ (f.lift fun s ↦ (𝓟 (g s)).lift h) = f.lift fun s ↦ h (g s)

Tactic:
by simp only [lift_principal, hh]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ 𝓟 univ = ⊤

Tactic:
principal_univ

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b ≠ toIocMod hp a b → ¬∃ x, b - x • p ∈ Set.Ioo a (a + p)

Tactic:
not_imp_not

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ x, b - x • p ∈ Set.Ioo a (a + p)) → toIcoMod hp a b = toIocMod hp a b