mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r

Tactic:
by
  rw [closedBall_zero_eq, preimage_metric_closedBall]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = vectorSpan k (⇑b '' univ)

Tactic:
vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ Submodule.span k (range fun j ↦ b ↑j -ᵥ b i) = Submodule.span k ((fun x ↦ x -ᵥ b i) '' ⇑b '' (univ \ {i}))
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : y ∈ p.closedBall 0 (r - p x)
⊢ y ∈ p.closedBall x r

Tactic:
p.mem_closedBall_zero

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y ≤ r - p x
⊢ y ∈ p.closedBall x r
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: case refine_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ∀ (p : ↥E) (v : ↥E.direction), ⟨φ ↑(v +ᵥ p), ⋯⟩ = (φ.linear.restrict ⋯) v +ᵥ ⟨φ ↑p, ⋯⟩

Tactic:
· intro p v
    simp only [Subtype.ext_iff, AffineSubspace.coe_vadd]
    apply AffineMap.map_vadd

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case h
𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
ε : ℝ
hε : ε > 0
hr : r ≤ 0
⊢ 0 < ‖1‖ ∧ ‖1‖ * r < ε

Tactic:
simpa using hr.trans_lt hε

Goal state after:
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ f ∈ [Pi.single 0 1 -[𝕜] Pi.single 1 1]

Tactic:
refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩

Goal state after:
𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 0 = f 0 ∧ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 1 = f 1
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
s : Simplex k P 0
⊢ s.closedInterior = {s.points 0}

Tactic:
by
  ext p
  simp only [Simplex.closedInterior, Simplex.setInterior, Nat.reduceAdd, univ_unique,
    Fin.default_eq_zero, Fin.isValue, sum_singleton, Set.mem_Icc, Set.mem_ofPred_eq,
    Set.mem_singleton_iff]
  constructor
  · rintro ⟨w, h0, hi, rfl⟩
    simp [affineCombination_apply, h0]
  · rintro rfl
    exact ⟨1, by simp [affineCombination_apply]⟩

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ nhdsKer (nhdsKer s) = nhdsKer s

Tactic:
by
  simp only [nhdsKer_eq_nhdsKer_iff_nhdsSet, nhdsSet_nhdsKer]

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
⊢ i ∉ s' → (if i ∈ s' then b * w' i else 0) • v i = 0

Tactic:
hi'

Goal state after:
case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : i ∉ s'
⊢ (if i ∈ s' then b * w' i else 0) • v i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
⊢ i ∉ s → (if i ∈ s then a * w i else 0) • v i = 0

Tactic:
hi'

Goal state after:
case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : i ∉ s
⊢ (if i ∈ s then a * w i else 0) • v i = 0
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
z : E
hs : Convex ℝ s
⊢ ConvexOn ℝ s fun z' ↦ dist z' z

Tactic:
by
  simpa [dist_eq_norm, preimage_preimage] using!
    (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Finset E
x : E
w : E → R
hw : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x

Tactic:
simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]

Goal state after:
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ t with w i ≠ 0, w i
⊢ f y ≤ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • ∑ i ∈ t with w i ≠ 0, w i • (f ∘ p) i

Tactic:
←
      centerMass,

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ t with w i ≠ 0, w i
⊢ f y ≤ {i ∈ t | w i ≠ 0}.centerMass w (f ∘ p)
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range ⇑f
⊢ (convexHull ℝ) (sphere x r) ⊆ Set.range ⇑f

Tactic:
convexHull_mono h,

Goal state after:
𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
h : sphere x r ⊆ Set.range ⇑f
⊢ (convexHull ℝ) (Set.range ⇑f) ⊆ Set.range ⇑f
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous[t, _] ⇑q
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
by
  -- The continuity of `q` gives us a finset `s` and a real `ε > 0`
  -- such that `hε : (s.sup p).ball 0 ε ⊆ q.ball 0 1`.
  rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩
  rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩
  -- Now forget that `E` already had a topology and view it as the (semi)normed space
  -- `(E, s.sup p)`.
  clear hp hq t
  let _ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
  let _ : NormedSpace 𝕜 E := { norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }
  -- The inclusion `hε` tells us exactly that `q` is *still* continuous for this new topology
  have : Continuous q := by
    apply Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) ?_)
    rw [← ball_eq_metric]
    exact hε
  -- Hence we can conclude by applying `bound_of_continuous_normedSpace`.
  rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩
  exact ⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ IsClosed[instTopologicalSpace] A ↔
    ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)

Tactic:
isClosed_coinduced,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ IsClosed[⨆ K,
          ⨆ (_ : IsCompact K),
            TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ }]
      (⇑(CompactCoherentification.mk X) ⁻¹' A) ↔
    ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x

Tactic:
have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g | EqOn (⇑g) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) (f' x)
H₂ : ∀ (x : α), Inseparable (s.piecewise f (⇑f') x) (f' x)
⊢ ∃ x ∈ {g | EqOn (⇑g) f s}, l ≤ 𝓝 x
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
⊢ μ[univ | s] = 0 ∨ μ[univ | s] = 1

Tactic:
simp only [cond, Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
    univ_inter, smul_eq_mul, ← ENNReal.div_eq_inv_mul]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
⊢ μ s / μ s = 0 ∨ μ s / μ s = 1
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ f.limsSup = 0

Tactic:
rw [limsSup]
  convert! sInf_empty
  simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

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

Goal state before:
pp: case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ := by
      rw [EventuallyEq, not_eventually] at hu
      exact hu.mono fun x hx => by simpa
    have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
      eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
    have hfu : f.limsup u ≠ 0 := mt limsup_eq_bot.1 hu
    simp [ha_top, top_mul', h_top_le, hfu]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ Continuous fun p ↦ p.1 * p.2

Tactic:
continuous_iff_continuousAt

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ ∀ (x : C(α, β) × C(α, β)), ContinuousAt (fun p ↦ p.1 * p.2) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ Continuous fun a ↦ a⁻¹

Tactic:
continuous_iff_continuousAt

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
⊢ ∀ (x : C(α, β)), ContinuousAt (fun a ↦ a⁻¹) x
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑s', f x ≠ f y

Tactic:
obtain ⟨f, m, w⟩ := h n

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s ↦ s.SeparatesPoints) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f ↦ ⇑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑s', f x ≠ f y
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
⊢ IsPiSystem (univ.pi '' univ.pi C)

Tactic:
by
  rintro _ ⟨s₁, hs₁, rfl⟩ _ ⟨s₂, hs₂, rfl⟩ hst
  rw [← pi_inter_distrib] at hst ⊢; rw [univ_pi_nonempty_iff] at hst
  exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) f
⊢ μ {y | essSup f μ < f y} = 0

Tactic:
simp_rw [← not_le]
  exact ae_le_essSup hf

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (ae μ) f
⊢ μ {y | f y < essInf f μ} = 0

Tactic:
by
  simp_rw [← not_le]
  exact ae_essInf_le hf

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

Goal state before:
pp: case cons
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod
⊢ ((μ a).prod (Measure.tprod l μ)) (s a ×ˢ Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) (a :: l)).prod

Tactic:
simp only [foldr_cons, prod_cons, map_cons]

Goal state after:
case cons
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod
⊢ ((μ a).prod (Measure.tprod l μ)) (s a ×ˢ Set.tprod l s) = (μ a) (s a) * (List.map (fun i ↦ (μ i) (s i)) l).prod
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑f x ⊔ (-↑f) x = ↑f x ⊔ -↑f x

Tactic:
Pi.neg_apply

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
x : α
hx_sup : ↑(f ⊔ -f) x = ↑f x ⊔ ↑(-f) x
hx_neg : ↑(-f) x = (-↑f) x
⊢ ↑f x ⊔ -↑f x = ↑f x ⊔ -↑f x
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
f : (i : ι) → α i
⊢ (Measure.pi μ) {f} = ∏ i, (μ i) {f i}

Tactic:
simpa [Set.univ_pi_singleton, -pi_pi] using pi_pi μ fun i ↦ {f i}

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x ↦ c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x ↦ c) a‖ₑ} = 0
x : α
hx_mem : x ∈ s
⊢ ‖c‖ₑ ≤ ‖s.indicator (fun x ↦ c) x‖ₑ

Tactic:
Set.indicator_of_mem hx_mem

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμs : μ s ≠ 0
h : eLpNormEssSup (s.indicator fun x ↦ c) μ < ‖c‖ₑ
h' : μ {a | ‖c‖ₑ ≤ ‖s.indicator (fun x ↦ c) a‖ₑ} = 0
x : α
hx_mem : x ∈ s
⊢ ‖c‖ₑ ≤ ‖c‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
⊢ eLpNormEssSup (s.piecewise f g) μ = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))

Tactic:
by
  simp only [eLpNormEssSup, ← ENNReal.essSup_piecewise hs]
  congr with x
  by_cases hx : x ∈ s <;> simp [hx]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ ↑c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), ↑(c ^ p) * ‖g a‖ₑ ^ p ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ q * (1 / q) = 1

Tactic:
rw [one_div, mul_inv_cancel₀ (ne_of_lt hq_pos).symm]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x ↦ RCLike.re (f x)) μ

Tactic:
exact RCLike.continuous_re.comp_aestronglyMeasurable hf.1

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hx : 0 < x
⊢ z ∈ Ioi 0 → x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)

Tactic:
(hz : 0 < z)

Goal state after:
x y z : ℝ
hx : 0 < x
hz : 0 < z
⊢ x < y → y < z → (log z - log y) / (z - y) < (log y - log x) / (y - x)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q

Tactic:
rw [← inv_lt_one₀ hp', ← sub_pos] at hp

Goal state after:
p q : ℝ
hp : 0 < 1 - p⁻¹
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
hp : 1 < p.toNNReal
⊢ p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q

Tactic:
simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
  apply toReal_iff ?_
  all_goals simpa [← coe_toNNReal_eq_toReal]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_8
inst✝ : ENorm ε
f : α → ε
μ ν : Measure α
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
rw [lintegral_add_measure _ μ ν]

Goal state after: