mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α✝ : Type u_2
β : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ ‖1‖ = 1

Tactic:
simpa using

Goal state after:
G : Type u_1
α✝ : Type u_2
β : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ (Finset.univ.sup fun b ↦ 1) = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖

Tactic:
simpa using

Goal state after:
β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a * a ^ (n + 1)‖₊ ≤ ‖a‖₊ * ‖a‖₊ ^ (n + 1)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a - a * b‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
f : S → ℝ
hf_pm : IsPowMul f
x : ↥A
n : ℕ
hn : 1 ≤ n
⊢ (fun x ↦ f ↑x) (x ^ n) = (fun x ↦ f ↑x) x ^ n

Tactic:
simpa using

Goal state after:
R : Type u_5
S : Type u_6
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
f : S → ℝ
hf_pm : IsPowMul f
x : ↥A
n : ℕ
hn : 1 ≤ n
⊢ f (↑x ^ n) = f ↑x ^ n
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : NormedAddCommGroup α
inst✝² : MulOneClass α
inst✝¹ : NormMulClass α
inst✝ : Nontrivial α
u : α
hu : u ≠ 0
⊢ ‖1‖ = 1

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : NormedAddCommGroup α
inst✝² : MulOneClass α
inst✝¹ : NormMulClass α
inst✝ : Nontrivial α
u : α
hu : u ≠ 0
⊢ ‖1‖ = 1
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NormedRing α
inst✝ : NormMulClass α
a✝ b✝ : α
h : a✝ * b✝ = 0
⊢ a✝ = 0 ∨ b✝ = 0

Tactic:
simpa using

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NormedRing α
inst✝ : NormMulClass α
a✝ b✝ : α
h : a✝ * b✝ = 0
⊢ ‖a✝‖ = 0 ∨ ‖b✝‖ = 0
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y z : R
⊢ v (-x + z) ≤ v (-x + y) + v (-y + z)

Tactic:
simpa using

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst✝ : Ring R
v : AbsoluteValue R ℝ
x y z : R
⊢ v (z - x) ≤ v (z - y) + v (y - x)
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : IsBoundedSMul α β
s : α
x y : β
⊢ ‖-(s • x) + s • y‖ ≤ ‖s‖ * ‖-x + y‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ ‖x * y₁ - x * y₂‖ ≤ ‖x‖ * ‖y₁ - y₂‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ y : α
⊢ ‖x₁ * y - x₂ * y‖ ≤ ‖x₁ - x₂‖ * ‖y‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ ‖a • b₁ - a • b₂‖ ≤ ‖a‖ * ‖b₁ - b₂‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ ‖a₁ • b - a₂ • b‖ ≤ ‖a₁ - a₂‖ * ‖b‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x < ε
⊢ dist (s • y) (s • x) < ‖s‖ * ε

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x < ε
⊢ ‖s‖ * dist y x < ‖s‖ * ε
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist p (s • x) < ‖s‖ * ε
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x ≤ ε
⊢ dist (s • y) (s • x) ≤ ‖s‖ * ε

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
y : β
h1 : dist y x ≤ ε
⊢ ‖s‖ * dist y x ≤ ‖s‖ * ε
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist (s • s⁻¹ • p) (s • x) ≤ ‖s‖ * ε

Tactic:
simpa using

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist p (s • x) ≤ ‖s‖ * ε
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t

Tactic:
Set.tprod,

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f ∈ TProd.mk (i :: l) ⁻¹' t i ×ˢ Set.tprod l t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : -↑m < 0
⊢ Tendsto (fun x ↦ x ^ (-↑m)) (𝓝[≠] 0) (cobounded α)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : -↑m < 0
⊢ Tendsto (fun x ↦ (x ^ m)⁻¹) (𝓝[≠] 0) (cobounded α)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ x ≠ 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ ¬x = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))
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)
this : Countable ↑s
⊢ ∀ (b : ↑s), MeasurableSet (f ↑b)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ ∀ a ∈ s, MeasurableSet (f a)
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 (⋂₀ s)

Tactic:
rw [sInter_eq_biInter]
  exact MeasurableSet.biInter hs h

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

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

Tactic:
simpa using

Goal state after:
α : Type u_6
inst✝¹ : SeminormedRing α
inst✝ : NormSMulClass ℤ α
n : ℕ
⊢ ‖↑n‖ = ↑n * ‖1‖
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: α : Type u_6
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormSMulClass ℤ α
a : ℕ
⊢ ‖↑a‖ = ↑a

Tactic:
simpa using

Goal state after:
α : Type u_6
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormSMulClass ℤ α
a : ℕ
⊢ ‖↑a‖ = ↑a
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ 2 * r' ≤ diam (ball x r)

Tactic:
simpa using

Goal state after:
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ diam (sphere x r') ≤ diam (ball x r)
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 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
x : 𝕜
hx : x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ
⊢ ‖x‖ ≤ s

Tactic:
simpa using

Goal state after:
𝕜 : Type u_6
𝕜' : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
c : Set 𝕜'
s : ℝ
hs : ∀ x ∈ cᶜ, ‖x‖ ≤ s
x : 𝕜
hx : x ∈ (⇑(algebraMap 𝕜 𝕜') ⁻¹' c)ᶜ
⊢ ‖x‖ ≤ s
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ⇑(algebraMap 𝕜 𝕜')

Tactic:
by
  refine Isometry.of_dist_eq fun x y => ?_
  rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap']

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

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

Tactic:
| coe n =>

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 y : E
⊢ ‖-x + y‖ = ‖-y + x‖

Tactic:
show ‖-x + y‖ = ‖-y + x‖

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
⊢ ‖-x + y‖ = ‖-y + x‖
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet {a | f a}
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet {a | ¬f a}
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 α
inst✝ : Fintype ι
μ : F
s : ι → Set α
⊢ μ (⋃ i, s i) ≤ ∑ i, μ (s i)

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Fintype ι
μ : F
s : ι → Set α
⊢ μ (⋃ i, s i) ≤ ∑ i, μ (s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ (s ∪ t) ≤ μ s + μ t

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ (⋃ b, bif b then s else t) ≤ μ s + μ t
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ s ≤ μ (s ∩ t) + μ (s \ t)

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ s ≤ μ (s ∩ t) + μ (s \ t)
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
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
x✝ : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
x✝ : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
⊢ Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M)

Tactic:
simpa using

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
⊢ Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ inclusion h '' Subtype.val ⁻¹' u ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ x ∈ s ∧ x ∈ u ↔ x ∈ u ∧ x ∈ s
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x y : β
hy : y ∉ measurableAtom x
⊢ ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x y : β
hy : y ∉ measurableAtom x
⊢ ∃ s, x ∈ s ∧ MeasurableSet s ∧ y ∉ s
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ↑n * ‖x‖ < δ

Tactic:
simpa using

Goal state after:
case hbc
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
hn₀ : n ≠ 0
x : G
hxδ : ‖x‖ < δ / ↑n
⊢ ↑n * ‖x‖ < δ
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
⊢ measurableAtom x = ⋂ y ∈ (measurableAtom x)ᶜ, s y

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ measurableAtom x ⊆ ⋂ y ∈ (measurableAtom x)ᶜ, s y

case h₂
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : Countable β
x : β
s : β → Set β
hs : ∀ y ∉ measurableAtom x, x ∈ s y ∧ MeasurableSet (s y) ∧ y ∉ s y
⊢ ⋂ y ∈ (measurableAtom x)ᶜ, s y ⊆ measurableAtom x
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.16
f : α → β
m : OuterMeasure α
s : ℕ → Set β
x✝ : Pairwise (Disjoint on s)
⊢ m (f ⁻¹' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f ⁻¹' s i)

Tactic:
simpa using

Goal state after:
α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.16
f : α → β
m : OuterMeasure α
s : ℕ → Set β
x✝ : Pairwise (Disjoint on s)
⊢ m (⋃ i, f ⁻¹' s i) ≤ ∑' (i : ℕ), m (f ⁻¹' s i)
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ m (f '' ⋃ i, s i) ≤ ∑' (i : ℕ), m (f '' s i)

Tactic:
simpa using

Goal state after:
α : Type u_1
β✝ : Type u_2
m✝ : OuterMeasure α
β : Type ?u.15
f : α → β
m : OuterMeasure β
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
⊢ m (⋃ i, f '' s i) ≤ ∑' (i : ℕ), m (f '' s i)
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ ↑x ≤ 1
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ ↑x
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ((map f) ma) s ≤ ((restrict (range f)) mb) s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_3
ma : OuterMeasure α
mb : OuterMeasure β
f : α → β
h : (map f) ma ≤ mb
s : Set β
⊢ ma (f ⁻¹' s) ≤ mb (s ∩ range f)
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ ↑x < 1
Module: Mathlib.Algebra.Order.Interval.Set.Instances

Goal state before:
pp: β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝² : Ring β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < ↑x
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤ MeasurableSpace.comap (fun b c ↦ g c b) pi

Tactic:
simpa using

Goal state after:
β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    ⨆ i, MeasurableSpace.comap (fun b c ↦ g c b) (MeasurableSpace.comap (fun b ↦ b i) (inst✝ i))
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (map f) ⊤ = ⊤

Tactic:
rw [map_top, hf.range_eq, restrict_univ]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d