mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k (map e s₂) p) (extend (⇑e) w₂ 0) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
⊢ ∑ x ∈ s₂, extend (⇑e) w₂ 0 (e x) = 1

Tactic:
convert! hw₂ with i hi

Goal state after:
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k (map e s₂) p) (extend (⇑e) w₂ 0) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
i : ι₂
hi : i ∈ s₂
⊢ extend (⇑e) w₂ 0 (e i) = w₂ i
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : Fintype ι
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial 𝕜
⊢ ∀ (x : ι → 𝕜), x ∉ stdSimplex 𝕜 ι

Tactic:
rintro f ⟨-, hf⟩; simp at hf

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_1
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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
he' : (Set.range ⇑(fs.orderEmbOfFin h).toEmbedding).indicator (extend (⇑(fs.orderEmbOfFin h).toEmbedding) w' 0) = w
j : Fin (m + 1)
⊢ extend (⇑(fs.orderEmbOfFin h)) w' 0 ((fs.orderEmbOfFin h) j) ∈ I

Tactic:
simp [(fs.orderEmbOfFin h).injective.extend_apply, hi]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case inr
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hw1 : ∀ i_1 ∈ univ.erase i, w i_1 = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ ∃ j, w j = 0

Tactic:
exact ⟨i + 1, hw1 _ (by simp)⟩

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

Goal state before:
pp: case refine_1.refine_2
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
hx : x ∈ s
⊢ (∑ y ∈ s, if x = y then 1 else 0) = 1

Tactic:
rw [Finset.sum_ite_eq, if_pos hx]

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

Goal state before:
pp: case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U
⊢ x ∈ U

Tactic:
inv_mul_cancel₀ hr₀,

Goal state after:
case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U
⊢ x ∈ U
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
⊢ x ∈ (convexHull 𝕜) (s.pi t)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
⊢ x ∈ (convexHull 𝕜) (s.pi t)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ ⨅ i, comap (⇑(p i)) (𝓝 0) ≤ p.moduleFilterBasis.filter

Tactic:
p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff

Goal state after:
case refine_2
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ ∀ i' ∈ p.moduleFilterBasis.toFilterBasis, id i' ∈ ⨅ i, comap (⇑(p i)) (𝓝 0)
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
⊢ IsTopologicalAddGroup E

Tactic:
rw [hp.withSeminorms_eq]

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
⊢ IsTopologicalAddGroup E
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
⊢ ContinuousSMul 𝕜 E

Tactic:
rw [hp.withSeminorms_eq]

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
⊢ ContinuousSMul 𝕜 E
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
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun x ↦ ContinuousLinearMap.id 𝕜 (F × G) ∘SL (prodₗ S) x

Tactic:
← coprod_inl_inr

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun x ↦ (inl 𝕜 F G).coprod (inr 𝕜 F G) ∘SL (prodₗ S) x
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case hbasis
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]

Goal state after:
case hbasis
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedSpace ℝ 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ p.moduleFilterBasis.filter.HasBasis (fun s ↦ s ∈ p.basisSets) id
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
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma p)

Tactic:
simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily 𝕜 E (κ i)
t : ι → TopologicalSpace E
this✝ : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ i_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ ⨅ i, t i = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
K

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
⊢ IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
⊢ ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
K

Goal state after:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
⊢ IsCompact K →
    ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
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
x : α
hx : x ∈ s
⊢ (fun x_1 ↦ f x) =ᶠ[𝓟 {g | EqOn (⇑g) f s}] fun f ↦ f x

Tactic:
exact fun _ h ↦ (h hx).symm

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ (s ∩ t) + μ[t | sᶜ] * μ sᶜ = μ t

Tactic:
cond_mul_eq_inter hms.compl,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ (s ∩ t) + μ (sᶜ ∩ t) = μ t
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
A₂ : Type u_4
inst✝³ : TopologicalSpace A₂
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₂
inst✝ : IsTopologicalSemiring A₂
⊢ { toFun := fun x ↦ (algebraMap R A) 0, continuous_toFun := ⋯ } = 0

Tactic:
by ext _; exact (algebraMap R A).map_zero

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ ↑C
⊢ ENNReal.ofReal (limsup (fun a ↦ (u a).toReal) f) = limsup u f

Tactic:
have h₁ : IsCoboundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) :=
    IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ by positivity
  have h₂ : IsBoundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) := by
    refine isBoundedUnder_of_eventually_le (a := C) ?_
    filter_upwards [hf] with a ha
    exact ENNReal.toReal_le_coe_of_le_coe ha
  refine (ENNReal.ofReal_limsup h₁ h₂).trans (limsup_congr ?_)
  filter_upwards [hf] with x hx
  exact ENNReal.ofReal_toReal (ne_top_of_le_ne_top (by simp : C ≠ ∞) hx)

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ u)) t * (uniformOn s) u

Tactic:
rw [← Set.inter_comm]
  exact uniformOn_inter hs

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

Goal state before:
pp: case refine_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (⋃ y, univ.pi fun i ↦ (hμ i).set (y i)) = univ

Tactic:
iUnion_univ_pi fun i => (hμ i).set,

Goal state after:
case refine_3
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝¹ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
C : (i : ι) → Set (Set (α i))
hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
this : Encodable ι
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (univ.pi fun a ↦ ⋃ j, (hμ a).set j) = univ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ (∫⁻ (x : α), s.indicator (fun x ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
by
      rw [lintegral_indicator_const₀ hs, ENNReal.mul_rpow_of_nonneg, ← ENNReal.rpow_mul,
        mul_one_div_cancel hp_pos.ne', ENNReal.rpow_one]
      positivity

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
      have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
      simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
hq0_ne : q ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm' 0 q μ = 0

Tactic:
by
  rcases le_or_gt 0 q with hq0 | hq_neg
  · exact eLpNorm'_zero (lt_of_le_of_ne hq0 hq0_ne.symm)
  · simp [eLpNorm'_eq_lintegral_enorm, hμ, hq_neg]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

case neg
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
⊢ (↑p)⁻¹ + (↑q)⁻¹ = (↑r)⁻¹

Tactic:
have hp := h.ne_zero

Goal state after:
case refine_2
p q r : ℝ≥0
hr : r ≠ 0
h : p.HolderTriple q r
hp : p ≠ 0
⊢ (↑p)⁻¹ + (↑q)⁻¹ = (↑r)⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0∞
h : p.toReal.HolderConjugate q.toReal
⊢ p.HolderConjugate q

Tactic:
rw [Real.HolderConjugate] at h

Goal state after:
p q : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal 1
⊢ p.HolderConjugate q
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ (1 + (p - 1)⁻¹)⁻¹ = 1⁻¹ - p⁻¹

Tactic:
rw [inv_eq_iff_eq_inv]

Goal state after:
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
p : ℝ
hp : 0 < p
hf : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ = 0

Tactic:
by
  rw [← eLpNorm'_zero hp (μ := μ) (ε := ε)]
  exact eLpNorm'_congr_enorm_ae (by simp [hf])

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

Goal state before:
pp: t : ℝ
ht : -1 ≤ t ∧ t ≤ 1
x : ℝ
⊢ rexp (t * x) = rexp ((1 + t) / 2 * x + (1 - t) / 2 * -x)

Tactic:
by ring_nf

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
by rw [monovaryOn_iff_smul_rearrangement]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f * g =ᵐ[μ] 0 * g

Tactic:
have hf_eq_zero : f =ᵐ[μ] 0 := ae_eq_zero_of_lintegral_rpow_eq_zero hp0 hf hf_zero

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
hf_eq_zero : f =ᵐ[μ] 0
⊢ f * g =ᵐ[μ] 0 * g
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
rw [← arith_mean_weighted_of_constant s w _ (z j) hw' fun i _ => congrFun rfl]

Goal state after:
case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ ∑ i ∈ s, w i * z j = ∑ i ∈ s, w i * z i