mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
⊢ count K v J ≤ count K v I

Tactic:
have := mul_le_mul_right h J⁻¹

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : J⁻¹ * I ≤ J⁻¹ * J
⊢ count K v J ≤ count K v I
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_notMem : ¬v ∈ {v | v.asIdeal ∣ J} ∪ {v | v.asIdeal ∣ Ideal.span {a}}
⊢ False

Tactic:
rw [mem_union, mem_ofPred_eq, mem_ofPred_eq] at h_notMem

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_notMem : ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
hg : ∃ j, g j ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ∞ }
this : Nonempty κ
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Tactic:
replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ∞ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ∞
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y ε₂

Tactic:
rw [← add_sub_cancel ε₁ ε₂]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε}

Tactic:
exact fun _ => ENNReal.coe_lt_coe.1

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rw [totallyBounded_iff_subset] at hs

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝ : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
⊢ comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 (SeparationQuotient X)) =
    comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε})

Tactic:
by
        simp [comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Iio a) = {a}

Tactic:
simp [frontier, closure_Iio' ha]

Goal state after:
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated

Tactic:
nhds_discrete

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f ≤ nhds x

Tactic:
by
    /- We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
      ball (therefore compact by properness) where it is nontrivial. -/
    obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one
    rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩
    have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
    rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf
        (le_principal_iff.2 this) with
      ⟨y, -, hy⟩
    exact ⟨y, hy⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ dist (sSup (S n)) 0 < ε

Tactic:
rw [Real.dist_0_eq_abs, abs_of_nonneg (S0 n)]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
ub : ∀ (m n N : ℕ), N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N)
S0m : ∀ (n : ℕ), 0 ∈ S n
S0 : ∀ (n : ℕ), 0 ≤ sSup (S n)
ε : ℝ
ε0 : ε > 0
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, dist (s m) (s n) < ε / 2
n : ℕ
hn : n ≥ N
⊢ sSup (S n) < ε
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst✝³] A ⊆ s ∩ Icc a b
⊢ t₁ ∈ s

Tactic:
apply this.trans inter_subset_left

Goal state after:
case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := ⋯
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := ⋯
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst✝³] A ⊆ s ∩ Icc a b
⊢ t₁ ∈ closure[inst✝³] A
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inl.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

pp: case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

pp: case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
· exact A a h'a b h'b

Goal state after:
case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝³ : FunLike 𝓕 E F
inst✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = ‖f (x⁻¹ * y)‖

Tactic:
simp only [map_mul, map_inv, ← dist_eq_norm_inv_mul]

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝³ : FunLike 𝓕 E F
inst✝² : Group E
inst✝¹ : SeminormedGroup F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x y : E
⊢ dist x y = dist (f x) (f y)
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)

Tactic:
simp_rw [← continuousWithinAt_univ] at hf

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: case hb
α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s + edist x y = ∞ → ediam (s ∪ t) = ∞

Tactic:
simp only [ENNReal.add_eq_top, edist_ne_top, or_false]

Goal state after:
case hb
α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s = ∞ → ediam (s ∪ t) = ∞
Module: Mathlib.Topology.UniformSpace.Real

Goal state before:
pp: ⊢ ∀ (u : ℕ → ℝ), CauchySeq u → ∃ a, Tendsto u atTop (nhds a)

Tactic:
intro u hu

Goal state after:
u : ℕ → ℝ
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (nhds a)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).toENNReal = x.toENNReal + y.toENNReal

Tactic:
induction x <;> induction y <;> try {· simp_all}

Goal state after:
case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ + ↑a✝).toENNReal = (↑a✝¹).toENNReal + (↑a✝).toENNReal
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

Tactic:
refine sInf_le_sInf fun x hx => ?_

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I ↦ sSup (a '' I)) '' F.sets
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)

Tactic:
refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ i ∈ f, g (⨆ b, ⨆ (_ : p b ∧ b ∈ i), u b) ≤ ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), g (u b)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ ⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Tactic:
iInf₂_sup_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ ⨆ i ∈ f, ⨅ i_1 ∈ i, u i_1 ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
by
  induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Tactic:
exact extend_apply' _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
comp_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ Tendsto (fun s ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), (⇑g ∘ f) b) L
⊢ HasProd f a L

Tactic:
comp_apply,

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), g (f b)) L
⊢ HasProd f a L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), (⇑g ∘ f) b) L
⊢ HasProd f a L

Tactic:
simp_rw [comp_apply, ← ha] at this

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (g a) L
⊢ HasProd f a L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun s ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun s ↦ (∏ x ∈ s, f x) * ∏ x ∈ s, g x) L.filter (𝓝 (a * b))

Tactic:
exact hf.mul hg

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

Tactic:
by
    rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]
    exact prod_ne_zero_iff.mpr hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
⊢ ∏' (c : γ), f (g c) = ∏' (b : β), f b

Tactic:
← Function.comp_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
⊢ tprod (f ∘ g) = ∏' (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L

Tactic:
by
  simp_rw [HasProd, Finset.prod_inv_distrib]
  exact Tendsto.inv₀ h ha

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ ∏ b ∈ hfg_fin.toFinset, (f ∘ ⇑g) b = ∏ b ∈ hf_fin.toFinset, f b

Tactic:
comp_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ ∏ x ∈ hfg_fin.toFinset, f (g x) = ∏ b ∈ hf_fin.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n ↦ f ↑n) ∧ Multipliable fun n ↦ f (-↑n)

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩ <;>
  apply p.comp_injective

Goal state after:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n ↦ -↑n
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
α : Type u_4
inst✝¹ : MetricSpace α
K : ℝ≥0
f : α → β
inst✝ : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
⊢ ProperSpace β

Tactic:
refine ⟨fun x₀ r => ?_⟩
  let K := f ⁻¹' closedBall x₀ r
  have A : IsClosed K := isClosed_closedBall.preimage f_cont
  have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall
  have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
  convert! this.image f_cont
  exact (hf.image_preimage _).symm

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.ball x r = Metric.ball (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst✝¹] (⋃ i, closure[inst✝¹] {x i})

Tactic:
refine IsSeqClosed.isClosed fun y l hy hy' => ?_
  by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}
  · obtain ⟨m, pm⟩ := hm
    exact subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')
  · have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by
      refine frequently_atTop.2 fun a => ?_
      have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
      simp only [mem_Iic, eventually_atTop] at this
      obtain ⟨c, hc⟩ := this
      obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
      refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
      by_contra! hab
      simp_all [hc (c + j) (c.le_add_right j) b hab.le]
    obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this
    choose ψ hψ1 hψ2 using hφ.2
    have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id
    refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim
    exact specializes_iff_mem_closure.2 (hψ2 n)

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

Goal state before:
pp: α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = (f ∘ g) a

Tactic:
comp_apply,

Goal state after:
α : Type uα
inst✝⁴ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝³ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ pkg'.extend f (pkg.map pkg' g (pkg.coe a)) = (f ∘ g) a
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Tactic:
comp_apply,

Goal state after:
α : Type uα
inst✝ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg.compare pkg' (pkg'.compare pkg (pkg'.coe a)) = id (pkg'.coe a)