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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝[s] x, r p.1 p.2
seg : ∀ᶠ (χ : α) in f, [y χ -[ℝ] z χ] ⊆ s
⊢ ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, p.2 ∈ s → r p.1 p.2

Tactic:
simpa [nhdsWithin, prod_eq_inf, ← inf_assoc, eventually_inf_principal] using hr

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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
i : ι
hi : i ∈ t
this : f (∑ k ∈ t, w k • p i) = ∑ k ∈ t, w k • f (p i)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)

Tactic:
convert this using 3

Goal state after:
case e'_2.a
𝕜 : 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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
i : ι
hi : i ∈ t
this : f (∑ k ∈ t, w k • p i) = ∑ k ∈ t, w k • f (p i)
x✝ : ι
a✝ : x✝ ∈ t
⊢ w x✝ • p x✝ = w x✝ • p i

case e'_3.a
𝕜 : 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✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
h : ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
i : ι
hi : i ∈ t
this : f (∑ k ∈ t, w k • p i) = ∑ k ∈ t, w k • f (p i)
x✝ : ι
a✝ : x✝ ∈ t
⊢ f (p x✝) = f (p i)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ (Finset.affineCombination 𝕜 u s.points) w ∈ s.closedInterior

Tactic:
Finset.affineCombination_indicator_subset _ _ u.subset_univ,

Goal state after:
case mp
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
⊢ (Finset.affineCombination 𝕜 Finset.univ s.points) ((↑u).indicator w) ∈ s.closedInterior
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
by
  rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
  exact AddGroupFilterBasis.nhds_zero_hasBasis _

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2

Tactic:
have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
    Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this✝ : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (x +ᵥ 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Tactic:
exact forall₃_congr fun _ _ _ => Filter.eventually_atTop

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
⊢ w = Finset.univ

Tactic:
ext j

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
j : Fin 1
⊢ j ∈ w ↔ j ∈ Finset.univ
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C

Tactic:
← inv_inv c,

Goal state after:
case neg
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
c : 𝕜
hc : ‖c⁻¹⁻¹‖ < 1
hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
h0 : ¬c = 0
⊢ ‖f‖ ≤ C
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝¹ x✝ : G →L[𝕜] G
⊢ (↑↑(e.arrowCongr e)).toFun (x✝¹ * x✝) = (↑↑(e.arrowCongr e)).toFun x✝¹ * (↑↑(e.arrowCongr e)).toFun x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝ : 𝕜
⊢ (↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝) = (algebraMap 𝕜 (H →L[𝕜] H)) x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ((s.sup q).comp f) x = (s.sup (q.comp f)) x

Tactic:
rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk ((q i) (f x)) ⋯) = ↑(s.sup fun i ↦ NNReal.mk ((q.comp f i) x) ⋯)
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
⊢ Tendsto F p (𝓝 f)

Tactic:
tendsto_iff_forall_isCompact_tendstoUniformlyOn

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ V

Tactic:
tendsto_iff_forall_isCompact_tendstoUniformlyOn

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : WeaklyLocallyCompactSpace α
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ V
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
⊢ f.bilinearComp 0 gF = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
⊢ f.bilinearComp gE 0 = 0

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ liminf (fun x ↦ u x * a) f = a * liminf u f

Tactic:
by
  simpa [mul_comm] using liminf_const_mul_of_ne_top ha_top

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 β
f : C(α, β)
⊢ Filter.Tendsto (fun a ↦ a⁻¹) (nhds f) (nhds f⁻¹)

Tactic:
tendsto_iff_forall_isCompact_tendstoUniformlyOn

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
this✝ : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
this : IsUniformGroup β
f : C(α, β)
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ i⁻¹ a) (⇑f⁻¹) (nhds f) K
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ uniformOn ∅ = 0

Tactic:
by simp [uniformOn]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
s : Set Ω
inst✝ : MeasurableSingletonClass Ω
⊢ uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Tactic:
by simp [uniformOn]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ↑(#⋯.toFinset) = ↑(#hsf.toFinset)
⊢ s ⊆ t

Tactic:
Nat.cast_inj

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #⋯.toFinset = #hsf.toFinset
⊢ s ⊆ t
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g : α →ₘ[μ] β
⊢ g ≤ f ⊔ g

Tactic:
by
  rw [← coeFn_le]
  filter_upwards [coeFn_sup f g] with _ ha
  rw [ha]
  exact le_sup_right

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → α → ℝ≥0∞
⊢ essSup (fun x ↦ liminf (fun n ↦ f n x) atTop) μ ≤ liminf (fun n ↦ essSup (fun x ↦ f n x) μ) atTop

Tactic:
essSup

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → α → ℝ≥0∞
⊢ limsup (fun x ↦ liminf (fun n ↦ f n x) atTop) (ae μ) ≤ liminf (fun n ↦ limsup (fun x ↦ f n x) (ae μ)) atTop
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := ⋯
A : 0 < (μ.restrict t) t
⊢ t ⊆ Function.support f

Tactic:
intro x (hx : d < f x)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : Function.support f ⊆ s
c : ℝ≥0∞
hc : c < essSup f μ
d : ℝ≥0∞
cd : c < d
hd : d < essSup f μ
t : Set α := {x | d < f x}
A : 0 < (μ.restrict t) t
x : α
hx : d < f x
⊢ x ∈ Function.support f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) = fun x ↦ Classical.choose h

Tactic:
by ext; simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)

Tactic:
← pi'_pi μ s,

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ (pi' μ) (univ.pi s) ≤ (Measure.pi μ) (univ.pi s)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

pp: case neg
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
· simp [h_top, eLpNormEssSup_eq_essSup_enorm]

Goal state after:
case neg
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
obtain hμ_top | hμ_ne_top := eq_or_ne (μ .univ) ∞

Goal state after:
case neg.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_top : μ Set.univ = ∞
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

case neg.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default).toOuterMeasure (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)

Tactic:
coe_toOuterMeasure

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
s : Set ((i : ι) → X i)
⊢ (μ default) (eval default '' s) = (μ default) (⇑e.symm ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
⊢ Measure.map (⇑(MeasurableEquiv.piUnique X)) (Measure.pi μ) = μ default

Tactic:
by
    set e := MeasurableEquiv.piUnique X
    have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by
      ext1 s
      rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure]
      congr 1; exact e.toEquiv.image_eq_preimage_symm s
    simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self,
      toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm]

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

Goal state before:
pp: case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ False

Tactic:
have := calc
      0⁻¹ = p⁻¹ + q⁻¹ := inv_eq p q 0
      _ < ⊤ + ⊤ := by simp [hp, hq, pos_iff_ne_zero]
      _ = ⊤ := by simp

Goal state after:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
this : 0⁻¹ < ∞
⊢ False
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ

Tactic:
exact eLpNorm'_mono_measure f hμν ENNReal.toReal_nonneg

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ p * q = p + q

Tactic:
by
  simpa only [sub_mul, sub_eq_iff_eq_add, one_mul] using h.sub_one_mul_conj

Goal state after:
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

Tactic:
simp only [smul_eq_mul, monovaryOn_iff_forall_smul_nonneg]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]

Goal state after:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ∞
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ ¬p < 0

Tactic:
simp [hp_nonneg]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
this : ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i

Tactic:
convert this using 3

Goal state after:
case e'_2.a
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
this : ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k
x✝ : ι
a✝ : x✝ ∈ s
⊢ z x✝ = z k

case e'_3.a
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
k : ι
hk : k ∈ s
this : ∏ i ∈ s, z k ^ w i = ∑ i ∈ s, w i * z k
x✝ : ι
a✝ : x✝ ∈ s
⊢ z x✝ = z k