mathlib-initiative/mathlib-tactics huggingface dataset:
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 f l (cobounded E)

Tactic:
← comap_norm_atTop',

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto f l (comap norm atTop)
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case h0
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) ≠ 0

pp: case hinf
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) ≠ ∞

Tactic:
<;>

Goal state after:
case h0
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) ≠ 0

case hinf
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ ↑(ratio f) ≠ ∞
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = 0
⊢ edist (e x) (e y) = 0

pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = ∞
⊢ edist (e x) (e y) = ∞

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = 0
⊢ edist (e x) (e y) = 0

case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = ∞
⊢ edist (e x) (e y) = ∞
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case ha
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖x.1‖

pp: case hd
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖y.2‖

Tactic:
<;>

Goal state after:
case ha
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖x.1‖

case hd
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ 0 ≤ ‖y.2‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1)‖ ≤ ‖↑a - 1‖ * ‖↑b - 1‖

pp: case h₂
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑b - 1) * (↑a - 1)‖ ≤ ‖↑b - 1‖ * ‖↑a - 1‖

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑a - 1) * (↑b - 1)‖ ≤ ‖↑a - 1‖ * ‖↑b - 1‖

case h₂
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖(↑b - 1) * (↑a - 1)‖ ≤ ‖↑b - 1‖ * ‖↑a - 1‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖₊ ≤ 2 * ‖↑a⁻¹‖₊ * ‖↑b⁻¹‖₊ * ‖↑a - 1‖₊ * ‖↑b - 1‖₊

Tactic:
simpa using! norm_commutator_units_sub_one_le a b

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

pp: case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

pp: case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

pp: case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

pp: case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∉ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

case pos
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i

case neg
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π ↑i
z : (i : ↥t) → π ↑i
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∉ t
⊢ updateFinset (updateFinset x s y) t z i = updateFinset x (s ∪ t) ((piFinsetUnion π hst) (y, z)) i
Module: Mathlib.Data.Prod.TProd

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

Tactic:
rw [mk_preimage_tprod l t]

Goal state after:
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 i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 ∈ {i_2 | i_2 ∈ i :: l} → f i_1 ∈ t i_1

Tactic:
simp_rw [mem_ofPred_eq, mem_cons]

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 i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖x‖

pp: case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖y‖

Tactic:
<;>

Goal state after:
case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖x‖

case hba
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ r ≤ ‖y‖
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case mp
K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K → IsComplete (closedBall 0 1)

pp: case mpr
K : Type u_4
inst✝ : NormedField K
⊢ IsComplete (closedBall 0 1) → CompleteSpace K

Tactic:
<;>

Goal state after:
case mp
K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K → IsComplete (closedBall 0 1)

case mpr
K : Type u_4
inst✝ : NormedField K
⊢ IsComplete (closedBall 0 1) → CompleteSpace K
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
h✝ : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) → MeasurableSet s

pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ MeasurableSet s → Measurable (s.indicator fun x ↦ b)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x ↦ b) → MeasurableSet s

case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ MeasurableSet s → Measurable (s.indicator fun x ↦ b)
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : p
⊢ MeasurableSet {_a | p}

pp: case neg
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : ¬p
⊢ MeasurableSet {_a | p}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : p
⊢ MeasurableSet {_a | p}

case neg
α : Type u_1
m : MeasurableSpace α
p : Prop
h✝ : ¬p
⊢ MeasurableSet {_a | p}
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case hx
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x + r • ‖y‖⁻¹ • y ∈ sphere x r

pp: case hy
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x - r • ‖y‖⁻¹ • y ∈ sphere x r

Tactic:
<;>

Goal state after:
case hx
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x + r • ‖y‖⁻¹ • y ∈ sphere x r

case hy
E : Type u_6
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x - r • ‖y‖⁻¹ • y ∈ sphere x r
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}

pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a | p a b}ᶜ)

Tactic:
<;>

Goal state after:
case h₂.h₁
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ k ≠ 0 → MeasurableSet {x | p x k}

case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
⊢ ∀ (b : ℕ), MeasurableSet (⋂ (_ : k < b), ⋂ (_ : b ≤ N), {a | p a b}ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:

Tactic:
<;>

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

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)

Tactic:
<;>

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝ : ℕ
⊢ k < b✝ → MeasurableSet (⋂ (_ : b✝ ≤ N), {a | p a b✝}ᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ

Tactic:
<;>

Goal state after:
case h₂.h₂
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
k : ℕ
hk : k ≤ N
b✝¹ : ℕ
b✝ : k < b✝¹
⊢ b✝¹ ≤ N → MeasurableSet {a | p a b✝¹}ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet {x | p x k}
⊢ Measurable fun x ↦ Nat.findGreatest (p x) N

Tactic:
refine measurable_findGreatest' fun k hk => ?_
  simp only [Nat.findGreatest_eq_iff, ofPred_and, ofPred_forall, ← compl_ofPred]
  repeat' apply_rules [MeasurableSet.inter, MeasurableSet.const, MeasurableSet.iInter,
    MeasurableSet.compl, hN] <;> try intros

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k ↦ {x | p x k}) (Nat.find ⋯))

Tactic:
exact MeasurableSet.disjointed hm _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ MeasurableSet u

Tactic:
convert! (hs.subtype_image hsu).union (ht.subtype_image htu)

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ u = Subtype.val '' Subtype.val ⁻¹' u ∪ Subtype.val '' Subtype.val ⁻¹' u
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
⊢ ‖f (n • x)‖ < C

Tactic:
· refine hC _ <| norm_nsmul_le.trans_lt ?_
        simpa only [norm_mul, Real.norm_natCast, lt_div_iff₀ hnpos, mul_comm] using hxδ

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

pp: case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x

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:
<;>

Goal state after:
case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β : Type u_3}, Functor.mapConst = Functor.map ∘ const β

case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α : Type u_3} (x : OuterMeasure α), id <$> x = x

case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ ∀ {α β γ : Type u_3} (g : α → β) (h : β → γ) (x : OuterMeasure α), (h ∘ g) <$> x = h <$> g <$> 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 β✝

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

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:
<;>

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

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

case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ γ✝ : Type u_3
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : OuterMeasure α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
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

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:
<;>

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

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
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)

Tactic:
exact MeasurableSet.univ.inl_image

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

Goal state before:
pp: case zero
⊢ zero = -1 ∨ zero = 0 ∨ zero = 1

pp: case neg
⊢ neg = -1 ∨ neg = 0 ∨ neg = 1

pp: case pos
⊢ pos = -1 ∨ pos = 0 ∨ pos = 1

Tactic:
<;>

Goal state after:
case zero
⊢ zero = -1 ∨ zero = 0 ∨ zero = 1

case neg
⊢ neg = -1 ∨ neg = 0 ∨ neg = 1

case pos
⊢ pos = -1 ∨ pos = 0 ∨ pos = 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
b : SignType
⊢ Decidable (zero ≤ b)

pp: case neg
b : SignType
⊢ Decidable (neg ≤ b)

pp: case pos
b : SignType
⊢ Decidable (pos ≤ b)

Tactic:
<;>

Goal state after:
case zero
b : SignType
⊢ Decidable (zero ≤ b)

case neg
b : SignType
⊢ Decidable (neg ≤ b)

case pos
b : SignType
⊢ Decidable (pos ≤ b)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ Decidable (zero ≤ zero)

pp: case zero.neg
⊢ Decidable (zero ≤ neg)

pp: case zero.pos
⊢ Decidable (zero ≤ pos)

pp: case neg.zero
⊢ Decidable (neg ≤ zero)

pp: case neg.neg
⊢ Decidable (neg ≤ neg)

pp: case neg.pos
⊢ Decidable (neg ≤ pos)

pp: case pos.zero
⊢ Decidable (pos ≤ zero)

pp: case pos.neg
⊢ Decidable (pos ≤ neg)

pp: case pos.pos
⊢ Decidable (pos ≤ pos)

Tactic:
<;>

Goal state after:
case zero.zero
⊢ Decidable (zero ≤ zero)

case zero.neg
⊢ Decidable (zero ≤ neg)

case zero.pos
⊢ Decidable (zero ≤ pos)

case neg.zero
⊢ Decidable (neg ≤ zero)

case neg.neg
⊢ Decidable (neg ≤ neg)

case neg.pos
⊢ Decidable (neg ≤ pos)

case pos.zero
⊢ Decidable (pos ≤ zero)

case pos.neg
⊢ Decidable (pos ≤ neg)

case pos.pos
⊢ Decidable (pos ≤ pos)
Module: Mathlib.Data.Sign.Defs

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

pp: case neg
⊢ 1 * neg = neg

pp: case pos
⊢ 1 * pos = pos

Tactic:
<;>

Goal state after:
case zero
⊢ 1 * zero = zero

case neg
⊢ 1 * neg = neg

case pos
⊢ 1 * pos = pos
Module: Mathlib.Data.Sign.Defs

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

pp: case neg
⊢ neg * 1 = neg

pp: case pos
⊢ pos * 1 = pos

Tactic:
<;>

Goal state after:
case zero
⊢ zero * 1 = zero

case neg
⊢ neg * 1 = neg

case pos
⊢ pos * 1 = pos
Module: Mathlib.Data.Sign.Defs

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

pp: case neg
⊢ 0 * neg = 0

pp: case pos
⊢ 0 * pos = 0

Tactic:
<;>

Goal state after:
case zero
⊢ 0 * zero = 0

case neg
⊢ 0 * neg = 0

case pos
⊢ 0 * pos = 0
Module: Mathlib.Data.Sign.Defs

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

pp: case neg
⊢ neg * 0 = 0

pp: case pos
⊢ pos * 0 = 0

Tactic:
<;>

Goal state after:
case zero
⊢ zero * 0 = 0

case neg
⊢ neg * 0 = 0

case pos
⊢ pos * 0 = 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
ha : zero ≠ 0
⊢ zero * id zero = 1

pp: case neg
ha : neg ≠ 0
⊢ neg * id neg = 1

pp: case pos
ha : pos ≠ 0
⊢ pos * id pos = 1

Tactic:
<;>

Goal state after:
case zero
ha : zero ≠ 0
⊢ zero * id zero = 1

case neg
ha : neg ≠ 0
⊢ neg * id neg = 1

case pos
ha : pos ≠ 0
⊢ pos * id pos = 1