mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case fst
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).1 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).1

pp: case snd
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).2 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).2

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).1 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).1

case snd
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := ⋯
τP : TopologicalSpace P := ⋯
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := ⋯
i₁ : M →ₗ[R] P := ⋯
i₂ : N →ₗ[R] P := ⋯
a : M
b : N
⊢ (i (a, b)).2 = (((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2)) (a, b)).2
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_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((∑ i ∈ s, g i) ∘SL f) x✝ = (∑ i ∈ s, g i ∘SL f) x✝

Tactic:
simp only [comp_apply, sum_apply]

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
inst✝ : Mul α
⊢ (mapMulHom (MulHom.id α)) 1 = (MonoidHom.id (WithOne α)) 1

pp: case coe
α : Type u
inst✝ : Mul α
a✝ : α
⊢ (mapMulHom (MulHom.id α)) ↑a✝ = (MonoidHom.id (WithOne α)) ↑a✝

Tactic:
<;>

Goal state after:
case one
α : Type u
inst✝ : Mul α
⊢ (mapMulHom (MulHom.id α)) 1 = (MonoidHom.id (WithOne α)) 1

case coe
α : Type u
inst✝ : Mul α
a✝ : α
⊢ (mapMulHom (MulHom.id α)) ↑a✝ = (MonoidHom.id (WithOne α)) ↑a✝
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ (mapMulHom g) ((mapMulHom f) 1) = (mapMulHom (g.comp f)) 1

pp: case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a✝ : α
⊢ (mapMulHom g) ((mapMulHom f) ↑a✝) = (mapMulHom (g.comp f)) ↑a✝

Tactic:
<;>

Goal state after:
case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ (mapMulHom g) ((mapMulHom f) 1) = (mapMulHom (g.comp f)) 1

case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a✝ : α
⊢ (mapMulHom g) ((mapMulHom f) ↑a✝) = (mapMulHom (g.comp f)) ↑a✝
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
⊢ (mapMulHom e.symm.toMulHom) ((mapMulHom e.toMulHom) 1) = 1

pp: case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
a✝ : α
⊢ (mapMulHom e.symm.toMulHom) ((mapMulHom e.toMulHom) ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
⊢ (mapMulHom e.symm.toMulHom) ((mapMulHom e.toMulHom) 1) = 1

case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
a✝ : α
⊢ (mapMulHom e.symm.toMulHom) ((mapMulHom e.toMulHom) ↑a✝) = ↑a✝
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
⊢ (mapMulHom e.toMulHom) ((mapMulHom e.symm.toMulHom) 1) = 1

pp: case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
a✝ : β
⊢ (mapMulHom e.toMulHom) ((mapMulHom e.symm.toMulHom) ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case one
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
⊢ (mapMulHom e.toMulHom) ((mapMulHom e.symm.toMulHom) 1) = 1

case coe
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
a✝ : β
⊢ (mapMulHom e.toMulHom) ((mapMulHom e.symm.toMulHom) ↑a✝) = ↑a✝
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

pp: case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)

Tactic:
<;>

Goal state after:
case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
by
  rw [← cocone_naturality F f]
  rfl

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

Goal state before:
pp: case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

pp: case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)

Tactic:
<;>

Goal state after:
case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j : J
⊢ (F.obj j).hom ≫ s.ι.app j = (((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).obj j).hom

Tactic:
obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
hik : i ⟶ k
hjk : j ⟶ k
⊢ (F.obj j).hom ≫ s.ι.app j = (((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).obj j).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: 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 := ⋯ }

pp: 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 := ⋯ }

Tactic:
<;>

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.Topology.Algebra.Module.Equiv

Goal state before:
pp: case hl
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₃
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inl R M₃ M₂) x✝ = (g.coprod f ∘SL inl R M₃ M₂) x✝

pp: case hr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₂
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inr R M₃ M₂) x✝ = (g.coprod f ∘SL inr R M₃ M₂) x✝

Tactic:
<;>

Goal state after:
case hl
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₃
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inl R M₃ M₂) x✝ = (g.coprod f ∘SL inl R M₃ M₂) x✝

case hr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₂
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inr R M₃ M₂) x✝ = (g.coprod f ∘SL inr R M₃ M₂) x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: 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 := ⋯ }

pp: 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 := ⋯ }

Tactic:
<;>

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.Presentable.Finite

Goal state before:
pp: 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] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

pp: 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] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F

Tactic:
<;>

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] [IsCardinalFiltered 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] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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: case refine_1
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasCardinalFilteredColimits C ℵ₀
H : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape J C
⊢ ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C

pp: 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] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape J C

Tactic:
<;>

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasCardinalFilteredColimits C ℵ₀
H : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered 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] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape J C
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ isCardinalPresentable C κ ≤ isCardinalPresentable C κ'

Tactic:
intro X hX

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : isCardinalPresentable C κ X
⊢ isCardinalPresentable C κ' X
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
⊢ IsCardinalFiltered J₂ κ

Tactic:
obtain ⟨h₁, h₂⟩ := (Functor.final_iff_of_isFiltered F).1 inferInstance

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ IsCardinalFiltered J₂ κ
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case hC
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
x✝ : ↑A
⊢ ((Hom.hom
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
              ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f))).comp
        MvPolynomial.C)
      x✝ =
    ((Hom.hom f).comp MvPolynomial.C) x✝

pp: case hX
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
i✝ : σ
⊢ (Hom.hom
        ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
          ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f)))
      (MvPolynomial.X i✝) =
    (Hom.hom f) (MvPolynomial.X i✝)

Tactic:
<;>

Goal state after:
case hC
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
x✝ : ↑A
⊢ ((Hom.hom
            ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
              ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f))).comp
        MvPolynomial.C)
      x✝ =
    ((Hom.hom f).comp MvPolynomial.C) x✝

case hX
R✝ A✝ B C : CommRingCat
inst✝² : TopologicalSpace ↑R✝
σ : Type v
R A : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
f : of (MvPolynomial σ ↑A) ⟶ R
i✝ : σ
⊢ (Hom.hom
        ((fun fx ↦ ofHom (MvPolynomial.eval₂Hom (Hom.hom fx.1) fx.2))
          ((fun f ↦ (ofHom MvPolynomial.C ≫ f, fun i ↦ (ConcreteCategory.hom f) (MvPolynomial.X i))) f)))
      (MvPolynomial.X i✝) =
    (Hom.hom f) (MvPolynomial.X i✝)