mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
⊢ Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
uv_disj

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case insert
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝ : Set X
s✝ : Set (Set X)
ha : a✝ ∉ s✝
hsf : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → (∀ t ∈ s✝, Dense t) → Dense (⋂₀ s✝)
ho : ∀ t ∈ insert a✝ s✝, IsOpen[inst✝] t
hd : ∀ t ∈ insert a✝ s✝, Dense t
⊢ Dense (⋂₀ insert a✝ s✝)

Tactic:
| insert ha hsf ih =>

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.zero
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
hn : 0 < 0
⊢ ∃ U, (∀ (i : Fin 0), IsClopen (U i)) ∧ (∀ (i : Fin 0), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
simp at hn

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

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
⊢ DiscreteUniformity Y

Tactic:
have h : SetRel.id = ⋂ y : Y, {p | p.2 = y → p.1 ∈ ({y} : Set Y)} := by
    ext x
    simp [SetRel.id]

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ DiscreteUniformity Y
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
⊢ CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
by
  simp only [cauchySeq_iff', Filter.eventually_atTop_prod_self', mem_preimage, Prod.map_apply]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift' fun s ↦ {y | (y, a) ∈ s}) ×ˢ (𝓤 α).lift' (ball b) =
    (𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
prod_lift'_lift'

Goal state after:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ((𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ ball b t) =
    (𝓤 α).lift fun s ↦ (𝓤 α).lift' fun t ↦ {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone fun s ↦ {y | (y, a) ∈ s}

case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ Monotone (ball b)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
let u := k ∩ { y | ∃ x ∈ s, (x, y) ∈ r }

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
s : Set (UniformSpace α)
⊢ (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace

Tactic:
rw [sInf_eq_iInf]
  simp only [← toTopologicalSpace_iInf]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f

Tactic:
refine ⟨le_antisymm ?_ hf.le_comap⟩
  rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
  exact comap_mono hg.le_comap

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i ↦ F i x) p)

Tactic:
simp only [cauchy_map_iff, hp, true_and]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p ↦ (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : β → α
hm : IsUniformInducing m
dense : DenseRange m
h : ∀ (f : Filter β), Cauchy f → ∃ x, map m f ≤ 𝓝 x
f : Filter α
hf : Cauchy f
p : Set (α × α) → Set α → Set α := fun s t ↦ {y | ∃ x ∈ t, (x, y) ∈ s}
g : Filter α := (𝓤 α).lift fun s ↦ f.lift' (p s)
mp₀ : Monotone p
mp₁ : ∀ {s : Set (α × α)}, Monotone (p s)
this✝⁵ : f ≤ g
this✝⁴ : g.NeBot
this✝³ : (comap m g).NeBot
this✝² : Cauchy g
this✝¹ : Cauchy (comap m g)
x : α
hx : map m (comap m g) ≤ 𝓝 x
this✝ : ClusterPt x (map m (comap m g))
this : ClusterPt x g
⊢ f ≤ g

Tactic:
by assumption

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen[inst✝.toTopologicalSpace] (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ j, ball x (V i) ⊆ U j

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen[inst✝.toTopologicalSpace] (U j)
hcover : K ⊆ ⋃ j, U j
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ i, ball x t ⊆ U i) → ∀ x ∈ K, ∃ i, ball x s ⊆ U i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s

Tactic:
have := le_max_left m n

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
this : m ≤ max m n
⊢ setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousAt F x₀
⊢ EquicontinuousAt F x₀

Tactic:
rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢

Goal state after:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F univ x₀
⊢ EquicontinuousWithinAt F univ x₀
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
⊢ EquicontinuousWithinAt (u ∘ Subtype.val) S x₀

Tactic:
by
  intro U hU
  rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩
  filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS
  rw [SetCoe.forall] at *
  change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx
  refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prodMk ?_).trans (preimage_mono hVU)
  exact (continuous_apply ⟨x, hxS⟩).comp hu₁

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 ∈ 1

Tactic:
exact one_mem_one

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)

Tactic:
exact ha.filter

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun x ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x ↦ x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
i : ι
⊢ uniformSpace α β 𝔖 ≤ UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x ↦ x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

Tactic:
rw [← uniformContinuous_iff_le_comap]
    exact UniformOnFun.precomp_uniformContinuous (h_image i)

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

Goal state before:
pp: case left
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun x i ↦ f i (x i)

pp: case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
· exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)

Goal state after:
case right
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
h :
  ∀ (i : ι),
    Continuous[inst✝¹ i, inst✝ i] (f i) ∧
      ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄,
    Tendsto (fun x i ↦ f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i ↦ f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i ↦ {x | x.1⁻¹ * x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one]
  exact h.comap _

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

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ x / c) (𝓝 a) = 𝓝 (a / c)

Tactic:
by
  convert! (Homeomorph.divRight c).map_nhds_eq .. using 2

Goal state after:
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₀ : α
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

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

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atTop l
⊢ Tendsto f (𝓝[>] 0) l

Tactic:
convert! h.comp tendsto_inv_nhdsGT_zero
  grind [inv_inv]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [@IsRightUniformGroup.uniformity_eq (G := G) us _ _]

Goal state after:
G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ 𝓤 G = comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) = N

Tactic:
convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
        · have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
          rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
        · exact (Submodule.range_subtype _).symm

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ (Hom.hom ((free R).map (α_ X Y Z).hom)) (freeMk ((((x, y), z).1.1, ((x, y), z).1.2), ((x, y), z).2)) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))

Tactic:
free_map_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
z : Z
x : X
y : Y
⊢ freeMk ((ConcreteCategory.hom (α_ X Y Z).hom) ((((x, y), z).1.1, ((x, y), z).1.2), ((x, y), z).2)) =
    (Hom.hom (μIso R X (Y ⊗ Z)).hom)
      ((Hom.hom ((free R).obj X ◁ (μIso R Y Z).hom))
        ((Hom.hom (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom)
          (freeMk ((x, y), z).1.1 ⊗ₜ[R] freeMk ((x, y), z).1.2 ⊗ₜ[R] freeMk ((x, y), z).2)))
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ((f + f').sum fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) =
    (sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) +
      sum f' fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ 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:
y₂

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
⊢ y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (sum f fun f' s ↦ (g + g').sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    (sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) +
      sum f fun f' s ↦ sum g' fun g' t ↦ single (f' ≫ g') (s * t)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((r • f).sum fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s ↦ (r • g).sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)
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₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ 𝟙 A₂ ≫ π₂ ≫ y₂ = 𝟙 A₂ ≫ x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
simpa only [id_comp] using hy₁

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ single f r ≫ single g s = single (f ≫ g) (r * s)

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ ((single f r).sum fun f' s_1 ↦ (single g s).sum fun g' t ↦ single (f' ≫ g') (s_1 * t)) = single (f ≫ g) (r * s)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
⊢ ∀ (X : Free R C), (sum (𝟙 X) fun f' r ↦ r • F.map f') = 𝟙 (F.obj X)

Tactic:
dsimp +instances [CategoryTheory.categoryFree]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
⊢ ∀ (X : Free R C), ((single (𝟙 X) 1).sum fun f' r ↦ r • F.map f') = 𝟙 (F.obj X)
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
inst✝ : Epi S.L₂.g
⊢ Epi (S.L₂.g ≫ S.v₂₃.τ₃)

Tactic:
apply epi_comp

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
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.a ≫ (reflectorAdjunction R).unit.app X.A = 𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
rw [← (reflectorAdjunction R).unit_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
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app ((reflector R ⋙ R).obj X.A) ≫ R.map ((reflector R).map X.a) =
    𝟙 ((reflector R ⋙ R).obj X.A)
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.map (c.π.app j) ≫ (D.obj j).a = 𝟙 c.pt ≫ c.π.app j

Tactic:
← T.η.naturality_assoc,

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).map (c.π.app j) ≫ T.η.app (D.obj j).A ≫ (D.obj j).a = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case inr.inl
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I.toLinearOrder
h : I.SymmStruct
x : ι
⊢ I.fst (x, x) ≫ c.π ((MultispanShape.prod ι).fst (x, x)) = I.snd (x, x) ≫ c.π ((MultispanShape.prod ι).snd (x, x))

Tactic:
simp [h.fst_eq_snd]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : HasEqualizerOfIsCosplitPair F
inst✝ : PreservesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by
    have := HasEqualizerOfIsCosplitPair.out F f g
    apply reflectsLimit_of_reflectsIsomorphisms⟩

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : HasEqualizerOfIsCosplitPair F
inst✝ : PreservesLimitOfIsCosplitPair F
this : ReflectsLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F