-- Mathlib/CategoryTheory/Sites/Monoidal.lean
lemma whiskerLeft {G₁ G₂ : Cᵒᵖ ⥤ A} {g : G₁ ⟶ G₂} (hg : J.W g) (F : Cᵒᵖ ⥤ A) :
    J.W (F ◁ g) := fun H h ↦ by
  have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)
  rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
    ((ihom.adjunction _).homEquiv _ _).bijective]
  rw [← Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _
    ((ihom.adjunction _).homEquiv _ _).bijective] at this
  convert this using 1
  ext α : 1
  dsimp
  rw [curry_natural_left]

Proof state:
case h.e'_3.h.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1) α = ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry) α

Tactic:
dsimp

Result:
case h.e'_3.h.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ MonoidalClosed.curry (F ◁ g ≫ α) = g ≫ MonoidalClosed.curry α

Proof state:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
⊢ Function.Bijective fun g_1 => F ◁ g ≫ g_1

Tactic:
have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)

Result:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 => g ≫ g_1
⊢ Function.Bijective fun g_1 => F ◁ g ≫ g_1

Proof state:
case h.e'_3.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
⊢ (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1) = (fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry

Tactic:
ext α : 1

Result:
case h.e'_3.h.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1) α = ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry) α

Proof state:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 => g ≫ g_1
⊢ Function.Bijective fun g_1 => F ◁ g ≫ g_1

Tactic:
rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
  ((ihom.adjunction _).homEquiv _ _).bijective]

Result:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 => g ≫ g_1
⊢ Function.Bijective (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1)

Proof state:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
⊢ Function.Bijective (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1)

Tactic:
convert this using 1

Result:
case h.e'_3.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
⊢ (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1) = (fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry

Proof state:
case h.e'_3.h.h
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
e_2✝ : (G₁ ⟶ (ihom F).obj H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ MonoidalClosed.curry (F ◁ g ≫ α) = g ≫ MonoidalClosed.curry α

Tactic:
rw [curry_natural_left]

Result:
no goals

Proof state:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 => g ≫ g_1
⊢ Function.Bijective (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1)

Tactic:
rw [← Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _
  ((ihom.adjunction _).homEquiv _ _).bijective] at this

Result:
C : Type u'
inst✝⁵ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝⁴ : Category.{v, u} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 => g ≫ g_1) ∘ MonoidalClosed.curry)
⊢ Function.Bijective (MonoidalClosed.curry ∘ fun g_1 => F ◁ g ≫ g_1)