mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (P Q R : Action V G) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
intros

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (P Q R : Action V G) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
intros

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x y : R) (b : X ⟶ Y), (x * y) • b = x • y • b

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (b : X ⟶ Y), 1 • b = b

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ 1 • b✝ = b✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R), a • 0 = 0

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ a✝ • 0 = 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (a : R) (x y : X ⟶ Y), a • (x + y) = a • x + a • y

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (r s : R) (x : X ⟶ Y), (r + s) • x = r • x + s • x

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x : X ⟶ Y), 0 • x = 0

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ 0 • x✝ = 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
⊢ ∀ (X Y Z : Action V G) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g

Tactic:
intros

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inl

Tactic:
intros

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inl
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inr

Tactic:
intros

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inr
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b) (m : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s.pt),
    ⋯.hom ≫ m = s.inl → ⋯.hom ≫ m = s.inr → m = ⋯.hom

Tactic:
intros

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
m✝ : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s✝.pt
x✝¹ : ⋯.hom ≫ m✝ = s✝.inl
x✝ : ⋯.hom ≫ m✝ = s✝.inr
⊢ m✝ = ⋯.hom
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ({ obj := fun t ↦ ∐ fun x ↦ x✝, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f), map_id := ⋯,
              map_comp := ⋯ }.map
          f_1 ≫
        Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
      (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫
        { obj := fun t ↦ ∐ fun x ↦ d₂, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f),
              map_id := ⋯, map_comp := ⋯ }.map
          f_1

Tactic:
intros

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ({ obj := fun t ↦ ∐ fun x ↦ x✝, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f), map_id := ⋯,
            map_comp := ⋯ }.map
        f✝ ≫
      Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
    (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫
      { obj := fun t ↦ ∐ fun x ↦ d₂, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f), map_id := ⋯,
            map_comp := ⋯ }.map
        f✝
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ (∀ (c : C), Epi (η.app c)) → Epi η

Tactic:
intros

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
a✝ : ∀ (c : C), Epi (η.app c)
⊢ Epi η
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : X ⟶ X} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    ((fun {x x_1} η h ↦ η ▷ h) f₁ X₂ ≫ (fun {f x x_1} η ↦ f ◁ η) f₂) ≫
        (fun {x x_1} η h ↦ η ▷ h) g₁ Y₂ ≫ (fun {f x x_1} η ↦ f ◁ η) g₂ =
      (fun {x x_1} η h ↦ η ▷ h) (f₁ ≫ g₁) X₂ ≫ (fun {f x x_1} η ↦ f ◁ η) (f₂ ≫ g₂)

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ ((fun {x x_1} η h ↦ η ▷ h) f₁✝ X₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) f₂✝) ≫
      (fun {x x_1} η h ↦ η ▷ h) g₁✝ Y₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) g₂✝ =
    (fun {x x_1} η h ↦ η ▷ h) (f₁✝ ≫ g₁✝) X₂✝ ≫ (fun {f x x_1} η ↦ f ◁ η) (f₂✝ ≫ g₂✝)
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).inv ≫ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
      (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
    F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]
  simp

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk ((F ⟨i, X⟩.fst).map f ≫ (α ⟨i, Y✝⟩.fst).app ⟨i, Y✝⟩.snd) =
    SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd ≫ (G ⟨i, X⟩.fst).map f)

Tactic:
rw [(α i).naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f

Tactic:
intros

Goal state after:
case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f

Tactic:
intros

Goal state after:
case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝
Module: Mathlib.CategoryTheory.Category.KleisliCat

Goal state before:
pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
intros

Goal state after:
case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type u_7
f : α →. α✝
⊢ id <$> f = f

Tactic:
funext a

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
α✝ : Type u_7
f : α →. α✝
a : α
⊢ (id <$> f) a = f a
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ (res f s).core t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
mem_core_res

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ (f.comp g).comp h x✝¹ ↔ x✝ ∈ f.comp (g.comp h) x✝¹

Tactic:
simp only [comp_apply, Part.bind_comp]

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

Goal state before:
pp: case e_g.e_a.e_f
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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ ε.hom = (ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))

Tactic:
exact (comp_id _).symm

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

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ X₂ Y₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁✝ Y₁✝ X₂✝ Y₂✝ : LocalizedMonoidal L W ε
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X₁ X₂ : LocalizedMonoidal L W ε), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁✝ X₂✝ : LocalizedMonoidal L W ε
⊢ 𝟙 X₁✝ ⊗ₘ 𝟙 X₂✝ = 𝟙 (X₁✝ ⊗ X₂✝)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : LocalizedMonoidal L W ε
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ⊗ₘ f₂✝) ≫ (g₁✝ ⊗ₘ g₂✝) = f₁✝ ≫ g₁✝ ⊗ₘ f₂✝ ≫ g₂✝
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X Y : LocalizedMonoidal L W ε), X ◁ 𝟙 Y = 𝟙 (X ⊗ Y)

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X✝ Y✝ : LocalizedMonoidal L W ε
⊢ X✝ ◁ 𝟙 Y✝ = 𝟙 (X✝ ⊗ Y✝)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ (X Y : LocalizedMonoidal L W ε), 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X✝ Y✝ : LocalizedMonoidal L W ε
⊢ 𝟙 X✝ ▷ Y✝ = 𝟙 (X✝ ⊗ Y✝)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
⊢ ∀ {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y), 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
intros

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X✝ Y✝ : LocalizedMonoidal L W ε
f✝ : X✝ ⟶ Y✝
⊢ 𝟙_ (LocalizedMonoidal L W ε) ◁ f✝ ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ f✝
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
inst✝³ : BraidedCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u
inst✝¹ : Category.{v, u} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Quiver.Hom.opEquiv.symm.trans homEquiv) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((Quiver.Hom.opEquiv.symm.trans homEquiv) g ⊗ₘ (Quiver.Hom.opEquiv.symm.trans homEquiv) f) ≫
        eComp V (Opposite.unop Z✝) (Opposite.unop Y✝) (Opposite.unop X✝)

Tactic:
exact homEquiv_comp g.unop f.unop

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ map p g ψ ⋯ τ ≫ ψ = τ

Tactic:
fac

Goal state after:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ τ = τ
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_2} D
inst✝² : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
⊢ F.HasLeftDerivedFunctor W

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  simpa only [hasLeftDerivedFunctor_iff F L W] using HasRightKanExtension.mk LF α

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
⊢ ∀ {X Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f

Tactic:
intro X Y f _

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : X ⟶ Y
a✝ : Mono (F.map f)
⊢ Mono f
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝¹ x✝ : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
Z : C
f : Z ⟶ A ⨯ B
z : (F.obj Z).obj
hgal : IsGalois Z
hfz : (ConcreteCategory.hom (F.map f)) z = (fiberBinaryProductEquiv F A B).symm (a, b)
⊢ (ConcreteCategory.hom (F.map (f ≫ prod.snd))) { obj := Z, pt := z, isGalois := hgal }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt

Tactic:
· simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_snd_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
⊢ (endEquivAutGalois F) (g ≫ f) = (endEquivAutGalois F) g * (endEquivAutGalois F) f

Tactic:
refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)
  simp only [map_mul, endEquivAutGalois_π, Aut.Aut_mul_def, NatTrans.comp_app, Iso.trans_hom]
  simp only [map_comp, FintypeCat.comp_apply, endEquivAutGalois_π]
  change f.app A (g.app A A.pt) =
    (f.app A ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt
  rw [← f.naturality, FintypeCat.comp_apply, endEquivAutGalois_π]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ μ * ↑σ⁻¹ ≈ μ

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ (μ * ↑σ⁻¹)⁻¹ * μ ∈ ↑V
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := ⋯
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) := ⋯
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ σ * τ ≈ τ

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Goal state after:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := ⋯
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) := ⋯
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (σ * τ)⁻¹ * τ ∈ MulAction.stabilizer (Aut F) a
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ univ → Groupoid.inv p ∈ univ

Tactic:
intros

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
a✝ : p✝ ∈ univ
⊢ Groupoid.inv p✝ ∈ univ