mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
        { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
        let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
        { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
          h₁ := fun {i j} k ↦
            (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
          w₁₁ := ⋯, w₁₂ := ⋯ }).s₀ =
    (𝟙 E).s₀

Tactic:
ext; simp

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 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
⊢ ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
        { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
          h₁ := fun {i j} k ↦
            (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
          w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
        let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
        { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).s₀ =
    (𝟙 F).s₀

Tactic:
ext; simp

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimitCone F).hom

Tactic:
suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫ lim.map (whiskerRight (currying.unitIso.app F).inv colim))
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
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (E.inter F.toPreOneHypercover).sieve₁ p₁ p₂ ∈ J W

Tactic:
PreOneHypercover.sieve₁_inter h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.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 i₂.1) (F.f i₂.2)))) ∈
    J W
Module: Mathlib.CategoryTheory.Sites.Over

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

Tactic:
by
    let W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
    let g₁' : W' ⟶ Y₁ := Over.homMk f₁
    let g₂' : W' ⟶ Y₂ := Over.homMk f₂ (by simpa using! h.symm =≫ Z.hom)
    exact hx g₁' g₂' hg₁ hg₂ (by ext; exact h)

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

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
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map (f✝.val ≫ g✝.val)) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
            ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
        ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv ((PresheafOfModules.pullback φ.hom).obj X✝.val)
            Y✝).symm
        (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X✝.val Y✝.val).symm g✝.val)

Tactic:
Adjunction.homEquiv_naturality_left_symm

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
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map (f✝.val ≫ g✝.val)) ≫
      ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
            ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
        ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val) =
    (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map f✝.val) ≫
      (PresheafOfModules.sheafification (𝟙 R.obj)).map ((PresheafOfModules.pullback φ.hom).map g✝.val) ≫
        ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((PresheafOfModules.pushforward φ.hom).obj Y✝.val)) Y✝).symm
          ((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).counit.app Y✝.val)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝ : Set (Opens ↑Y)
⊢ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝), is_open' := ⋯ } =
    sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝)

Tactic:
ext; simp

Goal state after:
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
⊢ PreservesLimit (Discrete.functor g) hf.functor

Tactic:
refine preservesLimit_of_preserves_limit_cone (Preorder.isLimitIInf g) ?_

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
g : ι → Opens ↑X
⊢ IsLimit (hf.functor.mapCone (Fan.mk (⨅ i, g i) fun i ↦ homOfLE ⋯))
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ id = (fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)

Tactic:
ext; simp

Goal state after:
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
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵
module : moduleTopology R (A ⧸ S) = TopologicalSpace.coinduced (⇑S.mkQ) inferInstance
⊢ TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵ = moduleTopology R (A ⧸ S)

Tactic:
module

Goal state after:
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
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵
module : moduleTopology R (A ⧸ S) = TopologicalSpace.coinduced (⇑S.mkQ) inferInstance
⊢ TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵ = TopologicalSpace.coinduced (⇑S.mkQ) inferInstance
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ (fun ab ↦ (bil ab.1) ab.2) = (fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap

Tactic:
ext; simp

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

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
f : M₁ →L[R] S
⊢ f.smulRight 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
x : M₂
⊢ smulRight 0 x = 0

Tactic:
ext; simp

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₁ : Type u_4
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₁
⊢ toSpanSingleton R₁ 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ toSpanSingleton R c ^ 0 = toSpanSingleton R (c ^ 0)

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ x✝ : U →L[R] V
⊢ lcomp W (x✝¹ + x✝) = lcomp W x✝¹ + lcomp W x✝

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ : R
x✝ : U →L[R] V
⊢ lcomp W (x✝¹ • x✝) = (RingHom.id R) x✝¹ • lcomp W x✝

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousAdd M
inst✝² : ContinuousConstSMul S M
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M
f : R →L[R] M
⊢ toSpanSingleton R ((fun f ↦ f 1) f) = f

Tactic:
ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) = MulHom.id ↑X

Tactic:
ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) = MulHom.id ↑X

Tactic:
ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.one
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ (Hom.hom m) 1 = (Hom.hom (descMorphism F s)) 1

Tactic:
map_one

Goal state after:
case h.one
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ 1 = (Hom.hom (descMorphism F s)) 1
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case refine_2
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S))).comp (AddMonoidHom.id (T ⊗[R] S)) =
    (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)).toAddMonoidHom.comp
      ↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S))

Tactic:
· ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (Over.forget X)

Tactic:
by
  refine ⟨fun J hJ hJ' ↦ ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨.ofExistsUnique fun s ↦ ?_⟩⟩⟩⟩
  obtain i := Nonempty.some ((inferInstance : Nonempty J))
  let s' : Cone F := ⟨Over.mk (s.π.app i ≫ (F.obj i).hom), fun j ↦ Over.homMk (s.π.app j) (by
    obtain ⟨k, hik, hjk, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    simp only [Functor.const_obj_obj, Over.mk_left, Over.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp), fun j k e ↦ by ext; simpa using (s.w e).symm⟩
  refine ⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩
  dsimp at hf
  exact congr($(hc.uniq s' (Over.homMk f (by simp [s', ← hf]))
    fun j ↦ Over.OverMorphism.ext (hf j)).left)

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

Goal state before:
pp: case neg
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
h₁ : IsUnit (↑e.symm ∘SL f)
⊢ f.IsInvertible

Tactic:
rcases h₁ with ⟨F, hF⟩

Goal state after:
case neg
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
⊢ f.IsInvertible
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + {Hom.snd a ≫ eqToHom ⋯}).Nodup

pp: case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : ¬J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + 0).Nodup

pp: case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : J.snd a = b
⊢ (0 + {Hom.snd a ≫ eqToHom ⋯}).Nodup

pp: case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : ¬J.snd a = b
⊢ (0 + 0).Nodup

Tactic:
· simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMultispan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]
          simp

Goal state after:
case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : ¬J.snd a = b
⊢ ({Hom.fst a ≫ eqToHom ⋯} + 0).Nodup

case pos
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : J.snd a = b
⊢ (0 + {Hom.snd a ≫ eqToHom ⋯}).Nodup

case neg
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst a = b
h✝ : ¬J.snd a = b
⊢ (0 + 0).Nodup
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ e.trans (α • f) = α • e.trans f

Tactic:
ext; simp

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) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
⊢ m =
    ofHom
      { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)), cont := ⋯ }

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

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

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
hn : ∃ f_1, Function.Surjective ⇑f_1 ∧ (ker f_1.toRingHom).FG
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
⊢ ∃ i g', f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i

Tactic:
let iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
hn : ∃ f_1, Function.Surjective ⇑f_1 ∧ (ker f_1.toRingHom).FG
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
⊢ ∃ i g', f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i