mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U

Tactic:
refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀

Tactic:
simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff,
    UniformSpace.ball, @forall_comm _ ι]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
        (UniformSpace.comap Prod.fst (uniformSpace α β)) ⊓
      UniformSpace.comap (⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
        (UniformSpace.comap Prod.snd (uniformSpace α γ)) =
    uniformSpace α (β × γ)

Tactic:
← UniformSpace.comap_comap,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (Prod.fst ∘ ⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ)) (uniformSpace α β) ⊓
      UniformSpace.comap (⇑(Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ))
        (UniformSpace.comap Prod.snd (uniformSpace α γ)) =
    uniformSpace α (β × γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) ((fun i ↦ uniformSpace α (δ i)) i)) =
    uniformSpace α ((i : ι) → δ i)

Tactic:
← UniformSpace.comap_comap,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : Filter ι
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) ((fun i ↦ uniformSpace α (δ i)) i) =
    uniformSpace α ((i : ι) → δ i)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
by
  rw [map₂_swap m]
  exact map_map₂_distrib fun _ _ => h_antidistrib _ _

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 ↦ ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩

Tactic:
exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous ((⋃₀ 𝔖).domRestrict ∘ ⇑(toFun 𝔖))

Tactic:
rw [uniformContinuous_pi]
  intro ⟨x, hx⟩
  obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx
  exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i,
      UniformSpace.comap (fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f)))
        (UniformSpace.comap (Function.eval i) (UniformFun.uniformSpace (↑↑i) β)) =
    uniformSpace α β 𝔖

Tactic:
← UniformSpace.comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i,
      UniformSpace.comap (Function.eval i ∘ fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f)))
        (UniformFun.uniformSpace (↑↑i) β) =
    uniformSpace α β 𝔖
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
⊢ CompleteSpace (α →ᵤ[𝔖] β)

Tactic:
by
  rcases isEmpty_or_nonempty β
  · infer_instance
  · refine ⟨fun {F} hF ↦ ?_⟩
    have := hF.1
    have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
      CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))
    choose! g hg using this
    use ofFun 𝔖 g
    simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]
    intro s hs U ⟨hU, hUc⟩
    rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩
    filter_upwards [hV] with f hf x hx
    refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_
    filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
s : Set α
hs : s ∈ f
⊢ s ^ 0 ∈ f ^ 0

Tactic:
rw [pow_zero]
    exact one_mem_one

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap Function.swap (UniformSpace.comap (Function.eval i) (uniformSpace α (δ i) 𝔖)) =
    uniformSpace α ((i : ι) → δ i) 𝔖

Tactic:
← UniformSpace.comap_comap,

Goal state after:
case e_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap (Function.eval i ∘ Function.swap) (uniformSpace α (δ i) 𝔖) = uniformSpace α ((i : ι) → δ i) 𝔖
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
have := image_comp (fun x => a + x) fun x => -x; dsimp [Function.comp_def] at this
  simp [sub_eq_add_neg, this, add_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : C(α, β)
⊢ (fun f ↦ { toFun := f, continuous_toFun := ⋯ }) ((fun f ↦ ⇑f) x✝) = x✝

Tactic:
by ext; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
f g : C(α, β)
inst✝ : DiscreteTopology α
x✝ : α → β
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f, continuous_toFun := ⋯ }) x✝) = x✝

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
⊢ IsClosedMap f

Tactic:
rw [isClosedMap_iff_clusterPt]
  exact fun s y ↦ h.clusterPt_of_mapClusterPt (ℱ := 𝓟 s) (y := y)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousWithinAt (fun a ↦ (List.map (fun i ↦ f i a) l).prod) t x

Tactic:
rw [continuousWithinAt_iff_continuousAt_domRestrict _ hx]

Goal state after:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
f : ι → X → M
l : List ι
t : Set X
h : ∀ i ∈ l, ContinuousOn (f i) t
x : X
hx : x ∈ t
⊢ ContinuousAt (t.domRestrict fun a ↦ (List.map (fun i ↦ f i a) l).prod) ⟨x, hx⟩
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ IsProperMap f ↔ Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Tactic:
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto,
    le_cofinite_iff_compl_singleton_mem, mem_map, preimage_compl]
  refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
    ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩
  rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩
  exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
    (compl_le_compl_iff_le.mp hKy)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
h : Tendsto f l atTop
⊢ Tendsto (fun x ↦ r⁻¹ * (r * f x)) l atTop

Tactic:
by simpa only [inv_mul_cancel_left₀ hr.ne']

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) ∪ {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) =
    univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
pi_univ_Ioc_update_right hm.2,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ (({z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) ∪ {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)) =
    univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ univ.pi fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i, Icc x (update z i (y i))

Tactic:
rintro a ⟨⟨hax, haz⟩, hay⟩
  simpa [not_and_or, hax, le_update_iff, haz _] using hay

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_2.inl
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)

pp: case refine_2.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)

