mathlib-initiative/mathlib-tactics huggingface dataset:
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
u : Set α := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
x : α
xs : x ∈ s
⊢ x ∈ SetRel.preimage r k → x ∈ U.preimage (range g)

Tactic:
⟨y, hy, xy⟩

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}
g : ↑u → α
hgs : ∀ (x : ↑u), g x ∈ s
hgr : ∀ (x : ↑u), (g x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
⊢ x ∈ U.preimage (range g)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t

Tactic:
exact hs.exists_subset_of_mem (Filter.mem_principal_self s) hU

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ UniformSpace.comap (⋃₀ 𝔖).domRestrict (uniformSpace fun i ↦ α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (uniformSpace fun i ↦ α ↑i)

Tactic:
simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]

Goal state after:
Module: Mathlib.Algebra.Order.Group.MinMax

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ |max a c - max b c| ≤ |a - b|

Tactic:
by
  simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
    using abs_max_sub_max_le_max a c b c

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = map₂ (fun a b ↦ m b a) g f

Tactic:
rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ UniformOnFun.gen 𝔖 s V ∈ ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈
    ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
    hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]
  simp only [Prod.forall]
  rfl

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
⊢ {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id U} ∈ F

Tactic:
rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
⊢ {g_1 | ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id U} ∈ F
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
⊢ ¬Disjoint f g → 1 ≤ f / g

Tactic:
rintro h s ⟨t₁, h₁, t₂, h₂, hs⟩

Goal state after:
case refine_2
α : Type u_2
inst✝ : Group α
f g : Filter α
h : ¬Disjoint f g
s t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
hs : t₁ / t₂ ⊆ s
⊢ s ∈ 1
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
hγz : (fun x ↦ γ • x) z ∈ V ∩ ⋂ γ, (fun x ↦ ↑γ • x) ⁻¹' u γ ∩ v γ
h : ¬γ • x = x
⊢ False

Tactic:
rw [mem_inter_iff, mem_iInter] at hz hγz

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∧ ∀ (i : ↑Γ₀), z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
hγz : (fun x ↦ γ • x) z ∈ V ∧ ∀ (i : ↑Γ₀), (fun x ↦ γ • x) z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
h : ¬γ • x = x
⊢ False
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
this : (fun a ↦ a.1 * a.2) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V, IsOpen[inst✝²] V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Tactic:
simpa only [prod_subset_iff] using! exists_nhds_square this

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✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
p : ι → Prop
hc : ∀ (i : ι), p i → Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (j : Subtype p), f (↑j) x

Tactic:
exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Tactic:
simpa only [inv_inv] using tendsto_inv_nhdsLE (a := a⁻¹)

Goal state after:
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:
rw [SetLike.ext'_iff] at hs ⊢

Goal state after:
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 = ↑⊤
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ c / x) (𝓝[>] a) = 𝓝[<] (c / a)

Tactic:
convert! (Homeomorph.divLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : IsTopologicalGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
c a : H
⊢ map (fun x ↦ c / x) (𝓝[<] a) = 𝓝[>] (c / a)

Tactic:
convert! (Homeomorph.divLeft c).isEmbedding.map_nhdsWithin_eq .. using 2
  simp

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun x ↦ g * x) ⁻¹' V

