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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
⊢ IsQuotientMap ((fun x ↦ c • x) ∘ ⇑f)

Tactic:
convert! hf.comp hc.isHomeomorph_smul.isQuotientMap

Goal state after:
M : Type u_1
α : Type u_2
inst✝⁸ : Monoid M
inst✝⁷ : TopologicalSpace α
inst✝⁶ : MulAction M α
inst✝⁵ : ContinuousConstSMul M α
S : Type u_4
β : Type u_5
inst✝⁴ : SMul S M
inst✝³ : SMul S α
inst✝² : IsScalarTower S M α
inst✝¹ : SMul S β
f : α →ₑ[id] β
inst✝ : TopologicalSpace β
hf : IsQuotientMap ⇑f
c : S
hc : IsUnit (c • 1)
⊢ (fun x ↦ c • x) ∘ ⇑f = ⇑f ∘ fun x ↦ (c • 1) • x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G : Type u_1
inst✝ : Group G
u₁ u₂ : UniformSpace G
h₁ : IsUniformGroup G
h₂ : IsUniformGroup G
⊢ IsUniformGroup G

Tactic:
rw [inf_eq_iInf]
  refine isUniformGroup_iInf fun b => ?_
  cases b <;> assumption

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, K * V ⊆ U

Tactic:
refine hK.induction_on ?_ ?_ ?_ ?_
  · exact ⟨univ, by simp⟩
  · rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
  · rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')
  · intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
s : Set M
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 (1 * 1)

Tactic:
simpa only [one_mul] using! hs

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : TopologicalSpace G✝
inst✝⁴ : Group G✝
inst✝³ : SeparatelyContinuousMul G✝
N✝ : Subgroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun p ↦ p.1 • p.2

Tactic:
rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ s⁻¹⁻¹ * t⁻¹⁻¹ = s * t

Tactic:
inv_inv,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ s * t⁻¹⁻¹ = s * t
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ closure[inst✝²] s / t = s / t

Tactic:
by
  simp_rw [div_eq_mul_inv, ht.inv.closure_mul]

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

Goal state before:
pp: G : Type w
inst✝ : Inv G
t₁ t₂ : TopologicalSpace G
h₁ : ContinuousInv G
h₂ : ContinuousInv G
⊢ ContinuousInv G

Tactic:
rw [inf_eq_iInf]
  refine continuousInv_iInf fun b => ?_
  cases b <;> assumption

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen[inst✝²] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
⊢ ∃ V ∈ 𝓝 1, IsClosed[inst✝²] V ∧ V⁻¹ = V ∧ V * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : s.topologicalClosure = ⊤
⊢ (Subgroup.map f s).topologicalClosure = ⊤

Tactic:
by
  rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
  exact hf'.dense_image hf hs

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ x * g) '' U ∩ U).Nonempty → g = 1

Tactic:
by
  have ⟨U, hU, hUinv, h⟩ := hS.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty
  refine ⟨U, hU, hUinv, fun g hgS hgU ↦ inv_eq_one.mp (h _ (S.inv_mem hgS) ?_)⟩
  rwa [Set.nonempty_image_mulLeft_inv_inter_iff, hUinv]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atBot ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : RingTopology R
⊢ f.toTopologicalSpace = g.toTopologicalSpace → f = g

Tactic:
_

Goal state after:
R : Type u_1
inst✝ : Ring R
f g : RingTopology R
a✝ : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (Units.val ∘ (unitsEquivPos R).invFun) ∧ Continuous fun x ↦ ↑((unitsEquivPos R).invFun x)⁻¹

Tactic:
refine ⟨by fun_prop, ?_⟩

Goal state after:
K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous fun x ↦ ↑((unitsEquivPos R).invFun x)⁻¹
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ p ∈ (fun p ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
rw [mem_preimage, uIcc_of_le h]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ Icc p.1 p.2 ∈ s
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
⊢ b * a ∈ Ioo (a ^ m) (a ^ (m + 1))

Tactic:
simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢

Goal state after:
case h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ m / a < b
⊢ a ^ m < b * a ∧ b < a ^ m
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
x : α
⊢ |f x| ≤ C → 0 ≤ (abs ∘ fun x ↦ f x * g x) x

Tactic:
_

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
x : α
a✝ : |f x| ≤ C
⊢ 0 ≤ (abs ∘ fun x ↦ f x * g x) x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Iio a))
⊢ i✝ ∈ s.1 → (Ioi ↑i✝).OrdConnected

Tactic:
_

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Iio a))
hi✝ : i✝ ∈ s.1
⊢ (Ioi ↑i✝).OrdConnected
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Ioi a))
⊢ i✝ ∈ s.2 → (Iio ↑i✝).OrdConnected

Tactic:
_

Goal state after:
case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Ioi a))
hi✝ : i✝ ∈ s.2
⊢ (Iio ↑i✝).OrdConnected
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ u, a < u
hl : ∃ l, l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ Tendsto f x (𝓝 a)

Tactic:
by
  simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
  exact fun l hl u => h l u hl

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : OrderTopology α
⊢ 𝓝 ⊤ = ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l)

Tactic:
by simp [nhds_eq_order (⊤ : α)]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
e : A ≃ₗ[R] B
⊢ dual ↑e.symm ∘ₗ dual ↑e = LinearMap.id

Tactic:
ext c _; exact congr(c $(e.right_inv _))

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ atTop.IsCountablyGenerated

Tactic:
rw [atTop_eq_pure_of_isTop hx]
    exact isCountablyGenerated_pure x

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
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f

