mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g₁ g₂ : StructuredArrow (op (G.obj U)) G.op
i : g₁ ⟶ g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map i ≫
      ⋯.amalgamate ⟨G.imageSieve g₂.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₂.2) U I.f g₂.hom.unop ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₁.2) U I.f g₁.hom.unop ⋯).op) ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i

Tactic:
obtain ⟨⟨W₁⟩, ⟨g₁⟩, rfl⟩ := g₁.mk_surjective

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g₂ : StructuredArrow (op (G.obj U)) G.op
W₁ : C
g₁ : unop (G.op.obj (op W₁)) ⟶ unop (op (G.obj U))
i : StructuredArrow.mk (op g₁) ⟶ g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map i ≫
      ⋯.amalgamate ⟨G.imageSieve g₂.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₂.2) U I.f g₂.hom.unop ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₁)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₁)).2) U I.f (StructuredArrow.mk (op g₁)).hom.unop ⋯).op)
        ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
rw [PreOneHypercover.congrIndexOneOfEq_congrFun hs₀ hs₁]

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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
rw [PreOneHypercover.congrIndexOneOfEq_congrFun hs₀ hs₁]

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

Goal state before:
pp: 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 = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ (Function.Bijective fun g ↦ G.op.whiskerLeft 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.obj R.property)]
    exact Function.Bijective.of_comp_iff'
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G P R.obj R.property)
        (fun g ↦ f ≫ g)

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

Goal state before:
pp: case refine_1.refine_2
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (i : E.multicospanShape.R) →
    (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.right i) ≅
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right i)

pp: case refine_1.refine_3
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.fst i) ≫ Iso.hom (?refine_1.refine_2 i) =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.fst i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst i)

pp: case refine_1.refine_4
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫ Iso.hom (?refine_1.refine_2 i) =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.snd i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)

Tactic:
· intro i
      exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op

Goal state after:
case refine_1.refine_3
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.fst i) ≫
        (G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op).hom =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.fst i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst i)

case refine_1.refine_4
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
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫
        (G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op).hom =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.snd i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)
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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
⊢ ∀ (E_1 : Multifork (E.multicospanIndex F.obj)) (m : E_1.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = E_1.ι i) → m = multiforkLift E_1

Tactic:
intro c m hm
    apply F.property.hom_ext_ofArrows _ E.mem₀
    intro i₀
    rw [multiforkLift_map]
    exact hm i₀

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ (overEquiv Y) (generate R) = generate (Presieve.functorPushforward (Over.forget X) R)

Tactic:
by
  refine le_antisymm (fun Z g hg ↦ ?_) ?_
  · rw [overEquiv_iff] at hg
    obtain ⟨W, u, v, hv, huv⟩ := hg
    exact ⟨W.left, u.left, v.left, ⟨W, v, 𝟙 _, hv, by simp⟩, congr($(huv).left)⟩
  · rw [generate_le_iff]
    rintro Z g ⟨W, u, v, hu, rfl⟩
    exact (overEquiv_iff _ _).mpr ⟨W, Over.homMk v, u, hu, rfl⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y

Tactic:
rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff,
      Sieve.overEquiv, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
      ← Sieve.generate_map_eq_functorPushforward]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ Sieve.generate (Presieve.map (Over.forget X) R) ∈ K.toGrothendieck Y.left
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: 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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ ((pushforward φ).obj M).unitHomEquiv
      (((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) (pullbackObjUnitToUnit φ ≫ f)) =
    pushforwardSections φ (M.unitHomEquiv f)

Tactic:
pushforwardSections_unitHomEquiv,

Goal state after:
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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ ((pushforward φ).obj M).unitHomEquiv
      (((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) (pullbackObjUnitToUnit φ ≫ f)) =
    ((pushforward φ).obj M).unitHomEquiv (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f)
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → ToType (F.obj (op (U i)))),
      F.IsCompatible U sf →
        ∃! s,
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

Tactic:
refine forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩

Goal state after:
case refine_1
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
    ∃! x,
      ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j
sf : (i : ι) → ToType (F.obj (op (U i)))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case refine_2.convert_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.obj.obj (op (iSup U)))
gl_spec : IsGluing F.obj U sf gl
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
gl' : ToType (F.obj.obj (op V))
gl'_spec : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) gl' = sf i
i : ι
⊢ (ConcreteCategory.hom (F.obj.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) gl' = sf i

Tactic:
· exact gl'_spec i

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom ((stalkFunctor C x).map f.hom)) ((ConcreteCategory.hom (F.presheaf.germ V₁ x hxV₁)) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
rw [stalkFunctor_map_germ_apply V₁ x hxV₁ f.1 s₁] at hs₁

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
t : CC (G.obj.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.obj V₁ x hxV₁)) ((ConcreteCategory.hom (f.hom.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S✝
inst✝⁹ : Ring R
inst✝⁸ : Ring S✝
A : Type u_3
inst✝⁷ : AddCommGroup A
inst✝⁶ : Module R A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
⊢ IsModuleTopology R (A ⧸ S)

Tactic:
constructor
  have := toContinuousAdd R A
  have quot := (Submodule.isOpenQuotientMap_mkQ S).isQuotientMap.eq_coinduced
  have module := ModuleTopology.eq_coinduced_of_surjective <| Submodule.mkQ_surjective S
  rw [quot, module]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : s.topologicalClosure = ⊤
⊢ (Submodule.map (↑f) s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ (hₗ ∘SL (c • fₗ)) x = (c • hₗ ∘SL fₗ) x

Tactic:
exact hₗ.map_smul_of_tower c (fₗ x)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
⊢ hₗ ∘SL (c • fₗ) = c • hₗ ∘SL fₗ

Tactic:
ext x
  exact hₗ.map_smul_of_tower c (fₗ x)

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
f : X ⟶ Y
x✝ : IsIso ((forget Semigrp).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget Semigrp).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toSemigrpIso.isIso_hom

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

Goal state before:
pp: 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₂
⊢ inverse 0 = 0

Tactic:
by
  by_cases h : IsInvertible (0 : M →L[R] M₂)
  · rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩
    ext x
    exact Subsingleton.elim _ _
  · exact inverse_of_not_isInvertible h

Goal state after:
Module: Mathlib.Algebra.Category.Ring.EqualizerPushout

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
isLimit : IsLimit fork :=
  (fork.isLimitEquivOfIsos (equalizerFork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr) (Iso.refl (of ↑S))
        (Iso.refl (pushoutCocone ↑R ↑S ↑S).pt)
        (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone ↑R ↑S) ⋯).toCommRingCatIso ⋯ ⋯ ⋯).symm
    (equalizerForkIsLimit (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr)
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
exact Fork.isLimitEquivOfIsos fork (Fork.ofι f pushout.condition) (Iso.refl _)
    (IsPushout.isoPushout isPushout) (Iso.refl _) (IsPushout.inl_isoPushout_hom isPushout).symm
    (IsPushout.inr_isoPushout_hom isPushout).symm rfl isLimit

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map γ ≫ F.map (minToLeft i₀ j) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    F.map γ ≫ F.map (minToRight i₀ j)

Tactic:
isoMap_hom_inv_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map γ ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app (IsCofiltered.min i₀ j) ≫
      F.map (minToLeft i₀ j) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j)

Tactic:
isoMap_hom_inv_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j) = s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ c.π.app i ≫ F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β

Tactic:
isoMap_hom_inv_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ c.π.app i ≫ F.map β = c.π.app i ≫ F.map β