Tactic:
by
  obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((x * ·) ⁻¹' V) := by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (by fun_prop) ?_
    rwa [mem_preimage, inv_mul_cancel_right]
  exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Type u_3
l : Filter ι
f : ι → β → α
s : Set β
hf : UniformCauchySeqOn f l s
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (m : ι × ι) in l ×ˢ l, ∀ x ∈ s, (f⁻¹ m.1 x, f⁻¹ m.2 x) ∈ u

Tactic:
by simpa using (uniformContinuous_inv.comp_uniformCauchySeqOn hf u hu)

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ

Tactic:
by rw [div_mul_div_comm]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
⊢ comap mabs (𝓝 1) = 𝓝 1

Tactic:
simp [nhds_eq_iInf_mabs_div]

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

Tactic:
tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩

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
tfae_5_to_4 : (∃ u ∈ Ioi a, Ico a u ⊆ s) → ∃ u ∈ Ioc a b, 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.PartialHomeomorph.Defs

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e' toPartialEquiv✝ : PartialEquiv X Y
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
h :
  { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
        continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv =
    e'
⊢ { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
          continuousOn_invFun := continuousOn_invFun✝ }.replacePartialEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
      continuousOn_invFun := continuousOn_invFun✝ }

Tactic:
subst e'

Goal state after:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialEquiv✝ : PartialEquiv X Y
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
⊢ { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
          continuousOn_invFun := continuousOn_invFun✝ }.replacePartialEquiv
      { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
          continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv✝, continuousOn_toFun := continuousOn_toFun✝,
      continuousOn_invFun := continuousOn_invFun✝ }
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e' : PartialEquiv X Y
toPartialHomeomorph✝ : PartialHomeomorph X Y
open_source✝ : IsOpen[inst✝¹] toPartialHomeomorph✝.source
open_target✝ : IsOpen[inst✝] toPartialHomeomorph✝.target
h :
  { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
        open_target := open_target✝ }.toPartialEquiv =
    e'
⊢ { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
          open_target := open_target✝ }.replacePartialEquiv
      e' h =
    { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝, open_target := open_target✝ }

Tactic:
subst e'

Goal state after:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialHomeomorph✝ : PartialHomeomorph X Y
open_source✝ : IsOpen[inst✝¹] toPartialHomeomorph✝.source
open_target✝ : IsOpen[inst✝] toPartialHomeomorph✝.target
⊢ { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
          open_target := open_target✝ }.replacePartialEquiv
      { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝,
          open_target := open_target✝ }.toPartialEquiv
      ⋯ =
    { toPartialHomeomorph := toPartialHomeomorph✝, open_source := open_source✝, open_target := open_target✝ }
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'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual 0) c = (dual f) 0

Tactic:
dual_zero,

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ 0 c = (dual f) 0
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
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ S.liftCycles a ha = x₁ ≫ S.toCycles
⊢ π ≫ a = x₁ ≫ S.f

Tactic:
by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles

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₂ x₂' : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
hx₂' : x₂' ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ S.f

Tactic:
suffices S.liftCycles x₂ hx₂ ≫ S.homologyπ = S.liftCycles x₂' hx₂' ≫ S.homologyπ ↔
      S.liftCycles (x₂ - x₂') (by simp [hx₂, hx₂']) ≫ S.homologyπ = 0 by
    simp [this, S.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements,
      sub_eq_iff_eq_add']
  rw [← sub_eq_zero, ← sub_comp, sub_liftCycles]

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:
by
  dsimp [μIso, freeMk]
  erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
hγ : γ ≫ homologyMap φ = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0

Tactic:
replace hγ := π₁ ≫= hγ

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact ↔ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
constructor
  · intro h
    constructor
    · exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero i))
        (fun i hi => h.exact i)
    · rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero n
      exact h.exact n (by lia)
  · rintro ⟨h, h'⟩
    refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.toIsComplex.zero i
      · exact h'.toIsComplex.zero 0
    · simp only [Nat.add_le_add_iff_right] at hi
      obtain hi | rfl := hi.lt_or_eq
      · exact h.exact i
      · exact h'.exact 0

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0

Tactic:
rw [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z = x₁ ≫ S₁.f
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 w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType (X₁ ⨯ X₂)
⊢ ((prodEquiv X₁ X₂) x).1 = (hom prod.fst) x

Tactic:
by
  simpa using! congr_hom (prodComparison_fst (forget C) X₁ X₂) x

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

Goal state before:
pp: case none
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y

pp: case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y

Tactic:
· left
    use y
    rfl

Goal state after:
case some
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : ToType ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y) ∨
    ∃ i y_1, (hom (ι f i)) y_1 = (hom (colimit.ι (wideSpan B X f) (some j))) y
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u // J.fst l = r' }
T₂ : Type := { u // J.snd l = r' }
x✝ : T₂
val✝ : Unit
h : J.snd l = r'
⊢ left l ⟶ right r'

Tactic:
subst h; exact Hom.snd l

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ = φ'

Tactic:
by
  ext i
  fin_cases i
  exact h

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : δ₀Functor.map f = δ₀Functor.map g
⊢ f = g

Tactic:
ext ⟨i, hi⟩
  obtain _ | i := i
  · exact h₀
  · exact congr_app h₁ ⟨i, by valid⟩

Goal state after: