mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet t

Tactic:
rwa [← h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
g : α → β
f : β → γ
hg : Function.Surjective g
⊢ mγ ≤ MeasurableSpace.map f mβ ↔ mγ ≤ MeasurableSpace.map f mβ

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ x, f (e x))

Tactic:
]

Goal state after:
case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ x, f (e x))
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)

Tactic:
]

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
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ x, f ↑x)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ x, f ↑x)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSingletonClass α
hf : Measurable f
h : {x | f x ≠ g x}.Countable
t : Set β
ht : MeasurableSet t
this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}
this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}
⊢ MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ b, bif b then s₁ else s₂)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ b, bif b then s₁ else s₂)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ᶜ ∪ s₂ᶜ)ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₂ ⊔ s₁ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ univ = univ

Tactic:
]

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}
h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x}
⊢ MeasurableSet ({x | p x}ᶜ ∪ {x | q x})

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x → q x} = {x | p x}ᶜ ∪ {x | q x}
⊢ MeasurableSet ({x | p x}ᶜ ∪ {x | q x})
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}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet ({x | p x → q x} ∩ {x | q x → p x})

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p q : α → Prop
hs : MeasurableSet {x | p x}
ht : MeasurableSet {x | q x}
h_eq : {x | p x ↔ q x} = {x | p x → q x} ∩ {x | q x → p x}
⊢ MeasurableSet ({x | p x → q x} ∩ {x | q x → p x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet (insert a s)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet (insert a s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : s.Countable
⊢ MeasurableSet (⋃ x ∈ s, {x})
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom S = generateFrom S

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ (∀ (i : ι), MeasurableSet s) ↔ ∀ (i : ι), MeasurableSet s

Tactic:
]

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:
by
  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:
]

Goal state after:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℤ
x : E
⊢ ‖n • x‖ = ‖n • x‖

Tactic:
]

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

Goal state before:
pp: α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℤ
⊢ |↑n| * ‖1‖ = |↑n| * ‖1‖

Tactic:
]

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

Goal state before:
pp: case inl
𝕜 : 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
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥⊥

Tactic:
]

Goal state after:
case inl
𝕜 : 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
this : IsAddTorsionFree E
⊢ DiscreteTopology ↥⊥
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
⊢ ∃ t, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ Subtype.val ⁻¹' t = {0}

Tactic:
]

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.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
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ k = 0 ↔ k = 0

Tactic:
]

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c / ‖x‖ < ‖r‖

pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖

Tactic:
]

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c / ‖x‖ < ‖r‖

case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ x ≠ 0

Tactic:
]

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ x ≠ 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬Bornology.IsBounded univ

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬Bornology.IsBounded univ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ ‖x‖ ≤ ‖x‖

pp: case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0

Tactic:
]

Goal state after:
case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ (Infinite.natEmbedding 𝕜) k - (Infinite.natEmbedding 𝕜) n ≠ 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ k ≠ n

Tactic:
]

Goal state after:
case neg._
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : Infinite 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Nontrivial E
inst✝ : NormedSpace 𝕜 E
H : ∀ (c : 𝕜), c ≠ 0 → ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
⊢ k ≠ n
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
⊢ ‖x • 1‖ = ‖x‖ * ‖1‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖x‖ = ‖x‖

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ ⇑(algebraMap 𝕜 𝕜') ⁻¹' c ∈ cobounded 𝕜

Tactic:
]

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : c ∈ cobounded 𝕜'
⊢ ⇑(algebraMap 𝕜 𝕜') ⁻¹' c ∈ cobounded 𝕜
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : ∃ C, ∀ x ∈ cᶜ, ‖x‖ ≤ C
⊢ ∃ C, ∀ x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ, ‖x‖ ≤ C

Tactic:
]

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
hc : ∃ C, ∀ x ∈ cᶜ, ‖x‖ ≤ C
⊢ ∃ C, ∀ x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ, ‖x‖ ≤ C
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (⋃ y ∈ s, f ⁻¹' {y})
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ ‖x - y‖ = ‖x - y‖

Tactic:
]

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁵ : NormedField 𝕜✝
inst✝⁴ : SeminormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜✝ 𝕜'
𝕜 : Type ?u.15
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : CharZero 𝕜
inst✝ : NormedAlgebra ℝ 𝕜
q : ℚ
x : 𝕜
⊢ ‖q‖ * ‖x‖ ≤ ‖q‖ * ‖x‖

Tactic:
]

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

Goal state before:
pp: case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ

Tactic:
]

Goal state after:
case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜' E
c : 𝕜
x : E
⊢ ‖c‖ * ‖x‖ = ‖c‖ * ‖x‖

Tactic:
]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ f ⁻¹' {false} = f ⁻¹' {false}

Tactic:
]

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = 0 • 0
⊢ ‖0‖ * ‖0‖ = 0

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x : E
this : 0 = 0 • 0
⊢ ‖0‖ * ‖0‖ = 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-1‖ * ‖-x + y‖

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y : E
this : -y + x = -1 • (-x + y)
⊢ ‖-x + y‖ = ‖-1‖ * ‖-x + y‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Norm E
inst✝ : Module 𝕜 E
core : SeminormedSpace.Core 𝕜 E
x y z : E
this : -x + z = -x + y + (-y + z)
⊢ ‖-x + y + (-y + z)‖ ≤ ‖-x + y‖ + ‖-y + z‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0
Module: Mathlib.Data.Real.ENatENNReal

Goal state before:
pp: n : ℕ∞
⊢ n = 0 ↔ n = 0

Tactic:
]

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
]

Goal state after:
𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 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, t i)

Tactic:
]

Goal state after:
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 α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)