mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i ↦ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' (k : ℕ), f (k + i)
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds

Goal state after:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i ↦ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x ↦ ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : ↑(↑s)ᶜ), f ↑x

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| ∏ b ∈ x✝, (fun x ↦ 1 + f x) b

Tactic:
prod_one_add_ordered

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx : Tendsto (fun s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
x✝ : Finset ι
| 1 + ∑ i ∈ x✝, f i * ∏ j ∈ x✝ with j < i, (1 + f j)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto (Real.toNNReal ∘ f) l atTop

Tactic:
Function.comp_def

Goal state after:
α : Type u_2
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto (fun x ↦ (f x).toNNReal) l atTop
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_s
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
s i : ι
hi : i ∈ Iic s
⊢ {j ∈ Iic s | j < i} = Iio i

Tactic:
grind

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

Goal state before:
pp: case succ.none
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ none ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr none

Tactic:
rfl

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

Goal state before:
pp: case succ.some
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
val✝ : NNReal
⊢ some val✝ ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr (some val✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
⊢ Bornology.IsBounded s

Tactic:
Set.image2_singleton_right

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith K₁ fun a ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded ((fun a ↦ f a b) '' s)
⊢ Bornology.IsBounded s
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
e : α ≃ᵢ β
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
by
  simp only [completeSpace_iff_isComplete_univ, ← e.range_eq_univ, ← image_univ,
    isComplete_image_iff e.isometry.isUniformInducing]

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

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

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ n ≤ n

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : T3Space α
f : β → γ → α
h : Multipliable (uncurry f)
h₁ : ∀ (b : β), Multipliable (f b)
h₂ : ∀ (c : γ), Multipliable fun b ↦ f b c
⊢ ∏' (p : γ × β), uncurry (fun b c ↦ f c b) p = ∏' (c : γ × β), uncurry f ((Equiv.prodComm γ β) c)

Tactic:
rfl

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

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
rfl

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

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (fun x ↦ a - x) = (fun p ↦ p.1 - p.2) ∘ fun x ↦ (a, x)

Tactic:
rfl

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

Goal state before:
pp: a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ (fun x ↦ x - a) = (fun p ↦ p.1 - p.2) ∘ fun x ↦ (x, a)

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)

Tactic:
← ENNReal.toReal_zero,

Goal state after:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (fun n ↦ (f n).toReal) fi (𝓝 (ENNReal.toReal 0)) ↔ Tendsto f fi (𝓝 0)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
a b : ℝ
h : a ≤ b
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ LipschitzWith (1 + 1) (uncurry dist)

Tactic:
exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right

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)
key : b.truncateToReal (liminf u f) = liminf (b.truncateToReal ∘ u) f
⊢ liminf (fun a ↦ b.truncateToReal (u a)) f = liminf (b.truncateToReal ∘ u) f

Tactic:
rfl

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)
key : b.truncateToReal (limsup u f) = limsup (b.truncateToReal ∘ u) f
⊢ limsup (fun a ↦ b.truncateToReal (u a)) f = limsup (b.truncateToReal ∘ u) f

Tactic:
rfl

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

Goal state before:
pp: X✝ : Type u_1
X : Type u_2
t : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
⊢ PseudoMetricSpace.toUniformSpace = TopologicalSpace.pseudoMetrizableSpaceUniformity X

Tactic:
rfl

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

Goal state before:
pp: X✝ : Type u_1
X : Type u_2
t : TopologicalSpace X
inst✝ : TopologicalSpace.MetrizableSpace X
⊢ (TopologicalSpace.metrizableSpaceMetric X).toPseudoMetricSpace = TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ (⇑(toPerm e))^[n] = (⇑e)^[n]

Tactic:
rfl

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

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * s.toReal = r • s.toReal

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = ↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
← Int.cast_natCast,

Goal state after:
case inl
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = ↑z.natAbs
⊢ ‖↑↑z.natAbs‖ = ‖↑z‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑z.natAbs‖ = ‖↑z‖

Tactic:
← Int.cast_natCast,

Goal state after:
case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑↑z.natAbs‖ = ‖↑z‖
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ ↑t, x₁ i = x₂ i
i : ι
hi : i ∈ s
h✝ : i ∈ t
⊢ y ⟨i, h✝⟩ = y ⟨i, h✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn f s
t : Finset ι
y : (i : ↥t) → π ↑i
⊢ DependsOn (fun x ↦ f (Function.updateFinset x t y)) (s \ ↑t)

Tactic:
refine fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)
  simp only [Function.updateFinset]
  split_ifs; · rfl
  simp_all

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Type u_2
inst✝ : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π ↑i
⊢ restrict₂ ⋯ y = y

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s : Finset ι
y z : (i : ↥s) → π ↑i
⊢ updateFinset x s y = updateFinset x s fun i ↦ y ⟨↑i, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (P.sup id)

Tactic:
Finset.sup_id_set_eq_sUnion

Goal state after:
α : Type u_1
s : Set (Set α)
P : Finset (Set α)
hP : P.Nonempty
PC : ↑P ⊆ s
⊢ MeasurableSet (⋃₀ ↑P)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
⊢ {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x}

Tactic:
grind

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
x✝ : α
⊢ (p x✝ ↔ q x✝) ↔ (p x✝ → q x✝) ∧ (q x✝ → p x✝)

Tactic:
grind

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: case empty
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s

Tactic:
change GenerateMeasurable (⋃₀ _) _ ↔ _
  simp [← ofPred_exists]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s

Tactic:
rfl

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

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ IsOpen {0}

Tactic:
isOpen_induced_iff

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ ∃ t, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ Subtype.val ⁻¹' t = {0}
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⋃ i, t i) = μ (⋃ i, disjointed t i)

Tactic:
rw [iUnion_disjointed]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ MeasurableSet (measurableAtom x)

Tactic:
have : measurableAtom x = ⋂ (y ∈ (measurableAtom x)ᶜ), s y := by
    apply Subset.antisymm
    · intro z hz
      simp only [mem_iInter, mem_compl_iff]
      intro i hi
      exact mem_of_mem_measurableAtom hz (hs i hi).2.1 (hs i hi).1
    · apply compl_subset_compl.1
      intro z hz
      simp only [compl_iInter, mem_iUnion, mem_compl_iff, exists_prop]
      exact ⟨z, hz, (hs z hz).2.2⟩

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
this : measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y
⊢ MeasurableSet (measurableAtom x)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ : Type u_3
⊢ Functor.mapConst = Functor.map ∘ const β✝

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ : Type u_3
x✝ : OuterMeasure α✝
⊢ id <$> x✝ = x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ γ✝ : Type u_3
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : OuterMeasure α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst✝¹ : Countable ι
inst✝ : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun i j ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → ↑(t i) → β := fun i ↦ g i ∘ Subtype.val
i : ι
x : α
hxi hxj : x ∈ t i
⊢ g' i ⟨x, hxi⟩ = g' i ⟨x, hxj⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ ⨆ i, MeasurableSpace.comap ((fun b ↦ b i) ∘ fun b a ↦ X a b) (inst✝ i) =
    ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
h : i ∈ s
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

Tactic:
simp [h, Measurable.eval, measurable_fst, measurable_snd]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
h : i ∉ s
⊢ Measurable fun x ↦ if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

Tactic:
simp [h, Measurable.eval, measurable_fst, measurable_snd]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
t : (i : δ) → Set (X i)
ht : ∀ (i : δ), MeasurableSet (t i)
⊢ univ.pi t = {f | ∀ (i : δ), f i ∈ t i}

Tactic:
grind

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace β
g : β → Finset α
⊢ (∀ (a : α), Measurable fun x ↦ a ∈ ↑(g x)) ↔ ∀ (a : α), Measurable fun x ↦ a ∈ g x

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ 1 * zero = zero

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ 1 * neg = neg

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ 1 * pos = pos

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ zero * 1 = zero

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ neg * 1 = neg

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ pos * 1 = pos

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ 0 * zero = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ 0 * neg = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ 0 * pos = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ zero * 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ neg * 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ pos * 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ - -zero = zero

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
⊢ - -neg = neg

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
⊢ - -pos = pos

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ -zero * zero = -(zero * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.neg
⊢ -zero * neg = -(zero * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.pos
⊢ -zero * pos = -(zero * pos)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.zero
⊢ -neg * zero = -(neg * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.neg
⊢ -neg * neg = -(neg * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.pos
⊢ -neg * pos = -(neg * pos)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.zero
⊢ -pos * zero = -(pos * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.neg
⊢ -pos * neg = -(pos * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.pos
⊢ -pos * pos = -(pos * pos)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ zero * -zero = -(zero * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.neg
⊢ zero * -neg = -(zero * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.pos
⊢ zero * -pos = -(zero * pos)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.zero
⊢ neg * -zero = -(neg * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.neg
⊢ neg * -neg = -(neg * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg.pos
⊢ neg * -pos = -(neg * pos)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.zero
⊢ pos * -zero = -(pos * zero)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.neg
⊢ pos * -neg = -(pos * neg)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos.pos
⊢ pos * -pos = -(pos * pos)

Tactic:
rfl

Goal state after: