mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
by
  rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]

Goal state after:
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
X : ι → Type u_4
inst✝⁴ : Bornology α
inst✝³ : Bornology β
inst✝² : (i : ι) → Bornology (X i)
inst✝¹ : BoundedSpace α
inst✝ : BoundedSpace β
⊢ BoundedSpace (α × β)

Tactic:
by
  simp [← cobounded_eq_bot_iff, cobounded_prod]

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

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

Tactic:
ε_pos

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist x' x.1 = r → (dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ r)

Tactic:
rintro rfl

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist x' x.1
⊢ dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ dist x' x.1
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist y' x.2 = r → (dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ r)

Tactic:
rintro rfl

Goal state after:
case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist y' x.2
⊢ dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ dist y' x.2
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
by
  rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩
  filter_upwards [eventually_closedBall_subset hs] with r hr
  exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), ball x r' = closedBall x r

Tactic:
ext
  simp [forall_gt_iff_le]

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ico a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
    rw [closure_Ioo hab]

Goal state after:
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
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * I' = spanSingleton R⁰ (I'.divMod I J') * J * I'
⊢ I' ≠ 0

Tactic:
rintro rfl

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
v : HeightOneSpectrum R
I J J' : FractionalIdeal R⁰ K
h : J ≤ I
hJ' : J' ≠ 0
hI : I ≠ 0
H : I * J' = 0 * J
h' : J' ≤ 0
this : (J' ⊓ spanSingleton R⁰ (divMod 0 I J') * I) * 0 = spanSingleton R⁰ (divMod 0 I J') * J * 0
⊢ False
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ b✝ : α
hab : a✝ ≤ b✝
⊢ a✝ = b✝ → IsCompact (Icc a✝ b✝)

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖ = 0

Tactic:
rintro rfl

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖ = 0
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : 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
⊢ Icc a b ⊆ s

Tactic:
set A := {t ∈ Icc a b | Icc a t ⊆ s}

Goal state after:
case inr
α : 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}
⊢ Icc a b ⊆ s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖₊ = 0

Tactic:
rintro rfl

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖₊ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ↑‖m.prod‖₊ ≤ ↑(Multiset.map (fun x ↦ ‖x‖₊) m).sum

Tactic:
push_cast

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun x ↦ ‖x‖₊) m)).sum
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ↑‖∏ a ∈ s, f a‖₊ ≤ ↑(∑ a ∈ s, ‖f a‖₊)

Tactic:
push_cast

Goal state after:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ‖∏ a ∈ s, f a‖ ≤ ∑ i ∈ s, ‖f i‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : 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
⊢ Icc a b ⊆ s

Tactic:
by
  rcases lt_or_ge b a with hab | hab
  · simp_all
  set A := {t ∈ Icc a b | Icc a t ⊆ s}
  have a_mem : a ∈ A := ⟨left_mem_Icc.mpr hab, by simp [ha]⟩
  have bdd_A : BddAbove A := ⟨b, fun t ht ↦ ht.1.2⟩
  set t₁ := sSup A
  have t₁_mem : t₁ ∈ Icc a b := ⟨le_csSup bdd_A a_mem, csSup_le ⟨a, a_mem⟩ (fun t ht ↦ ht.1.2)⟩
  obtain ⟨⟨t₁a, t₁b⟩, ht₁⟩ : t₁ ∈ A := by
    refine ⟨t₁_mem, fun t ht ↦ ?_⟩
    rcases ht.2.eq_or_lt with rfl | h
    · have : closure A ⊆ s ∩ Icc a b := by
        apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)
        have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
        exact ht.2 this
      apply this.trans inter_subset_left
      exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A
    · obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
      apply cA.2
      exact ⟨ht.1, tc.le⟩
  suffices t₁ = b by simpa [this] using ht₁
  apply eq_of_le_of_not_lt t₁b fun t₁b' ↦ ?_
  obtain ⟨m, t₁m, H⟩ : ∃ m > t₁, Ioo t₁ m ⊆ s :=
    (mem_nhdsGT_iff_exists_Ioo_subset' t₁b').mp (h t₁ ⟨t₁a, t₁b'⟩ (fun s hs ↦ ht₁ hs))
  obtain ⟨t, hat, ht⟩ : ∃ t, t₁ < t ∧ t < min m b := exists_between (lt_min t₁m t₁b')
  have : t ∈ A := by
    refine ⟨⟨by order, ht.le.trans (min_le_right _ _)⟩, fun t' ht' ↦ ?_⟩
    rcases le_or_gt t' t₁ with h't' | h't'
    · exact ht₁ ⟨ht'.1, h't'⟩
    · exact H ⟨h't', ht'.2.trans_lt <| ht.trans_le <| min_le_left ..⟩
  have : t ≤ t₁ := le_csSup bdd_A this
  order

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

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|

Tactic:
rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ a ∈ s, f a ≠ ∞

Tactic:
exact sum_ne_top.2 hf

Goal state after:
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ (∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal

Tactic:
rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ∑ i ∈ s, ↑(f i).toNNReal = ∑ a ∈ s, (f a).toReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case mp
x : EReal
h : ⊤ + x = ⊤
⊢ x ≠ ⊥

Tactic:
rintro rfl

Goal state after:
case mp
h : ⊤ + ⊥ = ⊤
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a

Tactic:
rcases h with ⟨i, i_s, b, hb⟩
  use b
  refine fun c hc ↦ hb c ?_
  rw [eventually_map] at hc ⊢
  refine hc.mono fun a h ↦ ?_
  simp only [sup'_le_iff] at h ⊢
  exact h i i_s

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x ↦ ⊥) f = ⊥

Tactic:
by
  rw [limsup_eq, eq_bot_iff]
  exact sInf_le (Eventually.of_forall fun _ => le_rfl)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ ⨅ i ∈ f, (⨆ a ∈ i, u a) ⊓ aᶜ = ⨅ s ∈ f, ⨆ a_1 ∈ s, u a_1 ⊓ aᶜ
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ (n + 1))

Tactic:
by
    rw [pow_succ]
    exact (h.pow_end n).mul_end h

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
z : β
x_z : z > x
hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1
⊢ ∀ᶠ (n : α) in f, u n ≤ x

Tactic:
exact (h z x_z).mono <| fun w hw ↦ (or_iff_left (not_le_of_gt hw)).1 (hz (u w))

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * ↑(3 * K) + ε / 2

Tactic:
push_cast

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
⊢ y < limsup u f

Tactic:
obtain ⟨z, y_z, z_x⟩ := h' y y_x

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst✝ : L.HasSupport
⊢ Multipliable f L

Tactic:
classical
  exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable (fun b ↦ (f b)⁻¹) L
⊢ Multipliable f L

Tactic:
simpa only [inv_inv] using hf.inv

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

Goal state before:
pp: case refine_2
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ f = 1 → HasProd f 1 L

Tactic:
rintro rfl

Goal state after:
case refine_2
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ 1 i
⊢ HasProd 1 1 L
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
e : Set α
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e

Tactic:
· obtain ⟨s, hs⟩ := vanish _ he
    exact ⟨s, fun t hts ↦ (t.tprod_subtype f).symm ▸ hs _ hts⟩

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

Goal state before:
pp: case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
⊢ a = 1 → Multipliable fun x ↦ a

Tactic:
rintro rfl

Goal state after:
case refine_2
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
⊢ Multipliable fun x ↦ 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [codisjoint_iff_le_sup]
      rintro (i | j) <;> simp

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

Goal state before:
pp: case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ (u1 ∪ u2) \ (u1 ∩ u2)
⊢ x ≠ 0

Tactic:
rintro rfl

Goal state after:
case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
hx : 0 ∈ (u1 ∪ u2) \ (u1 ∩ u2)
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', ↑a = x) ∧ ∃ a ∈ v', -↑a = x
⊢ f x = if x = 0 then f 0 else 1

Tactic:
suffices x = 0 by simp only [this, if_true]

Goal state after:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', ↑a = x) ∧ ∃ a ∈ v', -↑a = x
⊢ x = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : Ring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : T2Space α
x : α
h : Summable fun x_1 ↦ x ^ x_1
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, (1 - x) * x ^ i) atTop (nhds 1)

Tactic:
simpa [← Finset.mul_sum, mul_neg_geom_sum] using tendsto_const_nhds.sub h.tendsto_atTop_zero

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a ↦ ↑(f a)) (↑r) L ↔ HasSum f r L

Tactic:
simp only [HasSum, ← coe_sum, tendsto_coe]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ 2 * dist x y

Tactic:
dist_ofPreNNDist,

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ 2 * ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum)
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Set E
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Tactic:
simp [Metric.mem_closure_iff, dist_eq_norm_div]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist a ↑y < r + r

Tactic:
edist_comm a y

Goal state after:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(eball a r)
⊢ edist a ↑x + edist a ↑y < r + r

Tactic:
by rw [edist_comm a x, edist_comm a y]; exact ENNReal.add_lt_add x.2 y.2

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x // x ∈ Icc a b }
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ (f ∘ Subtype.val) x = f ↑x

Tactic:
comp_apply

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x // x ∈ Icc a b }
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ f ↑x = f ↑x
Module: Mathlib.Topology.Bornology.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: case refine_1
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ‖x‖ ≤ ‖f x‖

Tactic:
grw [hK.le_mul_norm' (map_one f), ← mul_assoc]
    exact mul_le_of_le_one_left (norm_nonneg' (f x)) (by simp [field])

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (Isometry.toDilation f hf) = 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
· exact ratio_of_trivial hf.toDilation h

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (Isometry.toDilation f hf) = 1
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
comp_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: ⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
by
  rw [← NNReal.isometry_coe.lipschitzWith_iff]
  have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    NNReal.isometry_coe.prodMap NNReal.isometry_coe
  convert!
    (((LipschitzWith.prod_fst.comp this.lipschitz).sub
          (LipschitzWith.prod_snd.comp this.lipschitz)).max_const
      0)
  norm_num

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
F : Type u_3
inst✝³ : PseudoMetricSpace X
inst✝² : PseudoMetricSpace Y
inst✝¹ : EquivLike F X Y
inst✝ : DilationEquivClass F X Y
e : F
⊢ map (⇑e) (cobounded X) = cobounded Y

Tactic:
by
  rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst✝ : DecidableEq ι
hl : (i :: l).Nodup
hj : j ∈ l
v : TProd α (i :: l)
⊢ j ≠ i

Tactic:
rintro rfl

Goal state after:
ι : Type u
α : ι → Type v
j : ι
l : List ι
inst✝ : DecidableEq ι
hj : j ∈ l
hl : (j :: l).Nodup
v : TProd α (j :: l)
⊢ False