mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
this :
  p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    p ≫
      pullback.snd ((E.inter F).f i) ((E.inter F).f j) ≫
        pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
          (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd)
⊢ pullback.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1

Tactic:
simp [this, pullback.condition_assoc, toPullback]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this) =
    (ConcreteCategory.hom (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app U)) x✝

Tactic:
apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)

Goal state after:
case hx
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝).Compatible

case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝).IsAmalgamation
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2

Tactic:
simp only [Category.assoc] at u₁
      simp [← reassoc_of% h₁, w, ← reassoc_of% u₁, ← pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
i j : E.I₀
k : E.I₁ i j
⊢ v₀ i = u₀ i

Tactic:
by simp [h₀]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
i j : E.I₀
k : E.I₁ i j
⊢ v₀ j = u₀ j

Tactic:
by simp [h₀]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
rw [Sieve.pullback_top]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P ⊤.arrows
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → Sieve.functorPushforward G S ∈ K (G.obj X)

Tactic:
rintro ⟨T, rfl⟩

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
T : ↑(K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₂ ((congrIndexOneOfEq ⋯ ⋯) k) = E.p₂ k ≫ eqToHom ⋯

pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
congrIndexOneOfEqIso_inv_p₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ E.p₂ k ≫ eqToHom ⋯ = E.p₂ k ≫ eqToHom ⋯

case w
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
⊢ E.toPreOneHypercover.HasPullbacks

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁶ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝³ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
⊢ Epi ((F.obj M).freeHomEquiv.symm ((F.obj M).freeHomEquiv (G.mapFreeHom F η)))

Tactic:
by
    simp only [mapFreeHom, Equiv.symm_apply_apply, epi_comp_iff_of_epi]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
⊢ HasColimit F

Tactic:
by
    have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
    apply hasColimit_of_iso (diagramIsoPair F)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ ↑((map U.inclusion').obj U) = ↑⊤

Tactic:
exact Subtype.coe_preimage_self _

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
⊢ ⋯.functor = map (inclusionTopIso X).inv

Tactic:
by
  refine CategoryTheory.Functor.ext ?_ ?_
  · intro U
    ext x
    exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
  · subsingleton

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
rintro ⟨⟨x, -, rfl⟩, hx⟩

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ ↑U
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ((map f).obj U))
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
g : ι → Opens ↑X
⊢ IsGLB (Set.range fun i ↦ hf.functor.obj (g i)) (⨅ i, hf.functor.obj (g i))

Tactic:
apply isGLB_iInf

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        ((((pushforwardId R).inv ≫
                      pushforwardNatTrans (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R)) adj.counit ≫
                        (pushforwardCongr ⋯).hom ≫ (pushforwardComp ψ φ).inv).app
                  ((pushforward ψ).obj X) ≫
                (pushforward ψ).map
                  (((pushforwardComp φ ψ).hom ≫
                        pushforwardNatTrans (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) adj.unit ≫
                          (pushforwardCongr ⋯).hom ≫ (pushforwardId S).hom).app
                    X)).val.app
          U))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x

Tactic:
change (X.val.presheaf.map (G.map (adj.counit.app U.unop)).op ≫
      X.val.presheaf.map (adj.unit.app (G.obj U.unop)).op) _ = _

Goal state after:
C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (G.map (adj.counit.app (Opposite.unop U))).op ≫
          X.val.presheaf.map (adj.unit.app (G.obj (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: case g
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ s.pt.left ⟶ (asEmptyCone x).pt.left

pp: case w
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map ?g ≫ (asEmptyCone x).pt.hom = s.pt.hom) CostructuredArrow.homMk._auto_1

Tactic:
· change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_mono s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)

Goal state after:
case w
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map (id (homOfLE ⋯).op) ≫ (asEmptyCone x).pt.hom = s.pt.hom)
    CostructuredArrow.homMk._auto_1
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_2.pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Tactic:
exact (hs <| op <| Pairwise.Hom.left i j).symm

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
· rintro ⟨h1, h2⟩
      use τ.induced e
      rw [induced_compose]
      refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩
      nth_rw 2 [← induced_id (t := τ)]
      simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
⊢ inverse 0 = 0

Tactic:
rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩
    ext x
    exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
⊢ m =
    ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ }

Tactic:
ext x
    refine congr($(hc.uniq ((forget₂ _ _).mapCone s) ((forget₂ _ _).map m) fun j ↦ ?_).hom x)
    ext y
    exact congr($(H j).hom y)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩ <;>
    simp only [isCardinalFiltered_aleph0_iff] at *

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ HasCardinalFilteredColimits C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩ <;>
    simp only [isCardinalFiltered_aleph0_iff] at *

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasCardinalFilteredColimits C ℵ₀
H : ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], HasColimitsOfShape J C
⊢ ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C

case refine_2
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], HasColimitsOfShape J C
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X✝ Y : C
e : X✝ ≅ Y
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
X : (isCardinalPresentable C κ).FullSubcategory
⊢ IsCardinalPresentable ((isCardinalPresentable C κ).ι.obj X) κ

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
φ : ι → (j ⟶ max k hι) := fun i ↦ f i ≫ toMax k hι i
⊢ ∀ (i : ι), f i ≫ (fun i ↦ toMax k hι i ≫ coeqHom φ hι) i = toCoeq φ hι

Tactic:
by simpa [φ] using coeq_condition φ hι

Goal state after: