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

Goal state before:
pp: α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
comm : ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) = ⇑e ∘ fun t ↦ t.2 / t.1
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

Tactic:
have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
    simpa using! (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)

Goal state after:
α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
comm : ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) = ⇑e ∘ fun t ↦ t.2 / t.1
lim : Tendsto (fun x ↦ x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1))
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
inst✝² : IsTopologicalRing K
inst✝¹ : CompactSpace K
inst✝ : T2Space K
⊢ Finite K

Tactic:
suffices DiscreteTopology K by
    exact finite_of_compact_of_discrete

Goal state after:
K : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
inst✝² : IsTopologicalRing K
inst✝¹ : CompactSpace K
inst✝ : T2Space K
⊢ DiscreteTopology K
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
u : α
au : u ∈ Ioc a b
hu : Ico a u ⊆ v
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

Tactic:
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ico a u ⊆ s) → ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a ε : α
hε : 1 < ε
⊢ {x | (fun x ↦ |x / a|ₘ < ε) x} ∈ 𝓟 {b | |a / b|ₘ < ε}

Tactic:
by simp only [mabs_div_comm, mem_principal_self]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
← h.image_eq,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ ↑e '' (e.source ∩ s) = e'.target ∩ t
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: M N : AddCommGrpCat
f : M ⟶ N
hf : Function.Injective ⇑(ConcreteCategory.hom f)
hN : Finite ↑N
⊢ Finite ↑M

Tactic:
exact Finite.of_injective _ hf

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective ⇑(CharacterModule.dual (Quot.desc F c).toIntLinearMap)

Tactic:
refine ⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
⊢ χ = ψ

case refine_2
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
⊢ ∃ a, (CharacterModule.dual (Quot.desc F c).toIntLinearMap) a = χ
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
          ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨x, hx⟩)) =
        Quot.mk (EndpointIdent p a) ⟨x, hx⟩

Tactic:
dsimp only

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (x : 𝕜) (hx : x ∈ Icc a (a + p)),
    x ≠ a + p →
      Quot.mk (EndpointIdent p a)
          (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨x, hx⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
        Quot.mk (EndpointIdent p a) ⟨x, hx⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
      ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩

Tactic:
dsimp only

Goal state after:
case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ Icc a (a + p)
⊢ Quot.mk (EndpointIdent p a)
      (Set.inclusion ⋯ ((equivIco p a) ((Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩).liftOn (fun x ↦ ↑↑x) ⋯))) =
    Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 1 • (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x

pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • (ConcreteCategory.hom f) x = 0

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
x₂' : A ⟶ S.X₂
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ S.liftCycles x₂ hx₂ = π ≫ S.liftCycles x₂' hx₂' + x₁ ≫ S.toCycles

Tactic:
simp [liftCycles_comp_homologyπ_eq_iff_up_to_refinements, ← cancel_mono S.iCycles]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.PIsoUnopOpP'.inv ≫
      (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    S.PIsoUnopOpP'.inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom

Tactic:
PIsoUnopOpP',

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.op.δ.unop ≫ pushout.inr S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom =
    (pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃).inv ≫
      (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁) ≫
        (pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
⊢ ∀ (X : WalkingMulticospan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMulticospan.left a => I.left a
          | WalkingMulticospan.right b => I.right b)
      | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b
      | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMulticospan.left a => I.left a
        | WalkingMulticospan.right b => I.right b)

Tactic:
by
    rintro (_ | _) <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
⊢ ∀ (X : WalkingMultispan J),
    (match X, X, 𝟙 X with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
      𝟙
        (match X with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)

Tactic:
by
    rintro (_ | _) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
Category.comp_id,

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = { f := s.ι.f ≫ T.ε.app X.A, h := ⋯ }.f

Tactic:
dsimp only

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
m : s.pt ⟶ (beckCoalgebraFork X).pt
hm : m ≫ (beckCoalgebraFork X).ι = s.ι
⊢ m.f = s.ι.f ≫ T.ε.app X.A
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        𝟙 (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
Category.comp_id,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ f ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (ofParallelHoms J f g).fstPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    ((ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
          (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
        𝟙 (Fan.mk Y fun x ↦ (Iso.refl Y).hom).pt) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝

Tactic:
Category.comp_id,

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J✝ : MulticospanShape
I : MulticospanIndex J✝ C
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
inst✝³ : HasProduct I.left
inst✝² : HasProduct I.right
J : MulticospanShape
inst✝¹ : Unique J.L
inst✝ : Unique J.R
X Y : C
f g : X ⟶ Y
x✝ : J.R
⊢ (Iso.refl (Fan.mk X fun x ↦ (Iso.refl X).hom).pt).hom ≫ g ≫ (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝ =
    (ofParallelHoms J f g).sndPiMapOfIsLimit (Fan.mk X fun x ↦ (Iso.refl X).hom)
        (Fan.isLimitMkOfUnique (Iso.refl Y) J.R) ≫
      (Fan.mk Y fun x ↦ (Iso.refl Y).hom).proj x✝
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (h.counit.app (L.obj (R.obj X)) ≫ h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)

Tactic:
← Adjunction.counit_naturality,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (L.map (R.map (h.counit.app X)) ≫ h.counit.app X) =
    R.map (L.map (R.map (h.counit.app X))) ≫ R.map (h.counit.app X)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.A ≅ ((Monad.comparison (reflectorAdjunction R)).obj ((reflector R).obj X.A)).A

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).toMonad.map (Iso.hom ?refine_1) ≫
      ((Monad.comparison (reflectorAdjunction R)).obj ((reflector R).obj X.A)).a =
    X.a ≫ Iso.hom ?refine_1

Tactic:
· exact asIso ((reflectorAdjunction R).unit.app X.A)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).toMonad.map (asIso ((reflectorAdjunction R).unit.app X.A)).hom ≫
      ((Monad.comparison (reflectorAdjunction R)).obj ((reflector R).obj X.A)).a =
    X.a ≫ (asIso ((reflectorAdjunction R).unit.app X.A)).hom
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.η.app (D.obj j).A ≫ T.map (c.ι.1 j) ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt

Tactic:
commuting,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.η.app (D.obj j).A ≫ (D.obj j).a ≫ c.ι.app j = c.ι.app j ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ T.map (c.ι.app j) ≫ lambda c t = T.map (T.map (c.ι.app j) ≫ lambda c t) ≫ lambda c t

Tactic:
commuting,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map ((D.obj j).a ≫ c.ι.app j) ≫ lambda c t
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (T.map (c.ι.app j) ≫ lambda c t) ≫ t.desc (T.forget.mapCocone s)

Tactic:
commuting,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = ((D.obj j).a ≫ c.ι.app j) ≫ t.desc (T.forget.mapCocone s)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := zero) (𝟙 _))
        (fun p h₁ h₂ ↦ ?_)
      have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁
      have hᵣ : StructuredArrow.mk right ∈ p := (h₂ (StructuredArrow.homMk .right)).1 h₁
      rintro ⟨⟨⟨⟩⟩, (_ | _), ⟨_⟩⟩
      · exact (h₂ (StructuredArrow.homMk .left)).2 hₗ
      · exact (h₂ (StructuredArrow.homMk .right)).2 hᵣ
      all_goals assumption

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
⊢ HasColimit F

Tactic:
by
      let c := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
      let : PreservesColimitsOfShape J _ :=
        (monadicAdjunction R).leftAdjoint_preservesColimits.1
      let t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit _)
      apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩
      apply
        (isoWhiskerLeft F (asIso (monadicAdjunction R).counit) :) ≪≫ F.rightUnitor

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (lambda c t ≫ T.map (c.π.1 j)) ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j

Tactic:
commuting,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ lambda c t ≫ T.map (c.π.app j) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (lambda c t ≫ T.map (c.π.app j))

Tactic:
commuting,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ lambda c t ≫ T.map (c.π.app j) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j ≫ (D.obj j).a)