mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (algebraMap A B) ((aeval x) p) = 0 ↔ (aeval x) p = 0

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval x) p • 1 = 0 ↔ (aeval x) p = 0
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type w₂
inst✝¹ : Category.{w₁, w₂} C
inst✝ : IsPreconnected J
X Y : C
α : (const J).obj X ⟶ (const J).obj Y
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ α.app x✝¹ = α.app x✝

Tactic:
by
    simpa using (α.naturality f).symm

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.left
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ Surjective ⇑((↑e).comp f)

Tactic:
rw [AlgHom.coe_comp]
    exact Function.Surjective.comp e.surjective hf.1

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
by rwa [isoClosure_le_iff]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure ≤ P

Tactic:
by rwa [isoClosure_le_iff]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
this : ∀ (i : ↥t), ∃ a, f a = (algebraMap A B) ↑i
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG

Tactic:
choose t' ht' using this

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ ((pre F G.functor).map
          (eqToHom ⋯ ≫
            ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                    (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                X ≫
              (𝟙
                    (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                      pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                X) ≫
        (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).base =
    (𝟙 ((pre F G.functor).obj X)).base

Tactic:
simp [preNatIso, transportIso]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
X : Grothendieck (G.functor ⋙ F)
⊢ eqToHom ⋯ ≫
      ((pre F G.functor).map
            (eqToHom ⋯ ≫
              ((map (G.functor.whiskerLeft (whiskerRight G.counitInv F))).whiskerLeft
                      (preNatIso (G.functor ⋙ F) G.unitIso.symm).symm.hom).app
                  X ≫
                (𝟙
                      (map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙
                        pre (G.functor ⋙ F) (G.functor ⋙ G.inverse))).app
                  X) ≫
          (preNatIso F G.counitIso.symm).symm.hom.app ((pre F G.functor).obj X)).fiber =
    (𝟙 ((pre F G.functor).obj X)).fiber

Tactic:
simp [preNatIso, transportIso]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
⊢ Ideal.span ↑(Finset.image g' Finset.univ ∪ Finset.image (⇑aeval_h) s) = RingHom.ker f.toRingHom

Tactic:
simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
⊢ Ideal.span (Set.range g' ∪ ⇑aeval_h '' ↑s) = RingHom.ker f.toRingHom
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithTerminal C)ᵒᵖ).map (op f) ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithInitial.of (op x)
                  | star => WithInitial.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (down f).op
                  | op star, op (of a), x, x_2 =>
                    WithInitial.starInitial.to
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
                | WithInitial.star, WithInitial.of (op unop), x =>
                  op
                    (starTerminal.from
                      (Opposite.unop
                        (match WithInitial.of (op unop) with
                        | WithInitial.of x => op (of (Opposite.unop x))
                        | WithInitial.star => op star)))
                | WithInitial.star, WithInitial.star, x =>
                  𝟙
                    (match WithInitial.star with
                    | WithInitial.of x => op (of (unop x))
                    | WithInitial.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        (op f)

Tactic:
by
            simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]
            rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (s : Fork (k ≫ hr.left) (k ≫ hr.right)) →
    { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }

Tactic:
intro s

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ { l // l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ y✝ : (WithInitial C)ᵒᵖ
f✝ : x✝ ⟶ y✝
x y : C
f : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithInitial C)ᵒᵖ).map f ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                  | op (of a), op star, x, x_2 =>
                    WithTerminal.starTerminal.from
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
                | WithTerminal.of (op unop), WithTerminal.star, x =>
                  op
                    (starInitial.to
                      (Opposite.unop
                        (match WithTerminal.of (op unop) with
                        | WithTerminal.of x => op (of (Opposite.unop x))
                        | WithTerminal.star => op star)))
                | WithTerminal.star, WithTerminal.star, x =>
                  𝟙
                    (match WithTerminal.star with
                    | WithTerminal.of x => op (of (unop x))
                    | WithTerminal.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by
            simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]
            rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
c : C
hc : IsTerminal c
c' : C
⊢ IsConnected (StructuredArrow c' (fromPUnit c))

Tactic:
by
    let : Inhabited (StructuredArrow c' (fromPUnit c)) := ⟨.mk (Y := default) (hc.from c')⟩
    let : Subsingleton (StructuredArrow c' (fromPUnit c)) :=
      ⟨fun i j ↦ StructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩
    infer_instance

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

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
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
⊢ (pre X T S).Final

Tactic:
refine ⟨fun f => ?_⟩

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
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f (pre X T S))
Module: Mathlib.CategoryTheory.Limits.Final

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
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
⊢ (pre T S X).Initial

Tactic:
refine ⟨fun f => ?_⟩

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
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow (pre T S X) f)
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)) (m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt),
    (∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j) → m = small_k.lift s.fst s.snd ⋯

Tactic:
intro s

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
⊢ ∀ (m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt),
    (∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j) → m = small_k.lift s.fst s.snd ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (s : Cofork (gr.left ≫ f) (gr.right ≫ f)) →
    { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
intro s

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f'

Tactic:
· algebraize [f.hom, g.hom, f'.hom, g'.hom, f'.hom.comp g.hom]
    have : IsScalarTower R S S' := .of_algebraMap_eq fun x ↦ congr($(hsq.1.1).hom x)
    have : Algebra.IsPushout R S R' S' := (CommRingCat.isPushout_iff_isPushout.mp hsq).symm
    exact h (R := R) (S := S) _ _ hf

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝² : P.ContainsZero
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : Q.ContainsZero
⊢ ∃ Z, IsZero Z ∧ (P ⊓ Q) Z

Tactic:
by
    obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero
    exact ⟨Z, hZ, P.prop_of_isZero hZ, hQ⟩

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
j : Fin (n + 1)
⊢ (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
        { as := 0 } ≫
      (Iso.refl
          (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
            F.map
              (Fin.cases
                (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                (fun i ↦
                  (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                j)).ι.app
      { as := 0 }

Tactic:
apply Category.comp_id

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
by
  induction n <;> simp [pow_succ, *]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B)

Tactic:
simp [IsIso.inv_comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (snd A B) = snd (F.obj A) (F.obj B)

Tactic:
simp [IsIso.inv_comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ lift ((s.snd ≫ fst A A) ≫ ι) (lift (s.fst ≫ fst A A) (s.fst ≫ snd A A) ≫ μ) ≫ μ = s.snd ≫ snd A A

Tactic:
lift_inv_left_eq,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ lift (s.fst ≫ fst A A) (s.fst ≫ snd A A) ≫ μ = lift (s.snd ≫ fst A A) (s.snd ≫ snd A A) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ∀ (s : PullbackCone μ μ) (m : s.pt ⟶ (A ⊗ A) ⊗ A),
    m ≫ μ ▷ A = s.fst →
      m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
        m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)

Tactic:
intro s

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ ∀ (m : s.pt ⟶ (A ⊗ A) ⊗ A),
    m ≫ μ ▷ A = s.fst →
      m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
        m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv (antipode R) * toConv id).ofConv c = (ofConv 1) c

Tactic:
rw [(ℛ R c).convMul_apply]

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv id * toConv (antipode R)).ofConv c = (ofConv 1) c

Tactic:
rw [(ℛ R c).convMul_apply]

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c