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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
by
    let W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
    let g₁' : W' ⟶ Y₁ := Over.homMk f₁.left
    let g₂' : W' ⟶ Y₂ := Over.homMk f₂.left
      (by simpa using! (Over.forget _).congr_map h.symm =≫ Z.hom)
    let e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl _)
      (by simpa [W'] using! (Over.w f₁).symm)
    convert congr_arg (F.obj.map e.inv.op)
      (hx g₁' g₂' hg₁ hg₂ (by ext; exact (Over.forget _).congr_map h)) using 1
    all_goals
      dsimp [e, W', g₁', g₂']
      rw [← Functor.map_comp_apply]
      apply ConcreteCategory.congr_hom
      congr 1
      rw [← op_comp]
      congr 1
      ext
      simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ Sieve.functorPullback F ((Sieve.overEquiv ((Over.post F).obj U)) S) ∈ J U.left

Tactic:
exact F.cover_lift J K hS

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ ((E.map (Over.post F)).map (Over.forget (F.obj X))).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left

Tactic:
← PreOneHypercover.map_comp,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (E.map (Over.post F ⋙ Over.forget (F.obj X))).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
· exact Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero i).mpr h))

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

Goal state before:
pp: X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
⊢ s = t

Tactic:
have := (isSheaf_iff_isSheaf_of_type _ _).mp
    ((Presheaf.isSheaf_iff_isSheaf_forget (C := Opens X) (A' := A) _ F (forget _)).mp hF)
  choose V hV hxV H using fun x : U.unop ↦ hst x.1 x.2
  refine (this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_
  · exact fun x hx ↦ ⟨V ⟨x, hx⟩, homOfLE (hV _), Sieve.ofArrows_mk _ _ _, hxV _⟩
  · rintro _ _ ⟨x⟩; exact H x

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

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ ∀ (x : single i ⟶ single j), x ∈ if h : i = j then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id_single
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ id_single i ∈ if h : i = i then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k : ι
⊢ ∀ (x : single i ⟶ pair j k), x ∈ ∅

Tactic:
rintro ⟨⟩

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

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k : ι
⊢ ∀ (x : pair i j ⟶ single k),
    x ∈ (if h : i = k then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = k then {right i j ≫ eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case left
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ left i j ∈ (if h : i = i then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = i then {right i j ≫ eqToHom ⋯} else ∅

case right
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ right i j ∈ (if h : i = j then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = j then {right i j ≫ eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j k l : ι
⊢ ∀ (x : pair i j ⟶ pair k l), x ∈ if h : i = k ∧ j = l then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id_pair
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ id_pair i j ∈ if h : i = i ∧ j = j then {eqToHom ⋯} else ∅
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X : TopCat
Y : Opens ↑X
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Tactic:
funext Z

Goal state after:
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux (coveringOfPresieve Y R) Y)).arrows.cocone.op)

Tactic:
covering_presieve_eq_self R

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
R : Presieve Y
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) Y
⊢ IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op) =
    IsLimit (Functor.mapCone F (Sieve.generate R).arrows.cocone.op)
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)
F : Presheaf C X
x : ↑X
V : Opens ↑X
hV : x ∈ V
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
⊢ x ∈ U ⊓ V

Tactic:
by simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
by
    rw [← nhds_prod_eq] at hmul
    refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;>
      simpa [ContinuousAt]

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

Goal state before:
pp: case h
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 : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.obj.map (i₁ x).op)) s = (ConcreteCategory.hom (F.obj.map (i₁ x).op)) t

Tactic:
heq,

Goal state after:
case h
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 : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t = (ConcreteCategory.hom (F.obj.map (i₁ x).op)) t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ Dense ↑s ↔ s.topologicalClosure = ⊤

Tactic:
by
  rw [← SetLike.coe_set_eq, dense_iff_closure_eq]
  simp

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
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
z : ↑X
hz : z ∈ V x ⊓ V y
⊢ (ConcreteCategory.hom (germ G.obj (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (G.obj.map ((V x).infLELeft (V y)).op))
        ((ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x))) =
    (ConcreteCategory.hom (germ G.obj (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (G.obj.map ((V x).infLERight (V y)).op))
        ((ConcreteCategory.hom (f.hom.app (op (V y)))) (sf y)))

Tactic:
heq,

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
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
z : ↑X
hz : z ∈ V x ⊓ V y
⊢ (ConcreteCategory.hom (germ G.obj (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (G.obj.map ((V x).infLELeft (V y)).op))
        ((ConcreteCategory.hom (G.obj.map (iVU x).op)) t)) =
    (ConcreteCategory.hom (germ G.obj (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (G.obj.map ((V x).infLERight (V y)).op)) ((ConcreteCategory.hom (G.obj.map (iVU y).op)) t))
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))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))

Tactic:
refine app_surjective_of_injective_of_locally_surjective f U (And.left <| h · ·) fun t x hx => ?_

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, ∃ (_ : 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
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
X Y : Type u_2
e : X ≃ Y
a✝ :
  ∀ {A : X → Type u_3} [inst : (i : X) → AddCommMonoid (A i)] [inst_1 : (i : X) → Module R (A i)]
    [inst_2 : (i : X) → TopologicalSpace (A i)] [∀ (i : X), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : X) → A i)
A : Y → Type u_3
inst✝³ : (i : Y) → AddCommMonoid (A i)
inst✝² : (i : Y) → Module R (A i)
inst✝¹ : (i : Y) → TopologicalSpace (A i)
inst✝ : ∀ (i : Y), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Y) → A i)

Tactic:
case =>

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option ι) → A i)

Tactic:
case =>

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T⁻¹ (↑T x) = x

Tactic:
← mul_apply_eq_comp,

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ (↑T⁻¹ * ↑T) x = x
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T (↑T⁻¹ x) = x

Tactic:
← mul_apply_eq_comp,

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ (↑T * ↑T⁻¹) x = x
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a b : J.L
⊢ ∀ (x : left a ⟶ left b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.id (left a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ∀ (x : left a ⟶ right b),
    x ∈
      {
        val :=
          (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
            if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0,
        nodup := ⋯ }

Tactic:
rintro ⟨⟩

Goal state after:
case fst
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
⊢ Hom.fst b ∈
    {
      val :=
        (if e : J.fst b = J.fst b then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
          if e : J.snd b = J.fst b then {eqToHom ⋯ ≫ Hom.snd b} else 0,
      nodup := ⋯ }

case snd
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
⊢ Hom.snd b ∈
    {
      val :=
        (if e : J.fst b = J.snd b then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
          if e : J.snd b = J.snd b then {eqToHom ⋯ ≫ Hom.snd b} else 0,
      nodup := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
b : J.L
⊢ ∀ (x : right a ⟶ left b), x ∈ ∅

Tactic:
rintro ⟨⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a b : J.R
⊢ ∀ (x : right a ⟶ right b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a b : J.L
⊢ ∀ (x : left a ⟶ left b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.id (left a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ∀ (x : left a ⟶ right b),
    x ∈
      {
        val :=
          (if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0) +
            if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0,
        nodup := ⋯ }

Tactic:
rintro ⟨⟩

Goal state after:
case fst
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.fst a ∈
    {
      val :=
        (if e : J.fst a = J.fst a then {Hom.fst a ≫ eqToHom ⋯} else 0) +
          if e : J.snd a = J.fst a then {Hom.snd a ≫ eqToHom ⋯} else 0,
      nodup := ⋯ }

case snd
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.snd a ∈
    {
      val :=
        (if e : J.fst a = J.snd a then {Hom.fst a ≫ eqToHom ⋯} else 0) +
          if e : J.snd a = J.snd a then {Hom.snd a ≫ eqToHom ⋯} else 0,
      nodup := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
b : J.L
⊢ ∀ (x : right a ⟶ left b), x ∈ ∅

Tactic:
rintro ⟨⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a b : J.R
⊢ ∀ (x : right a ⟶ right b), x ∈ if e : a = b then {eqToHom ⋯} else ∅

Tactic:
rintro ⟨⟩

Goal state after:
case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