Tactic:
· simp only [h.left, h.right, zpow_zero, mul_one]
      exact tendsto_const_nhds

Goal state after:
case refine_2.inr
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans (PartialEquiv.refl β)).source = e.source

Tactic:
simp [trans_source]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
simp [trans_source]

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

Goal state before:
pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
have k_eq : k = kl ∪ kr := by
    -- this `have` can be removed, but makes `grind` slower
    have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
    ext
    grind

Goal state after:
case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ toIcoMod hp a x = toIocMod hp a x

Tactic:
← not_modEq_iff_toIcoMod_eq_toIocMod hp,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ¬a ≡ x [PMOD p]
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
h : (ofSpanSingleton a) ⟨a, ⋯⟩ = 0
⊢ a = 0

Tactic:
ofSpanSingleton,

Goal state after:
A : Type uA
inst✝ : AddCommGroup A
a : A
h :
  (Submodule.liftQSpanSingleton (↑(addOrderOf a))
            (AddMonoidHom.toIntLinearMap (int.divByNat (if addOrderOf a = 0 then 2 else addOrderOf a))) ⋯ ∘ₗ
          ↑(intSpanEquivQuotAddOrderOf a)).toAddMonoidHom
      ⟨a, ⋯⟩ =
    0
⊢ a = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (a_1 : ↑(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_1)) =
      Quot.mk (EndpointIdent p a) a_1

Tactic:
by
      rintro ⟨x, hx⟩
      rcases ne_or_eq x (a + p) with (h | rfl)
      · revert x
        dsimp only
        intro x hx h
        congr
        ext1
        apply congr_arg Subtype.val ((equivIco p a).right_inv ⟨x, hx.1, hx.2.lt_of_ne h⟩)
      · rw [← Quot.sound EndpointIdent.mk]
        dsimp only
        congr
        ext1
        apply congr_arg Subtype.val
          ((equivIco p a).right_inv ⟨a, le_refl a, lt_add_of_pos_right a hp.out⟩)

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : HopfAlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝³ ◁ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ X₂✝
x✝ : HopfAlgCat R
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ▷ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ⊗ₘ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
      ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝) ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (α_ x✝² x✝¹ x✝).hom).toBialgHom')) =
    (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x)
          (((Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                  ((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ⊗ᵢ
                    Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
                α_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ≪≫
                  (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ⊗ᵢ
                      Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)) ≪≫
                    Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝¹ ⊗ x✝))).hom.toBialgHom'))

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (λ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R (𝟙_ (HopfAlgCat R)).carrier x✝.carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)) ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                ((Iso.refl (𝟙_ (BialgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
              λ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
by ext; rfl

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (ρ_ x✝).hom).toBialgHom') =
    (TensorProduct.mk R x✝.carrier (𝟙_ (HopfAlgCat R)).carrier).compr₂ₛₗ
      ((fun x ↦ ↑x)
        (((Iso.refl
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ⊗
                      (forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R)))).symm ≪≫
                (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ⊗ᵢ (Iso.refl (𝟙_ (BialgCat R))).symm)) ≪≫
              ρ_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom.toBialgHom')

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (μIso R X Y).inv) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
dsimp [μIso, freeMk]
  erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

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

Tactic:
by
  rw [epi_iff_surjective_up_to_refinements]
  constructor
  · intro h A y₂ hy₂
    obtain ⟨A₁, π₁, hπ₁, γ, hγ⟩ := h (S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ)
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
    replace hγ := π₂ ≫= hγ
    simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements] at hγ
    obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := hγ
    exact ⟨A₃, π₃ ≫ π₂ ≫ π₁, inferInstance, π₃ ≫ x₂, by simp only [assoc, hx₂, comp_zero],
      x₁, by simpa only [assoc] using hx₁⟩
  · intro h A γ
    obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_up_to_refinements γ
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ hy₂
    refine ⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ, ?_⟩
    simp only [assoc, fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements]
    exact ⟨A₂, 𝟙 _, inferInstance, y₁, by simpa only [id_comp] using hy₁⟩

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.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₀₂, zero_τ₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case mp
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ IsPullback t l r b →
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (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₃

Tactic:
intro h
    exact ⟨h.w, fun x₁ y₁ ⟨h₁, h₂⟩ ↦ ext_of_isPullback h h₁ h₂, exists_of_isPullback h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: case mpr
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ (t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (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₃) →
    IsPullback t l r b

Tactic:
· rintro ⟨w, h₁, h₂⟩
    let φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨⟨t x₁, l x₁⟩, congr_hom w x₁⟩
    have hφ : IsIso φ := by
      rw [isIso_iff_bijective]
      constructor
      · intro _ _ h
        simp [φ] at h
        grind
      · intro x
        obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)
        cat_disch
    exact ⟨⟨w⟩, ⟨IsLimit.ofIsoLimit ((Types.pullbackLimitCone r b).isLimit)
      (PullbackCone.ext (asIso φ)).symm⟩⟩

Goal state after: