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

Goal state before:
pp: case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
hai : LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
⊢ AffineIndependent k (⇑f ∘ p)

Tactic:
simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub]

Goal state after:
case inr
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
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective ⇑f
i : ι
hai : LinearIndependent k fun i_1 ↦ p ↑i_1 -ᵥ p i
⊢ LinearIndependent k fun i_1 ↦ f.linear (p ↑i_1 -ᵥ p i)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
⊢ s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs

Tactic:
by
  rw [range_face_points]
  exact s.independent.mem_affineSpan_iff i fs

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points = Set.range s.points

Tactic:
rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : Fintype Z
⊢ Function.Injective fun s ↦ ↑s

Tactic:
by aesop

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
y : Y
⊢ ∀ i ∈ {x | f x = y}, 0 ≤ s i

Tactic:
by aesop

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

Goal state before:
pp: S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : Fintype X
inst✝² : Fintype Y
inst✝¹ : Fintype Z
inst✝ : IsOrderedRing S
f : X → Y
s : ↑(stdSimplex S X)
⊢ (FunOnFinite.linearMap S S f) ⇑s ∈ ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X

Tactic:
by aesop

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ t.centerMass w z = t'.centerMass w' z'

Tactic:
classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
p : (i : ι) → X i
⊢ nhdsKer {p} = univ.pi fun i ↦ nhdsKer {p i}

Tactic:
simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
a : α
⊢ 𝓝ˢ {a} = 𝓝 a

Tactic:
nhdsSet_singleton

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
a : α
⊢ 𝓝 a = 𝓝 a
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent k fun x ↦ ![p₁, p₂, p₃] ↑x
h : ![p₁, p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
x : Fin 3
⊢ x ∈ {x | x ≠ 2} → ![p₁, p₂, p₃] x ∈ ↑s

Tactic:
fin_cases x <;> simp +decide [hp₁, hp₂]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i}
ha : AffineIndependent k fun x ↦ f ↑x
⊢ f i ∉ affineSpan k (f '' {x | x ≠ i})

Tactic:
by aesop

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)

Tactic:
cthickening_of_nonpos hδ

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (closure s)
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ IsUniformInducing ⇑(outCLM K E)

Tactic:
rw [← isUniformInducing_mk.of_comp_iff, mk_comp_outCLM]
  exact .id

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

Goal state before:
pp: case refine_1.inr
𝕜 : 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
i₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
⊢ p i = ∑ i ∈ t, w i • p i

Tactic:
calc p i = p i₀ := by rw [H _ hi]
      _ = (1 : 𝕜) • p i₀ := by simp
      _ = (∑ j ∈ t, w j) • p i₀ := by rw [h₁]
      _ = ∑ j ∈ t, (w j • p i₀) := by rw [sum_smul]
      _ = ∑ j ∈ t, (w j • p j) := by congr! 2 with j hj; rw [← H _ hj]

Goal state after:
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
val✝ : Fintype ι
t : (i : ι) → Set (E i)
h : ∀ i ∈ Set.univ, x i ∈ (convexHull 𝕜) (t i)
⊢ x ∈ (convexHull 𝕜) (Set.univ.pi t)

Tactic:
simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies] at h

Goal state after:
𝕜 : 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
val✝ : Fintype ι
t : (i : ι) → Set (E i)
h :
  ∀ (i : ι), ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ (i_1 : ι), z i_1 ∈ t i) ∧ ∑ i_1, w i_1 • z i_1 = x i
⊢ x ∈ (convexHull 𝕜) (Set.univ.pi t)
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
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝ : j ∈ Finset.univ
⊢ ∀ a ∈ Finset.univ, ↑a ∈ piFinset fun k ↦ if hk : k = i then ⋯ ▸ {j} else Finset.univ

Tactic:
by aesop

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

Goal state before:
pp: 𝕜 : Type u_11
E : Type u_12
ι : Type u_13
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous[inst✝, _] ⇑(p i)
U : Set E
hU : U ∈ p.basisSets
⊢ U ∈ 𝓝 0

Tactic:
obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU
  clear hU
  refine Seminorm.ball_mem_nhds ?_ hr
  classical
  induction s using Finset.induction_on with
  | empty => simpa using continuous_zero
  | insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
G : Type u_8
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ f '' s, (I.sup p) x < r) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r

Tactic:
Set.forall_mem_image

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
G : Type u_8
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r > 0, ∀ x ∈ f '' s, (p i) x < r) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r

Tactic:
Set.forall_mem_image

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ ‖f‖₊ ≤ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)

Tactic:
rw [← sSup_unit_ball_eq_nnnorm]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ sSup ((fun x ↦ ‖f x‖₊) '' ball 0 1) ≤ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)
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 σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ WithSeminorms (q.comp f)

Tactic:
rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero,
    q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.comap_iInf]

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 σ₁₂
inst✝ : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this✝ : IsTopologicalAddGroup F
x✝ : TopologicalSpace E := TopologicalSpace.induced (⇑f) inferInstance
this : IsTopologicalAddGroup E
⊢ ⨅ i, comap (⇑f) (comap (⇑(q i)) (𝓝 0)) = ⨅ i, comap (⇑(q.comp f i)) (𝓝 0)
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s ≠ 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]

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 β
⊢ Continuous fun a ↦ a⁻¹

Tactic:
by
    let : UniformSpace β := IsTopologicalGroup.rightUniformSpace β
    have : IsUniformGroup β := isUniformGroup_of_commGroup
    rw [continuous_iff_continuousAt]
    intro f
    rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]
    exact fun K hK =>
      uniformContinuous_inv.comp_tendstoUniformlyOn
        (tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ mk ↑(mk f hf) ⋯ = mk f hf

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ mk f hf = mk f hf
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ g.compQuasiMeasurePreserving f hf = (mk ↑g ⋯).compQuasiMeasurePreserving f hf

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f hf
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous[inst✝¹, inst✝] g
f : α →ₘ[μ] β
⊢ comp g hg f = comp g hg (mk ↑f ⋯)

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous[inst✝¹, inst✝] g
f : α →ₘ[μ] β
⊢ comp g hg f = comp g hg f
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ compMeasurable g hg f = compMeasurable g hg (mk ↑f ⋯)

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ compMeasurable g hg f = compMeasurable g hg f
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ limsup u f ≠ ∞

Tactic:
simp only [limsup, limsSup, eventually_map, ne_eq, sInf_eq_top, Set.mem_ofPred_eq, not_forall]

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ ∃ x, ∃ (_ : ∀ᶠ (a : α) in f, u a ≤ x), ¬x = ∞
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ f.toGerm = (mk ↑f ⋯).toGerm

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ f.toGerm = f.toGerm
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
r : β → γ → Prop
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ LiftRel r f g ↔ LiftRel r f (mk ↑g ⋯)

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
r : β → γ → Prop
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ LiftRel r f g ↔ LiftRel r f g
Module: Mathlib.Probability.UniformOn

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

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs') <;> rcases t.eq_empty_or_nonempty with (rfl | ht')
  · simp
  · simp [uniformOn_self ht ht']
  · simp [uniformOn_self hs hs']
  rw [uniformOn, uniformOn, uniformOn, cond_apply hs.measurableSet,
    cond_apply ht.measurableSet, cond_apply (hs.union ht).measurableSet,
    cond_apply (hs.union ht).measurableSet, cond_apply (hs.union ht).measurableSet]
  conv_lhs =>
    rw [Set.union_inter_cancel_left, Set.union_inter_cancel_right,
      mul_comm (Measure.count (s ∪ t))⁻¹, mul_comm (Measure.count (s ∪ t))⁻¹, ← mul_assoc,
      ← mul_assoc, mul_comm _ (Measure.count s), mul_comm _ (Measure.count t), ← mul_assoc,
      ← mul_assoc]
  rw [ENNReal.mul_inv_cancel, ENNReal.mul_inv_cancel, one_mul, one_mul, ← add_mul, ← measure_union,
    Set.union_inter_distrib_right, mul_comm]
  exacts [hst.mono inf_le_left inf_le_left, (ht.inter_of_left _).measurableSet,
    Measure.count_ne_zero ht', (Measure.count_apply_lt_top.2 ht).ne, Measure.count_ne_zero hs',
    (Measure.count_apply_lt_top.2 hs).ne]

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

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
⊢ eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
by
  rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]

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

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

Tactic:
have := Classical.choose_spec h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
this : const α b = mk (Function.const α (Classical.choose h)) ⋯
⊢ Function.const α (Classical.choose h) x = b
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ (mk ↑f ⋯).lintegral = f.lintegral

Tactic:
mk_coeFn

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α →ₘ[μ] ℝ≥0∞
⊢ f.lintegral = f.lintegral
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (fun x ↦ rexp (t * f x)) μ
⊢ AEMeasurable f μ

Tactic:
by
  simpa only [mul_div_cancel_left₀ _ ht]
    using (aemeasurable_of_aemeasurable_exp hf).fun_div (aemeasurable_const (b := t))

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

Goal state before:
pp: ⊢ 2⁻¹ + 2⁻¹ = 1⁻¹

Tactic:
← two_mul,

Goal state after:
⊢ 2 * 2⁻¹ = 1⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

Tactic:
← Measure.le_add_left le_rfl

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
μ ν : Measure α
p : ℝ≥0∞
⊢ eLpNorm f p ν ≤ eLpNorm f p ν
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x ↦ f x ^ p) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

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

Tactic:
rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero
  filter_upwards [hf_zero] with x
  rw [Pi.zero_apply, ← not_imp_not]
  exact fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x ↦ x ^ (n + n)

Tactic:
← two_mul,

Goal state after:
𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x ↦ x ^ (2 * n)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A * B, HasSum (fun i ↦ f i * g i) C

Tactic:
have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by
    rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]

Goal state after:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun i ↦ f i ^ p) (A ^ p)
hg : HasSum (fun i ↦ g i ^ q) (B ^ q)
H₁ : Summable fun i ↦ f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C ≤ A * B, HasSum (fun i ↦ f i * g i) C