mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
Z : ObjectProperty C
x✝⁵ x✝⁴ x✝³ : Z.FullSubcategory
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ + x✝) = x✝² ≫ x✝¹ + x✝² ≫ x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : J → (Q ⟶ R)
h : R ⟶ S
⊢ (∑ j ∈ s, f j ≫ g j) ≫ h = ∑ j ∈ s, f j ≫ g j ≫ h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'

Tactic:
comp_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : -g ≫ f = g' ≫ (-f)
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : -g ≫ f = g' ≫ (-f)
⊢ g = g'

Tactic:
comp_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : -g ≫ f = -g' ≫ f
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 * f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ f * 0 = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
⊢ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero c.pt
R✝ : C
g : Y ⟶ R✝
hg : f ≫ g = 0
⊢ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso g
⊢ f ≫ g = 0 ↔ f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ (f - g) = c.ι ≫ 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ : s.pt ⟶ (forkOfKernelFork c).pt
h : m✝ ≫ (forkOfKernelFork c).ι = s.ι
⊢ m✝ = i.lift (kernelForkOfFork s)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ : s.pt ⟶ (kernelForkOfFork c).pt
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = s.ι
⊢ m✝ = i.lift (forkOfKernelFork s)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ (f - g) ≫ c.π = 0 ≫ c.π

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m✝ = s.π
⊢ m✝ = i.desc (cokernelCoforkOfCofork s)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ : (cokernelCoforkOfCofork c).pt ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = s.π
⊢ m✝ = i.desc (coforkOfCokernelCofork s)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ (↑a • e.hom) ≫ (↑a⁻¹ • e.inv) = 𝟙 X

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ (↑a⁻¹ • e.inv) ≫ (↑a • e.hom) = 𝟙 Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteLimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasLimitsOfShape J C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasLimitsOfShape J C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteColimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasColimitsOfShape J C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape J C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ [zero, one].toFinset

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    x ∈
      WalkingParallelPair.recOn j
        (WalkingParallelPair.recOn j' [WalkingParallelPairHom.id zero].toFinset [left, right].toFinset)
        (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteLimits C
⊢ HasEqualizers C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
⊢ HasCoequalizers C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ Finset (j ⟶ j')

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j' (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
        if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j (Option.casesOn j' {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
        if h : some j = j' then ⋯.mpr {Hom.id j'} else ∅

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteLimits C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
x : WalkingPair
⊢ x ∈ {WalkingPair.left, WalkingPair.right}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePullbacks C
⊢ HasPullbacks C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePushouts C
⊢ HasPushouts C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
⊢ HasLimitsOfShape (Discrete ι) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
⊢ HasColimitsOfShape (Discrete ι) C

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
J : ℕ
⊢ HasColimitsOfShape (Discrete (Fin J)) C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
X : C
inst✝ : Nonempty C
⊢ ⊤ (Classical.arbitrary C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
⊢ (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q : ObjectProperty C
X : C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ (P ⊔ Q).IsClosedUnderIsomorphisms

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ ∀ {X Y : C} (x : X ≅ Y), ⊤ X → ⊤ Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
⊢ (⨆ a, P a) X ↔ ∃ a, P a X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure = ⨆ a, (P a).isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
inst✝ : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
⊢ (⨆ a, P a).IsClosedUnderIsomorphisms

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
inst✝ : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : (⨅ a, P a) X✝
⊢ (⨅ a, P a) Y✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ¬P = ⊥ ↔ ∃ X, P X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.Nonempty ↔ ¬P = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ¬P.Nonempty ↔ P = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteLimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
⊢ PreservesLimitsOfShape (Discrete J) F

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
⊢ PreservesLimitsOfShape (Discrete J) F
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
⊢ PreservesLimitsOfShape (Discrete J) F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteColimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesColimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsColimitsOfShape J F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
hY : P Y
e : X ≅ Y
⊢ ⊤ { obj := Y, property := hY }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ⊤.map P.ι = P.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ NPow.npow = NPow.npow

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
⊢ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toLeftCancelMonoid M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toRightCancelMonoid M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toCommMonoid M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ ZPow.zpow = ZPow.zpow

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : ZPow.zpow = ZPow.zpow
⊢ Div.div = Div.div

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
⊢ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toDivInvMonoid G)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toGroup G)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ Fork.ι s ≫ f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ s.π.app one = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ ι ≫ f = ι ≫ 0

Tactic:
by

Goal state after: