mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) x ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) x, x_in⟩ ∈
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
mem_ker,

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
T : Type u₃
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
inst✝ : Flat S T
x : T ⊗[S] P.toExtension.Cotangent
x_in✝ :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) x ∈
    (Q.comp P).toExtension.cotangentComplex.ker
x_in :
  (Q.comp P).toExtension.cotangentComplex ((liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) x) =
    0
⊢ ⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) x, x_in✝⟩ ∈
    (liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s✝ : Finset S
hs : Submodule.span R ↑s✝ = ⊤
x s : S
hsq : s ∈ q.primeCompl
r : R
hr : r ∉ p
t : S
e' : (algebraMap R S) r = s * t
⊢ (algebraMap R (Localization.AtPrime p)) ↑⟨r, hr⟩ • IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hsq⟩ ∈
    Submodule.span (Localization.AtPrime p) (Set.range ⇑(algebraMap S (Localization.AtPrime q)))

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
hq : p.primesOver S = {q}
inst✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s✝ : Finset S
hs : Submodule.span R ↑s✝ = ⊤
x s : S
hsq : s ∈ q.primeCompl
r : R
hr : r ∉ p
t : S
e' : (algebraMap R S) r = s * t
⊢ (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) ((algebraMap R (Localization.AtPrime p)) ↑⟨r, hr⟩) *
      IsLocalization.mk' (Localization.AtPrime q) x ⟨s, hsq⟩ ∈
    Submodule.span (Localization.AtPrime p) (Set.range ⇑(algebraMap S (Localization.AtPrime q)))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map (algebraMap R Sq') p = map (↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)) (map (algebraMap R Sq) p)

Tactic:
rw [IsScalarTower.algebraMap_eq R Sq Sq', Ideal.map_map,
          ← AlgEquiv.toAlgHom_toRingHom, AlgEquiv.toAlgHom_ofBijective, Algebra.toRingHom_ofId]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
rw [sInf_def, ← isLUB_neg', neg_neg]

Goal state after:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ nnabs x = x.toNNReal

Tactic:
ext
  rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (⇑ofDual ⁻¹' s).ordConnectedSection = ⇑ofDual ⁻¹' s.ordConnectedSection

Tactic:
by
  simp only [ordConnectedSection]
  simp +unfoldPartialApp only [ordConnectedProj]
  ext x
  simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
    ofDual_toDual]
  tauto

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

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
· rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
    exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Tactic:
· simpa using ENNReal.pow_pos ha.bot_lt _

Goal state after:
case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))

Tactic:
lift x to ℝ≥0 using h'x
  lift y to ℝ≥0 using h'y
  have A : y ≠ 0 := by simpa only [Ne, coe_eq_zero] using (zero_lt_one.trans hy).ne'
  obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) := by
    refine NNReal.exists_mem_Ioc_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx
  refine ⟨n, ?_, ?_⟩
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
  · rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]

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

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = x ^ (-n)

Tactic:
ENNReal.zpow_neg,

Goal state after:
x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Tactic:
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁

Tactic:
exact dist_lt_add_of_nonempty_closedBall_inter_ball h

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x y z : X
⊢ dist x z ≤ dist x y + dist y z

Tactic:
simpa [h, dist_nonneg, add_nonneg, ← ENNReal.ofReal_add] using edist_triangle x y z

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
⊢ SeparableSpace α

Tactic:
have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε := by
    simpa only [univ_subset_iff] using hs

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
this : ∀ ε > 0, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ SeparableSpace α
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩

Goal state after:
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : t.Countable
hsub : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Tactic:
by
  have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
    eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
  simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists

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

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
by
  simp [enorm, nnnorm_of_nonneg hr, ENNReal.ofReal, toNNReal, hr]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
f : ι → F
hf : Surjective f
g : F → E
⊢ ‖g ∘ f‖ = ‖g‖

Tactic:
by
  obtain (h | h) := isEmpty_or_nonempty F
  · have : IsEmpty ι := f.isEmpty
    simp [Subsingleton.elim g 1]
  apply le_antisymm (pi_norm_comp_le' g f)
  obtain ⟨⟨x, h⟩, -⟩ := IsGreatest.pi_norm' g
  obtain ⟨y, rfl⟩ := hf x
  exact h ▸ norm_le_pi_norm' (g ∘ f) y

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
I J : FractionalIdeal R⁰ K
⊢ I.divMod 0 J = 0

Tactic:
simp [divMod]

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
I J : FractionalIdeal R⁰ K
⊢ I.divMod J 0 = 0

Tactic:
simp [divMod]

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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < m

Tactic:
obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm
    filter_upwards [Ioo_mem_nhdsGT xz] with w hw
    exact (Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm

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

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
⊢ False

Tactic:
rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
      (Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with ⟨x, hx⟩

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
x : ↑s
hx : s ∩ Iic ↑x = ∅
⊢ False
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:
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
y : E
ε : ℝ
a : E
⊢ a ∈ ball y ε ↔ a ∈ {x | ‖x⁻¹ * y‖ < ε}

Tactic:
by simp [dist_eq_norm_inv_mul]

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

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
← not_ordConnected_inter_Icc_iff hx hy

Goal state after:
case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ¬(s ∩ Icc x y).OrdConnected
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False

Tactic:
exact (nonempty_of_mem (hb.and hb')).ne_empty this

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

Goal state before:
pp: β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop f
⊢ BddAbove (range f)

Tactic:
← Nat.cofinite_eq_atTop

Goal state after:
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩
  rintro ⟨c, hc⟩; rw [eventually_map] at hc
  obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
  exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_ge hx⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ SupConvergenceClass (α × β)

Tactic:
constructor
  rintro ⟨a, b⟩ s h
  rw [isLUB_prod, ← range_domRestrict, ← range_domRestrict] at h
  have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) :=
    tendsto_atTop_isLUB (monotone_fst.domRestrict s) h.1
  have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) :=
    tendsto_atTop_isLUB (monotone_snd.domRestrict s) h.2
  exact A.prodMk_nhds B

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

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

Tactic:
iterate_one

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
⊢ L.NeBot ∨ L.filter = ⊥

Tactic:
by
  by_cases h : L.filter = ⊥
  · exact .inr h
  · exact .inl ⟨⟨h⟩⟩

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 : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∏ b ∈ t, f b = ∏ b ∈ (↑s ∩ L.support).toFinset, f b

Tactic:
apply Finset.prod_congr_of_eq_on_inter

Goal state after:
case h₁
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∉ (↑s ∩ L.support).toFinset → f a = 1

case h₂
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ (↑s ∩ L.support).toFinset, a ∉ t → f a = 1

case h
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∈ L.support, b ∉ s → f b = 1
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
h1 : ⋂ b ∈ ↑s ∩ L.support, {s | b ∈ s} ∈ L.filter
t : Finset β
ht' : ↑t ⊆ L.support
ht : ∀ i ∈ ↑s ∩ L.support, t ∈ {s | i ∈ s}
⊢ ∀ a ∈ t, a ∈ (↑s ∩ L.support).toFinset → f a = f a
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 : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
this : (⇑g ∘ fun s ↦ ∏ b ∈ s, f b) = fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b
⊢ HasProd (⇑g ∘ f) (g a) L

Tactic:
unfold HasProd

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a L
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous[inst✝⁴, inst✝²] ⇑g
this : (⇑g ∘ fun s ↦ ∏ b ∈ s, f b) = fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (fun s ↦ ∏ b ∈ s, (⇑g ∘ f) b) L.filter (𝓝 (g a))
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 ↦ ∏ x ∈ s, g (f x)) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)

Tactic:
← _root_.map_prod

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 ↦ g (∏ x ∈ s, f x)) L.filter (𝓝 (g a)) ↔ Tendsto (fun s ↦ ∏ x ∈ s, f x) L.filter (𝓝 a)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
⊢ HasProd f m ↔ Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f m
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 ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))

Tactic:
prod_mul_distrib

Goal state after:
α : 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))
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : L.NeBot
⊢ ∏'[L] (i : ι), f i ≤ 1

Tactic:
exact hf.hasProd.le_one h

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, ∀ (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_1
β : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
inst✝¹ : Infinite β
inst✝ : T2Space G
a : G
h : Multipliable fun x ↦ a
⊢ a = 1

Tactic:
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 β

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
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f atTop (𝓝 1)

Tactic:
← Nat.cofinite_eq_atTop

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)
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:
← mul_div_assoc,

Goal state after:
α : 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