mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (a ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)) ∪
        Set.range ⇑(Hom.hom (b ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)))

Tactic:
IsPushout.inl_isoIsPushout_inv,

Goal state after:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst✝¹ : Algebra ↑R ↑A := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑B := (Hom.hom g).toAlgebra
e : ↑(of (↑A ⊗[↑R] ↑B)) ≃+* ↑X := (IsPushout.isoIsPushout A B ⋯ H).commRingCatIsoToRingEquiv
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range ⇑(Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom)) ∪
        Set.range ⇑(Hom.hom (b ≫ (IsPushout.isoIsPushout A B ⋯ H).inv)))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂) (f₁ m) = s • mk' f₂ m ⟨↑s, ⋯⟩

Tactic:
rw [liftOfLE, lift_apply]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ f₂ m = s • mk' f₂ m ⟨↑s, ⋯⟩
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
i : J
⊢ IsUnit ((ConcreteCategory.hom (c.π.app i)) x)

Tactic:
obtain ⟨k, f, g, lh, eq⟩ := hj x hx i

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
x : ↑c.pt
hx : IsUnit ((Hom.hom (c.π.app j)) x)
i k : J
f : i ⟶ k
g : j ⟶ k
lh : IsLocalHom (Hom.hom (F.map f))
eq :
  (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
    (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
⊢ IsUnit ((ConcreteCategory.hom (c.π.app i)) x)
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
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : V.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : V.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ U.hom ≫ F.map (StructuredArrow.Hom.right h ≫ q₁) = f ≫ Final.homToLift F Y ≫ F.map q₂

Tactic:
simp only [F.map_comp, StructuredArrow.w_assoc, hq]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).fst = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).fst

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).snd

Tactic:
· apply m₁.trans (big_k.isLimit.fac s' WalkingCospan.left).symm

Goal state after:
case refine_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ IsKernelPair (pullback.fst f g) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)

Tactic:
by
  refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩
  · simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
  · simp only [assoc, lift_fst_assoc, pullback.condition]
  · ext <;> simp
  · ext
    · simp [s.condition]
    · simp
  · apply pullback.hom_ext
    · simpa using hm WalkingCospan.left =≫ pullback.fst f g
    · apply PullbackCone.IsLimit.hom_ext h.isLimit
      · simpa using hm WalkingCospan.left =≫ pullback.snd f g
      · simpa using hm WalkingCospan.right =≫ pullback.snd f g

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : inv a ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f

Tactic:
IsIso.inv_comp_eq,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a ≫ 𝟙 X
⊢ Mono f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
refine ⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x✝¹⁰ : CommRing R
x✝⁹ : CommRing S
x✝⁸ : CommRing R'
x✝⁷ : CommRing S'
x✝⁶ : Algebra R S
x✝⁵ : Algebra R R'
x✝⁴ : Algebra R S'
x✝³ : Algebra S S'
x✝² : Algebra R' S'
x✝¹ : IsScalarTower R S S'
x✝ : IsScalarTower R R' S'
hsq : Algebra.IsPushout R S R' S'
hRS : (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R' S')

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'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderLimitsOfShape J → W.limitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩
    exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
⊢ W.IsStableUnderColimitsOfShape J → W.colimitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩
    exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
⊢ W α

Tactic:
have : HasColimit X₁ := ⟨c₁, hc₁⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : W.RespectsIso
hW :
  ∀ (X₁ X₂ : J → C) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)
X₁ X₂ : Discrete J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory (Discrete J) f
α : c₁.pt ⟶ c₂.pt
hα : ∀ (j : Discrete J), c₁.ι.app j ≫ α = f.app j ≫ c₂.ι.app j
φ : (j : J) → X₁.obj { as := j } ⟶ X₂.obj { as := j } := fun j ↦ f.app { as := j }
this : HasColimit X₁
⊢ W α
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P.diagonal (e.hom ≫ f)

Tactic:
rwa [diagonal_iff, pullback.diagonal_comp, P.cancel_left_of_respectsIso,
      P.cancel_left_of_respectsIso, ← P.cancel_right_of_respectsIso _
        (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)),
      ← pullback.condition, P.cancel_left_of_respectsIso]

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

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape J
⊢ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
by
  rwa [← isClosedUnderColimitsOfShape_iff_op]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' (λ_ X).hom

Tactic:
simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ (ConcreteCategory.hom (F.map (α.homEquiv'.symm 1 ▷ X).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (α.homEquiv'.symm 1 ▷ X).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' (λ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' (ρ_ X).hom

Tactic:
simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ (ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm 1).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm 1).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' (ρ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'
      (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫
        α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv'
      ((α_ X X X).hom ≫
        X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫
          α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)))

Tactic:
simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ (ConcreteCategory.hom (F.map (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X).op))
        (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X).op))
        (α.homEquiv' (snd X X)) =
    (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
        ((ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))).op))
          (α.homEquiv' (fst X X))) *
      (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
        ((ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))).op))
          (α.homEquiv' (snd X X)))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y✝ : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ α.homEquiv' (lift f₁ f₂ ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' f₁ * α.homEquiv' f₂

Tactic:
simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y✝ : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ (ConcreteCategory.hom (F.map (lift f₁ f₂).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (lift f₁ f₂).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' f₁ * α.homEquiv' f₂
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
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
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (Functor.empty C) F
⊢ IsIso (terminalComparison F)

Tactic:
by
  rw [← preservesTerminalIso_hom]
  infer_instance

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 A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (f ⊗ₘ g) ≫ prodComparison F A' B' = F.map f ⊗ₘ F.map g

Tactic:
IsIso.inv_comp_eq,

Goal state after:
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 A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ F.map (f ⊗ₘ g) ≫ prodComparison F A' B' = prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)
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 B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ inv (prodComparison F A B) ≫ F.map (A ◁ g) ≫ prodComparison F A B' = F.obj A ◁ F.map g

Tactic:
IsIso.inv_comp_eq,

Goal state after:
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 B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g
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 A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ inv (prodComparison F A B) ≫ F.map (f ▷ B) ≫ prodComparison F A' B = F.map f ▷ F.obj B

Tactic:
IsIso.inv_comp_eq,

Goal state after:
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 A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ ι = (β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ

Tactic:
apply lift_left_mul_ext μ
  nth_rw 2 [← Category.comp_id μ]
  rw [← comp_lift, Category.assoc, left_inv, ← Category.assoc (β_ A A).hom,
    ← lift_snd_fst, lift_map, lift_lift_assoc]
  nth_rw 2 [← Category.id_comp μ]
  rw [← lift_fst_snd, ← lift_lift_assoc (fst A A ≫ _), lift_comp_inv_left, lift_comp_one_left,
    lift_comp_inv_left, comp_toUnit_assoc]

Goal state after:
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType' β 0 → Empty :=
  fun x ↦
    match x with
    | ⟨val, h⟩ => ⋯.elim
⊢ Empty → WType' β 0

Tactic:
by
    intro x
    cases x

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)

Tactic:
· apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs
    rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
      ← image_comp, hsec', image_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Surjective ⇑L

Tactic:
· rw [← range_eq_top, eq_top_iff, LinearMap.range_codRestrict, ← map_le_iff_le_comap,
      Submodule.map_top, range_subtype]
    rintro ⟨d, e⟩
    have h := eq₂ d (-e)
    simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker,
      Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range,
      Function.prod_apply] at h ⊢
    grind

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

Goal state before:
pp: case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
ker_pow_eq_ker_pow_finrank_of_le h_cases

Goal state after:
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ finrank K V) ≤ LinearMap.ker (f ^ finrank K V)