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

Goal state before:
pp: case empty
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ ∅, I i ≠ 0
⊢ count K v (∏ i ∈ ∅, I i) = ∑ i ∈ ∅, count K v (I i)

Tactic:
Finset.prod_empty,

Goal state after:
case empty
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ ∅, I i ≠ 0
⊢ count K v 1 = ∑ i ∈ ∅, count K v (I i)
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0

Tactic:
toENNReal,

Goal state after:
x : EReal
hx : x ≤ 0
⊢ (if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (↑x).toENNReal = x

Tactic:
toENNReal,

Goal state after:
case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (if ↑x = ⊤ then ∞ else ENNReal.ofReal (↑x).toReal) = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : a ≠ ∞ ∨ b ≠ 0
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
cases b

Goal state after:
case top
a : ℝ≥0∞
ha : a ≠ 0 ∨ ∞ ≠ ∞
hb : a ≠ ∞ ∨ ∞ ≠ 0
⊢ (a * ∞)⁻¹ = a⁻¹ * ∞⁻¹

case coe
a : ℝ≥0∞
x✝ : ℝ≥0
ha : a ≠ 0 ∨ ↑x✝ ≠ ∞
hb : a ≠ ∞ ∨ ↑x✝ ≠ 0
⊢ (a * ↑x✝)⁻¹ = a⁻¹ * (↑x✝)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹

Tactic:
cases b

Goal state after:
case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]

Goal state after:
case coe.inr
a x✝ : ℝ≥0
h : a < x✝
ha : a ≠ 0
⊢ x✝⁻¹ < a⁻¹
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case inl
γ : Type w
inst✝ : MetricSpace γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ (closedBall x r).Subsingleton

Tactic:
rw [closedBall_eq_empty.2 hr]
    exact subsingleton_empty

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

Goal state before:
pp: α : Type u_3
inst✝ : PseudoMetricSpace α
r : ℝ
hpos : 0 < r
hr : Pairwise fun x1 x2 ↦ r ≤ dist x1 x2
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = ⊥

Tactic:
by rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ frontier (Ioc a b) = {a, b}

Tactic:
by
  rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_sdiff_Ioo_same h.le]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
x : E
f : Filter E
⊢ Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖

Tactic:
by
  simp [NormedGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_ofPred, eventually_iff]

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ NoncompactSpace α

Tactic:
by
  rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Rat

Goal state before:
pp: r₁ r₂ : ℚ
⊢ |(-(↑r₁ - ↑r₂))| = |-↑r₁ + ↑r₂|

Tactic:
neg_sub

Goal state after:
r₁ r₂ : ℚ
⊢ |↑r₂ - ↑r₁| = |-↑r₁ + ↑r₂|
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a✝ : α
s✝ : Finset α
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (∀ i ∈ s✝, f i < g i) → ∑ i ∈ s✝, f i < ∑ i ∈ s✝, g i
Hlt : f a✝ < g a✝ ∧ ∀ x ∈ s✝, f x < g x
⊢ f a✝ + ∑ i ∈ s✝, f i < g a✝ + ∑ i ∈ s✝, g i

Tactic:
exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x + y).toReal = x.toReal + y.toReal

Tactic:
lift x to ℝ using ⟨hx, h'x⟩

Goal state after:
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x + y).toReal = (↑x).toReal + y.toReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ min (emultiplicity p.asIdeal (I none)) (emultiplicity p.asIdeal (⨆ b, I (some b))) =
    ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
ih,

Goal state after:
case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ min (emultiplicity p.asIdeal (I none)) (⨅ i, emultiplicity p.asIdeal (I (some i))) =
    ⨅ i, emultiplicity p.asIdeal (I i)
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
⊢ multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)

Tactic:
have H i : FiniteMultiplicity p.asIdeal (I i) :=
    FiniteMultiplicity.of_prime_left (prime p) <| hI i

Goal state after:
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
⊢ multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x - y).toReal = x.toReal - y.toReal

Tactic:
lift x to ℝ using ⟨hx, h'x⟩

Goal state after:
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ (↑x - y).toReal = (↑x).toReal - y.toReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
by
  induction x <;> induction y <;> try {· simp_all [zero_tsub, ENNReal.sub_top]}
  rename_i x y
  by_cases hxy : x ≤ y
  · rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]
    exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm
  · rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe,
      ofReal_sub x (EReal.coe_nonneg.mp hy)]
    simp

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b + a - ↑b = a

Tactic:
rw [add_comm, EReal.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
inf_iSup₂_eq,

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz f^[n + 1]

Tactic:
rw [iterate_add, iterate_one]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ f.limsSup ≤ a

Tactic:
exact limsSup_le_of_le hf h

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

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
filter_upwards [h_lt] with n hn using hn.le

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
b : EReal
h : ⊥ ≠ 0 ∧ b ≠ 0
⊢ ⊥ * b ≠ 0

Tactic:
cases b

Goal state after:
case bot.bot
h : ⊥ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊥ * ⊥ ≠ 0

case bot.coe
a✝ : ℝ
h : ⊥ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊥ * ↑a✝ ≠ 0

case bot.top
h : ⊥ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊥ * ⊤ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
b : EReal
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ b ≠ 0
⊢ ↑a✝ * b ≠ 0

Tactic:
cases b

Goal state after:
case coe.bot
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊥ ≠ 0
⊢ ↑a✝ * ⊥ ≠ 0

case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ↑a✝¹ * ↑a✝ ≠ 0

case coe.top
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
⊢ ↑a✝ * ⊤ ≠ 0
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
b : EReal
h : ⊤ ≠ 0 ∧ b ≠ 0
⊢ ⊤ * b ≠ 0

Tactic:
cases b

Goal state after:
case top.bot
h : ⊤ ≠ 0 ∧ ⊥ ≠ 0
⊢ ⊤ * ⊥ ≠ 0

case top.coe
a✝ : ℝ
h : ⊤ ≠ 0 ∧ ↑a✝ ≠ 0
⊢ ⊤ * ↑a✝ ≠ 0

case top.top
h : ⊤ ≠ 0 ∧ ⊤ ≠ 0
⊢ ⊤ * ⊤ ≠ 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∉ m
⊢ liminfReparam f s p j ∈ m

Tactic:
simp only [m, liminfReparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

Tactic:
by_cases hf : (mulSupport f).Finite

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : (mulSupport f).Finite
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b

case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ (if L.HasSupport ∧ (mulSupport fun b ↦ f b).Finite then ∏ᶠ (b : β), f b
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ⋯) =
    ∏ᶠ (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ 1 = ∏ᶠ (b : β), f b

Tactic:
finprod_of_infinite_mulSupport

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ 1 = 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
this : L.LeAtTop
hf : ¬(mulSupport f).Finite
⊢ (mulSupport f).Infinite
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg_coe
a b c : ℝ≥0∞
hc : 0 < c
⊢ (↑a + ↑b) * -↑c = ↑a * -↑c + ↑b * -↑c

Tactic:
| neg_coe c hc =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H : ¬∃ j, s ↑j = ∅
H' : ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
A : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = ∅
⊢ liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ n • x + x = ↑(n + 1) * x

Tactic:
ih,

Goal state after:
case succ
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ ↑n * x + x = ↑(n + 1) * x
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousMul M
f : ℕ → M
hf : Multipliable fun n ↦ f (n + 1)
⊢ ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)

Tactic:
by
  simpa only [prod_range_one] using hf.prod_mul_tprod_nat_mul'.symm

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

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ ∏' (i : ℕ), f i = (∏ j ∈ range i, f j) * ∏' (k : ℕ), f (k + i)

Tactic:
hf.prod_mul_tprod_nat_add i

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ ∏' (i : ℕ), f i = ∏' (i : ℕ), f i
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)
⊢ HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)

Tactic:
by
  simp_rw [hasProd_subtype_iff_mulIndicator] at *
  rw [Finset.mulIndicator_biUnion _ _ hs]
  exact hasProd_prod hf

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
x : ℤ
hx : x ∈ u
⊢ x ∈ image Nat.cast v' ∪ image Int.negSucc v'

Tactic:
simp only [mem_union, mem_image]
    cases x
    · exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩
    · exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩

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
⊢ ∏' (c : γ), f (g c) = ∏' (b : β), f b

Tactic:
by
  classical
  have : mulSupport f = g '' mulSupport (f ∘ g) := by
    rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
  rw [← Function.comp_def]
  by_cases hf_fin : (mulSupport f).Finite
  · have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
    lift g to γ ↪ β using hg
    simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge,
      comp_apply, ← Finset.prod_map]
    refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
    simp [this]
  · have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

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

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
conv =>

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑' (b : ↑↑(antidiagonal x✝)), f (↑b).1 * g (↑b).2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A
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
x y z : X
lxy lyz : List X
⊢ (zipWith d (x :: (lxy ++ y :: lyz)) (lxy ++ y :: lyz ++ [z])).sum =
    (zipWith d (x :: (lxy ++ y :: lyz)) (lxy ++ [y] ++ (lyz ++ [z]))).sum

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
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length

Tactic:
← @singleton_append _ y,

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
x y z : X
lxy lyz : List X
⊢ (zipWith d (x :: (lxy ++ ([y] ++ lyz))) (lxy ++ ([y] ++ lyz) ++ [z])).sum =
    (zipWith d (x :: (lxy ++ ([y] ++ lyz))) (lxy ++ [y] ++ (lyz ++ [z]))).sum

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
x y z : X
lxy lyz : List X
⊢ (x :: lxy).length = (lxy ++ [y]).length
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y

Tactic:
by
  simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_inj]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y

Tactic:
rw [← h, hg _, hg _]

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.sphere x r = Metric.sphere (h x) r

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

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₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
⊢ ¬L.length ≤ m

Tactic:
intro hLm

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₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : m ∈ s
hLm : L.length ≤ m
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
b : β
t : Set γ
f : β × γ → α
⊢ ∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)

Tactic:
rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]

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

Goal state before:
pp: case refine_1
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

pp: case refine_2
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε

Tactic:
· filter_upwards [h ε hε] with n hn
    refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
    rw [tsub_le_iff_right] at hn ⊢
    rwa [add_comm]

Goal state after:
case refine_2
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case mk
α : Type u_1
inst✝ : LinearOrder α
b val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
apply projIic_of_mem

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
a : X
⊢ 1 • ↑a = ↑a

Tactic:
by rw [← coe_smul, one_smul]

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
liminf_le : liminf u f ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (liminf u f).toReal = b.truncateToReal (liminf u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b

Tactic:
simpa only [eventually_map] using le_b

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b

Tactic:
simpa only [eventually_map] using le_b

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

Goal state before:
pp: case refine_2
α : Type u
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x ↦ f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i ↦ g i x) x i

Tactic:
exact (hg i).2 hx

Goal state after: