mathlib-initiative/mathlib-tactics huggingface dataset:
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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ k

Tactic:
hnd

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
k : K
hk : I = spanSingleton R⁰ k
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hnd : mk' K n d = k
hn0 : n ≠ 0
⊢ spanSingleton R⁰ k = spanSingleton R⁰ k
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Tactic:
cases x <;> norm_num

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

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ x.swap ∈ {x | d x.1 x.2 < r}

Tactic:
rwa [mem_ofPred, symm]

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ ¬Associated v.asIdeal w.asIdeal

Tactic:
associated_iff_eq,

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ ¬v.asIdeal = w.asIdeal
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
J : Ideal R
hJ : J ≠ 0
⊢ count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
    Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero v.associates_irreducible]

Goal state after:
case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x✝ y✝ : α
h : edist x✝ y✝ < ∞
⊢ edist y✝ x✝ < ∞

Tactic:
by rwa [edist_comm]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ ∑ p ∈ s, a p ∈ J

Tactic:
exact sum_mem fun p hp ↦ Ideal.mul_le_left (ha p hp)

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ici a ∩ Iic b) = Ioo a b

Tactic:
interior_inter,

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ici a) ∩ interior (Iic b) = Ioo a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ici a ∩ Iio b) = Ioo a b

Tactic:
interior_inter,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ici a) ∩ interior (Iio b) = Ioo a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ioi a ∩ Iic b) = Ioo a b

Tactic:
interior_inter,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ioi a) ∩ interior (Iic b) = Ioo a b
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
⊢ f x ≤ f b

Tactic:
rcases hxb.eq_or_lt with rfl | hxb

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
hb : x ∈ s
hxb : x ≤ x
⊢ f x ≤ f x

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb✝ : x ≤ b
hxb : x < b
⊢ f x ≤ f b
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
⊢ Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x d) (y (f (x d))))

Tactic:
simp only [disjoint_iff_forall_ne, mem_Ioo, ne_eq, and_imp]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
⊢ ∀ ⦃a : α⦄, x c < a → a < y (f (x c)) → ∀ ⦃b : α⦄, x d < b → b < y (f (x d)) → ¬a = b
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ dist a b = ‖b⁻¹ * a‖

Tactic:
by
  rw [dist_comm, dist_eq_norm_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖

Tactic:
rw [add_comm]
  refine (norm_mul_le' _ _).trans_eq' ?_
  rw [div_mul_cancel]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Tactic:
simpa using norm_mul_le' (u / v) (v / w)

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

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i
y : (i : ι) → X i
hy : ∀ (i : ι), y i ∈ s i
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c

Tactic:
exact fun b => ediam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
⊢ ∏ i, (↑i).maxPowDividing (map (algebraMap S R) p) = ∏ i, ↑i ^ (↑i).ramificationIdx S

Tactic:
let _ : Fintype {v : HeightOneSpectrum R // v.asIdeal ∣ map (algebraMap S R) p} := hF

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
S : Type u_3
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S R
inst✝³ : Algebra.IsIntegral S R
inst✝² : IsDomain S
inst✝¹ : Module.IsTorsionFree S R
p : Ideal S
inst✝ : p.IsMaximal
hp : p ≠ 0
h : map (algebraMap S R) p ≠ 0
hF : Fintype ↑{v | v.asIdeal ∣ map (algebraMap S R) p} := ⋯.fintype
x✝ : Fintype { v // v.asIdeal ∣ map (algebraMap S R) p } := hF
⊢ ∏ i, (↑i).maxPowDividing (map (algebraMap S R) p) = ∏ i, ↑i ^ (↑i).ramificationIdx S
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)

Tactic:
Ideal.sup_eq_prod_inf_factors hI hJ,

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal (normalizedFactors I ∩ normalizedFactors J).prod =
    min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
ε : G
ε1 : ε > 1
hε : ∀ g ∈ S, g ∉ Ioo 1 ε
⊢ ∃ a, S = closure {a}

Tactic:
exact cyclic_of_isolated_one ε1 (disjoint_left.2 hε)

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
⊢ (⨆ i, f a i) + ⨆ i, ∑ a ∈ s, f a i = ⨆ i, f a i + ∑ a ∈ s, f a i

Tactic:
refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Goal state after:
case cons
ι : Type u_1
α : Type u_2
f : α → ι → ℝ≥0∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : ∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)
  · simp [h]
  · obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
    exact tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

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

Goal state before:
pp: case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)

Tactic:
rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)
    · exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
    · rwa [tendsto_nhds_unique h (hl'.comp hg)]

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

Goal state before:
pp: α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod

Tactic:
simp only [List.map_cons, List.prod_cons]

Goal state after:
α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)

Tactic:
exact (h i).mul_end (LipschitzWith.list_prod f K h l)

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
· exact tendsto_of_liminf_eq_limsup (le_antisymm (le_trans (liminf_le_limsup h h') hsup) hinf)
      (le_antisymm hsup (le_trans hinf (liminf_le_limsup h h'))) h h'

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

Goal state before:
pp: x : EReal
h : x < 0
⊢ ⊤ * x = ⊥

Tactic:
rw [EReal.mul_comm]
  exact mul_top_of_neg h

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

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

Tactic:
simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]

Goal state after:
a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
this : ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x} ∈ L.filter
⊢ s ∈ L.filter

Tactic:
exact Filter.mem_of_superset this fun r hr ↦ ht r (by simpa using! hr)

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

Goal state before:

Tactic:
rs n
    _ = rs (⟨n, by simp [hn]⟩ : {n | b'' < u n r}) := rfl
    _ ≤ ⨆ n : {n | b'' < u n r}, rs n := by
      refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using! hb''
      exact Finite.bddAbove_range _
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_right
    _ ≤ v := hv

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

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
⊢ (L.map f).support = ⇑f '' L.support

Tactic:
by
  ext c
  rcases em (c ∈ range f) with ⟨b, rfl⟩ | hc
  · simp [support]
  · exact ⟨fun hc' ↦ have := hc'.exists; by grind, by grind⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : Fintype β
f : β → α
L : SummationFilter β
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd f (∏ b ∈ L.support.toFinset, f b) L

Tactic:
by
  apply tendsto_nhds_of_eventually_eq
  have h1 : ⋂ b ∈ L.support, {s | b ∈ s} ∈ L.filter :=
    (L.filter.biInter_mem L.support.toFinite).mpr (by tauto)
  have h2 : ⋂ b ∈ L.supportᶜ, {s | b ∉ s} ∈ L.filter :=
    (L.filter.biInter_mem L.supportᶜ.toFinite).mpr
      (fun b hb ↦ (L.eventually_mem_or_not_mem b).resolve_left hb)
  filter_upwards [h1, h2] with s hs hs'
  congr 1
  simp only [Set.mem_iInter, Set.mem_ofPred_eq, Set.mem_compl_iff] at hs hs'
  grind

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 β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
rw [tprod_def, dif_pos ha]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f
    (if L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite then finprod (L.support.mulIndicator fun b ↦ f b)
    else if HasProd (fun b ↦ f b) 1 L then 1 else Exists.choose ha)
    L
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 γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ g 1 = ∏'[L] (i : β), g (f i)

Tactic:
simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = ∏ i ∈ {i}, f i

Tactic:
prod_singleton

Goal state after:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = f i
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : ¬Multipliable fun a ↦ f ↑a
⊢ ∏' (b : ↑t), f ↑b ∈ o

Tactic:
· exact tprod_eq_one_of_not_multipliable ht ▸ mem_of_mem_nhds ho

Goal state after:
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 : Finset β
hs : ∀ (t : Set β), (∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s) → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e

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

Goal state after:
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 ((t i).mulIndicator f) (a i)
⊢ HasProd ((⋃ i ∈ s, t i).mulIndicator f) (∏ i ∈ s, a i)

Tactic:
Finset.mulIndicator_biUnion _ _ hs

Goal state after:
α : 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 ((t i).mulIndicator f) (a i)
⊢ HasProd (fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a) (∏ i ∈ s, a i)
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
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
by_cases hf : Multipliable f
  · have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]
    have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds
    simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat
  · refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm
    rwa [multipliable_nat_add_iff n]

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

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

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · by_contra ha
    have : {a}ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
    have : Finite β := by
      simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
    exact not_finite β
  · rintro rfl
    exact multipliable_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏ b ∈ {b}, f b = f b

pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
prod_singleton

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ f b = f b

α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s, f x

Tactic:
rw [← prod_attach]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↥s), f ↑x = ∏ x ∈ s.attach, f ↑x
Module: Mathlib.Topology.Sequences

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst✝] s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s

Tactic:
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩

Goal state after: