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

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
⊢ d ∈ 𝓤 α → ∃ t, t.Finite ∧ d.preimage t ∈ g

Tactic:
hd

Goal state after:
case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
hd : d ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ d.preimage t ∈ g
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
have h_subset : interUnionBalls xs u U
      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
    fun x hx ↦ Set.mem_iInter.1 hx i

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ Filter.comap (Prod.mk x) (𝓤 α)
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
← lift'_comp_uniformity

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ Filter.comap (Prod.mk x) ((𝓤 α).lift' fun s ↦ s ○ s)
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : (i : ι) → Filter (α i)
hl : ∀ (i : ι), Cauchy (l i)
this : ∀ (i : ι), (l i).NeBot
⊢ Cauchy (Filter.pi l)

Tactic:
simpa [cauchy_pi_iff]

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

Goal state before:
pp: case he
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ ∅, (f p x, f q x) ∈ u

pp: case hmono
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u

pp: case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u

pp: case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u

Tactic:
· exact ⟨univ, univ_mem, by simp⟩

Goal state after:
case hmono
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u

case hunion
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u

case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Module: Mathlib.Algebra.Order.Group.MinMax

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

Tactic:
by
  grind

Goal state after:
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:
by
  rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢
  exact equicontinuousWithinAt_iInf_dom hk

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : (𝓤 α).HasBasis p s
⊢ (∀ (i : κ),
      p i → ∀ᶠ (x : X) in 𝓝 x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
⊢ map₂ Prod.mk f g = f ×ˢ g

Tactic:
by
  simp only [← map_prod_eq_map₂, map_id']

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

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

Tactic:
rw [← map_prod_eq_map₂, prod_pure, map_map]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p ↦ m p.1 p.2) ∘ fun a ↦ (a, b)) f = map (fun x ↦ m x b) f
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x ↦ u ∘ x) ∘ F) x₀
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x ↦ u ∘ x) ∘ F) S x₀

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x ↦ u ∘ x) ∘ F) S x₀
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
⊢ RightInverse (fun g ↦ ⟨g.comp f, ⋯⟩) fun g ↦ hf.lift ↑g ⋯

Tactic:
by
    intro g
    ext a
    simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SMul M α
inst✝³ : ContinuousConstSMul M α
inst✝² : TopologicalSpace β
g : β → α
b : β
s : Set β
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
c : M
⊢ Continuous[inst✝⁵, inst✝⁵] fun x ↦ MulOpposite.op c • x

Tactic:
by simpa only [op_smul_eq_smul] using continuous_const_smul c

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p

Tactic:
have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
h' : TendstoUniformly F' f p
⊢ TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p
Module: Mathlib.Topology.Algebra.IsUniformGroup.Constructions

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁴ : Group G✝
inst✝³ : Group H
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → UniformSpace (G i)
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), IsUniformGroup (G i)
⊢ IsUniformGroup ((i : ι) → G i)

Tactic:
rw [Pi.uniformSpace_eq]

Goal state after:
G✝ : Type u_1
H : Type u_2
hom : Type u_3
inst✝⁴ : Group G✝
inst✝³ : Group H
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → UniformSpace (G i)
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), IsUniformGroup (G i)
⊢ IsUniformGroup ((i : ι) → G i)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
simp_rw [← Ultrafilter.clusterPt_iff] at hY ⊢

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
𝒰 : Ultrafilter X
y : Y
hY : ClusterPt y ↑(Ultrafilter.map f 𝒰)
⊢ ∃ x, f x = y ∧ ClusterPt x ↑𝒰
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: ι : 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 : ι), IsProperMap (f i)
⊢ IsProperMap fun x i ↦ f i (x i)

Tactic:
by
  simp_rw [isProperMap_iff_ultrafilter] at h ⊢
  constructor
  -- Continuity is clear.
  · exact continuous_pi fun i ↦ (h i).1.comp (continuous_apply i)
  -- Let `𝒰 : Ultrafilter (Π i, X i)`, and assume that `Π i, f i` tends to some `y : Π i, Y i`
  -- along `𝒰`.
  · intro 𝒰 y hy
  -- That means that each `f i` tends to `y i` along `map (eval i) 𝒰`.
    have : ∀ i, Tendsto (f i) (Ultrafilter.map (eval i) 𝒰) (𝓝 (y i)) := by
      simpa [tendsto_pi_nhds] using! hy
  -- Thus, by properness of all the `f i`s, we can choose some `x : Π i, X i` such that, for all
  -- `i`, `f i (x i) = y i` and `map (eval i) 𝒰` tends to  `x i`.
    choose x hxy hx using fun i ↦ (h i).2 (this i)
  -- By the properties of the product topology, that means that `𝒰` tends to `x`,
  -- which completes the proof since `(Π i, f i) x = y`.
    refine ⟨x, funext hxy, ?_⟩
    rwa [nhds_pi, le_pi]

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

Goal state before:
pp: G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x * b) l (𝓝 (c * b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨?_, Tendsto.mul_const b⟩
  convert! Tendsto.mul_const b⁻¹ using 3 <;> rw [mul_inv_cancel_right]

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

Goal state before:
pp: case empty
α : Type u_3
β : Type u_4
ι : Type u_5
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
inst✝ : UniformSpace β
f : ι → β → α
h : ∀ i ∈ ∅, UniformContinuous (f i)
⊢ UniformContinuous fun x ↦ ∏ i ∈ ∅, f i x

Tactic:
simpa using uniformContinuous_const

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

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g * h ∈ connectedComponent 1

Tactic:
rw [connectedComponent_eq hg]
  have hmul : g ∈ connectedComponent (g * h) := by
    apply Continuous.image_connectedComponent_subset (continuous_const_mul g)
    rw [← connectedComponent_eq hh]
    exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
  simpa [← connectedComponent_eq hmul] using mem_connectedComponent

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
α : Type u_1
l : Filter α
inst✝¹ : l.NeBot
inst✝ : T2Space G
f g : α → G
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
hfg : Tendsto (fun x ↦ f x / g x) l (𝓝 1)
⊢ Tendsto f l (𝓝 b)

Tactic:
by simpa using hfg.mul hg

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}
⊢ ∀ (a : Set (Set α)),
    a.Finite →
      a ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a} →
        ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ a = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
intro k k_fin hk

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}
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : S.X₁.isFinite
h₃ : S.X₃.isFinite
⊢ S.X₂.isFinite

Tactic:
simp only [prop_isFinite_iff] at h₁ h₃ ⊢

Goal state after:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
⊢ Finite ↑S.X₂
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
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (c + c').toAddMonoidHom ⋯) x = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) x

Tactic:
refine x.induction_on ?_ ?_ ?_

Goal state after:
case refine_1
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
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (c + c').toAddMonoidHom ⋯) 0 = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) 0

case refine_2
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
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B),
    (liftAddHom (c + c').toAddMonoidHom ⋯) (x ⊗ₜ[R] y) =
      (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) (x ⊗ₜ[R] y)

case refine_3
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
c c' : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B),
    (liftAddHom (c + c').toAddMonoidHom ⋯) x = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) x →
      (liftAddHom (c + c').toAddMonoidHom ⋯) y = (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) y →
        (liftAddHom (c + c').toAddMonoidHom ⋯) (x + y) =
          (liftAddHom c.toAddMonoidHom ⋯ + liftAddHom c'.toAddMonoidHom ⋯) (x + y)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_2.a
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
ne : (f ⁻¹' Iic z).Nonempty
bdd : BddAbove (f ⁻¹' Iic z)
a : X
ha : a ∈ f ⁻¹' Ioi z
⊢ sSup (f ⁻¹' Iic z) ≤ a

Tactic:
exact csSup_le ne fun b hb ↦ (hf.mono.reflect_lt (hb.trans_lt ha)).le

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

Tactic:
rw [S.exact_iff_epi_toCycles, epi_iff_surjective_up_to_refinements]
  constructor
  · intro hS A a ha
    obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)
    exact ⟨A', π, hπ, x₁, by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles⟩
  · intro hS A a
    obtain ⟨A', π, hπ, x₁, fac⟩ := hS (a ≫ S.iCycles) (by simp)
    exact ⟨A', π, hπ, x₁, by simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]⟩

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
⊢ Mono (homologyMap φ)

Tactic:
Preadditive.mono_iff_cancel_zero

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
⊢ ∀ (P : C) (g : P ⟶ S₁.homology), g ≫ homologyMap φ = 0 → g = 0
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
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0

Tactic:
obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ :=
      h (π₂ ≫ z) (by rw [assoc, hz, comp_zero]) y (by simpa)

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
⊢ S₁.liftCycles z hz ≫ S₁.homologyπ = 0
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✝ : Mono S.L₁.f
⊢ Mono S.L₀.f

Tactic:
have : Mono (S.L₀.f ≫ S.v₀₁.τ₂) := by
    rw [← S.v₀₁.comm₁₂]
    apply mono_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Mono S.L₁.f
this : Mono (S.L₀.f ≫ S.v₀₁.τ₂)
⊢ Mono S.L₀.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₁ × ToType X₂
⊢ (hom prod.fst) ((prodEquiv X₁ X₂).symm x) = x.1

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Goal state after:
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)
y : ToType (X₁ ⨯ X₂)
⊢ (hom prod.fst) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).1
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₁ × ToType X₂
⊢ (hom prod.snd) ((prodEquiv X₁ X₂).symm x) = x.2

Tactic:
obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x

Goal state after:
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)
y : ToType (X₁ ⨯ X₂)
⊢ (hom prod.snd) ((prodEquiv X₁ X₂).symm ((prodEquiv X₁ X₂) y)) = ((prodEquiv X₁ X₂) y).2
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
c : Cofan I.left
d : Cofan I.right
hc : IsColimit c
i : J.L
⊢ c.inj i ≫ I.sndSigmaMapOfIsColimit d hc = I.snd i ≫ d.inj (J.snd i)

Tactic:
simp [sndSigmaMapOfIsColimit]

Goal state after: