-- Mathlib/CategoryTheory/Sites/Equivalence.lean
lemma W_inverseImage_whiskeringLeft :
    K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W

Proof state:
case h.mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f →
    LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)

Tactic:
rintro h _ ⟨R, rfl⟩

Result:
case h.mpr.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
h : LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f
R : Sheaf J A
⊢ Function.Bijective fun g => ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f ≫ g

Proof state:
case h.h.a.mp.intro.intro.intro.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P✝ Q : Cᵒᵖ ⥤ A
f : P✝ ⟶ Q
P : Dᵒᵖ ⥤ A
R : Sheaf K A
e : P ≅ (sheafToPresheaf K A).obj R
⊢ ObjectProperty.isoClosure (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj) P

Tactic:
exact ⟨_, ⟨_, rfl⟩, ⟨e.trans ((sheafToPresheaf _ _).mapIso
  ((G.sheafPushforwardContinuous A K J).objObjPreimageIso R).symm)⟩⟩

Result:
no goals

Proof state:
case h.mp.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
h :
  LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
    (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)
R : Sheaf J A
⊢ Function.Bijective fun g => f ≫ g

Tactic:
exact (h₂ R).1 (h _ ⟨R, rfl⟩)

Result:
no goals

Proof state:
case h.mpr.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
h : LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f
R : Sheaf J A
⊢ Function.Bijective fun g => ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f ≫ g

Tactic:
exact (h₂ R).2 (h _ ⟨R, rfl⟩)

Result:
no goals

Proof state:
case h.mp
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f) →
    LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f

Tactic:
rintro h _ ⟨R, rfl⟩

Result:
case h.mp.intro
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g
h :
  LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
    (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)
R : Sheaf J A
⊢ Function.Bijective fun g => f ≫ g

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ (Function.Bijective fun g => whiskerLeft G.op f ≫ g) ↔ Function.Bijective fun g => f ≫ g

Tactic:
rw [← Function.Bijective.of_comp_iff _
  (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.val R.cond)]

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ Function.Bijective ((fun g => whiskerLeft G.op f ≫ g) ∘ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map) ↔
    Function.Bijective fun g => f ≫ g

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = LeftBousfield.W fun x => x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ Function.Bijective ((fun g => whiskerLeft G.op f ≫ g) ∘ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map) ↔
    Function.Bijective fun g => f ≫ g

Tactic:
exact Function.Bijective.of_comp_iff'
  (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.val R.cond)
    (fun g ↦ f ≫ g)

Result:
no goals