Tactic:
intro A₀

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
⊢ ∀ (x₂ : A₀ ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
⊢ IsIso φ

Tactic:
rw [isIso_iff_bijective]

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
⊢ Function.Bijective ⇑(hom φ)
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
a₁✝ : X₁
⊢ ∀ ⦃a₂ : (fun X ↦ X) X₁⦄, (hom φ) a₁✝ = (hom φ) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
case left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
a₁✝ a₂✝ : X₁
⊢ (hom φ) a₁✝ = (hom φ) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
⊢ Function.RightInverse
    (fun x ↦
      ⟨fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
        ⋯⟩)
    fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩

Tactic:
by
    intro x
    ext i
    rfl

Goal state after:
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
⊢ h.toMonad.μ.app (R.obj X) ≫ R.map (h.counit.app X) = h.toMonad.map (R.map (h.counit.app X)) ≫ R.map (h.counit.app X)

Tactic:
by
        dsimp
        rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]

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

Goal state before:
pp: X✝ : WalkingReflexivePair
⊢ ∀ {Y : WalkingReflexivePair} (f : X✝.Hom Y), (Hom.id X✝).comp f = f

Tactic:
_

Goal state after:
X✝ Y✝ : WalkingReflexivePair
⊢ ∀ (f : X✝.Hom Y✝), (Hom.id X✝).comp f = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: X✝ : WalkingReflexivePair
⊢ ∀ {Y : WalkingReflexivePair} (f : X✝.Hom Y), f.comp (Hom.id Y) = f

Tactic:
_

Goal state after:
X✝ Y✝ : WalkingReflexivePair
⊢ ∀ (f : X✝.Hom Y✝), f.comp (Hom.id Y✝) = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: W✝ : WalkingReflexivePair
⊢ ∀ {X Y Z : WalkingReflexivePair} (f : W✝.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_

Goal state after:
W✝ X✝ : WalkingReflexivePair
⊢ ∀ {Y Z : WalkingReflexivePair} (f : W✝.Hom X✝) (g : X✝.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: W✝ X✝ : WalkingReflexivePair
⊢ ∀ {Y Z : WalkingReflexivePair} (f : W✝.Hom X✝) (g : X✝.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_

Goal state after:
W✝ X✝ Y✝ : WalkingReflexivePair
⊢ ∀ {Z : WalkingReflexivePair} (f : W✝.Hom X✝) (g : X✝.Hom Y✝) (h : Y✝.Hom Z), (f.comp g).comp h = f.comp (g.comp h)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: W✝ X✝ Y✝ : WalkingReflexivePair
⊢ ∀ {Z : WalkingReflexivePair} (f : W✝.Hom X✝) (g : X✝.Hom Y✝) (h : Y✝.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_

Goal state after:
W✝ X✝ Y✝ Z✝ : WalkingReflexivePair
⊢ ∀ (f : W✝.Hom X✝) (g : X✝.Hom Y✝) (h : Y✝.Hom Z✝), (f.comp g).comp h = f.comp (g.comp h)
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

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

Goal state after:
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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map,
        (D.obj j).unit]

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 : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ c.π.app j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: X✝ : WalkingParallelPair
⊢ ∀ {Y Z : WalkingParallelPair} (f : X✝ ⟶ Y) (g : Y ⟶ Z),
    (match Z, X✝, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y, X✝, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z, Y, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)

Tactic:
_

Goal state after:
X✝ Y✝ : WalkingParallelPair
⊢ ∀ {Z : WalkingParallelPair} (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z),
    (match Z, X✝, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y✝, X✝, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z, Y✝, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: X✝ Y✝ : WalkingParallelPair
⊢ ∀ {Z : WalkingParallelPair} (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z),
    (match Z, X✝, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y✝, X✝, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z, Y✝, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)

Tactic:
_

Goal state after:
X✝ Y✝ Z✝ : WalkingParallelPair
⊢ ∀ (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝),
    (match Z✝, X✝, f ≫ g with
      | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
      | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
      | x, .(x), WalkingParallelPairHom.id .(x) =>
        Hom.id
          (match x with
          | one => WalkingReflexivePair.zero
          | zero => WalkingReflexivePair.one)) =
      (match Y✝, X✝, f with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)) ≫
        match Z✝, Y✝, g with
        | .(one), .(zero), WalkingParallelPairHom.left => Hom.left
        | .(one), .(zero), WalkingParallelPairHom.right => Hom.right
        | x, .(x), WalkingParallelPairHom.id .(x) =>
          Hom.id
            (match x with
            | one => WalkingReflexivePair.zero
            | zero => WalkingReflexivePair.one)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 _proof_361✝ ≅ g.obj' 0 _proof_361✝
app₁ : f.obj' 1 _proof_362✝ ≅ g.obj' 1 _proof_362✝
app₂ : f.obj' 2 _proof_363✝ ≅ g.obj' 2 _proof_363✝
app₃ : f.obj' 3 _proof_364✝ ≅ g.obj' 3 _proof_364✝
app₄ : f.obj' 4 _proof_365✝ ≅ g.obj' 4 _proof_365✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_362✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_362✝
w₁ : f.map' 1 2 _proof_246✝ _proof_363✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_363✝
w₂ : f.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_364✝
w₃ : f.map' 3 4 _proof_364✝ _proof_365✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_365✝
⊢ g.map' 2 3 _proof_299✝ _proof_364✝ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_299✝ _proof_364✝

Tactic:
by rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]

Goal state after: