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

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure ((convexHull ℝ) (extremePoints ℝ s)) = s

Tactic:
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
  by_contra hs
  obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
  obtain ⟨l, r, hlr, hrx⟩ :=
    geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
  have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩
  obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn
  obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩
  linarith [hlr _ (subset_closure <| subset_convexHull _ _ <|
    h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA]

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
hc : x ∉ affineSpan 𝕜 s
⊢ False

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h _ (affineSpan 𝕜 s).closed_of_finiteDimensional.isOpen_compl hc

Goal state after:
case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
hc : x ∉ affineSpan 𝕜 s
z : P
hz₁ : z ∈ (↑(affineSpan 𝕜 s))ᶜ
hz₂ : z ∈ s
⊢ False
Module: Mathlib.Geometry.Convex.ConvexSpace.Prod

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
⊢ ι →₀ X

Tactic:
refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_

Goal state after:
I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
⊢ ∀ (a : ι), (iConvexComb w fun x ↦ x a) ≠ 0 → a ∈ w.weights.support.biUnion support
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
⊢ ∀ (v : ι), {v} ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
by
    simp only [Set.mem_union, Set.mem_ofPred_eq, Set.mem_image]
    intro v
    exact Or.inl ⟨v, rfl⟩

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

Goal state before:
pp: case htc
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ ∀ (i : ι), IsClosed (F i)

pp: case inr.hst
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ ∀ (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty

Tactic:
· intro i
    exact (h_compact i).isClosed

Goal state after:
case inr.hst
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
h_fin : ∀ (I : Finset ι), (⋂ i ∈ I, F i).Nonempty
i0 : ι
⊢ ∀ (u : Finset ι), (F i0 ∩ ⋂ i ∈ u, F i).Nonempty
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ s.WOppSide x x ↔ x ∈ s

Tactic:
by
  constructor
  · rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
    obtain ⟨a, -, -, -, -, h₁, -⟩ := h.exists_eq_smul_add
    rw [add_comm, vsub_add_vsub_cancel, ← eq_vadd_iff_vsub_eq] at h₁
    rw [h₁]
    exact s.smul_vsub_vadd_mem a hp₂ hp₁ hp₁
  · exact fun h => ⟨x, h, x, h, SameRay.rfl⟩

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

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : 0 ≤ 0
habv : 0 + bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u (0 • y + bv • q), x_1 ∈ (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
rw [zero_add] at habv
    rw [zero_smul, zero_add, habv, one_smul]
    exact ⟨q, right_mem_segment _ _ _, subset_convexHull _ _ <| by simp⟩

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
by
  have :
      dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
        b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
    simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
      eq_comm]
  simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image]
    at this
  rwa [(vsub_left_injective _).mem_set_image] at this

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ MemLp.toLp (fun x ↦ (B (↑↑(f₁ + f₂) x)) (↑↑g x)) ⋯ =
    MemLp.toLp ((fun x ↦ (B (↑↑f₁ x)) (↑↑g x)) + fun x ↦ (B (↑↑f₂ x)) (↑↑g x)) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f₁ f₂ : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (fun x ↦ (B (↑↑(f₁ + f₂) x)) (↑↑g x)) =ᵐ[μ] (fun x ↦ (B (↑↑f₁ x)) (↑↑g x)) + fun x ↦ (B (↑↑f₂ x)) (↑↑g x)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
⊢ MemLp.toLp (fun x ↦ (B (↑↑f x)) (↑↑(g₁ + g₂) x)) ⋯ =
    MemLp.toLp ((fun x ↦ (B (↑↑f x)) (↑↑g₁ x)) + fun x ↦ (B (↑↑f x)) (↑↑g₂ x)) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
⊢ (fun x ↦ (B (↑↑f x)) (↑↑(g₁ + g₂) x)) =ᵐ[μ] (fun x ↦ (B (↑↑f x)) (↑↑g₁ x)) + fun x ↦ (B (↑↑f x)) (↑↑g₂ x)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ MemLp.toLp (fun x ↦ (B (↑↑(c • f) x)) (↑↑g x)) ⋯ = MemLp.toLp (c • fun x ↦ (B (↑↑f x)) (↑↑g x)) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (fun x ↦ (B (↑↑(c • f) x)) (↑↑g x)) =ᵐ[μ] c • fun x ↦ (B (↑↑f x)) (↑↑g x)
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
      ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
    SignType.sign (w₁ i) = SignType.sign (w₂ i) ∧ w₁ i ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hs, h0⟩ ↦ s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0⟩

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
h :
  (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
⊢ SignType.sign (w₁ i) = SignType.sign (w₂ i) ∧ w₁ i ≠ 0
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ MemLp.toLp (fun x ↦ (B (↑↑f x)) (↑↑(c • g) x)) ⋯ = MemLp.toLp (c • fun x ↦ (B (↑↑f x)) (↑↑g x)) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
⊢ (fun x ↦ (B (↑↑f x)) (↑↑(c • g) x)) =ᵐ[μ] c • fun x ↦ (B (↑↑f x)) (↑↑g x)
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ MemLp.toLp (↑↑(f₁ + f₂) • ↑↑g) ⋯ = MemLp.toLp (↑↑f₁ • ↑↑g + ↑↑f₂ • ↑↑g) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f₁ f₂ : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ ↑↑(f₁ + f₂) • ↑↑g =ᵐ[μ] ↑↑f₁ • ↑↑g + ↑↑f₂ • ↑↑g
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : IsScalarTower 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ MemLp.toLp (↑↑(c • f) • ↑↑g) ⋯ = MemLp.toLp (c • ↑↑f • ↑↑g) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : IsScalarTower 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ ↑↑(c • f) • ↑↑g =ᵐ[μ] c • ↑↑f • ↑↑g
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ MemLp.toLp (c • ↑↑f • ↑↑g) ⋯ = MemLp.toLp (↑↑f • ↑↑(c • g)) ⋯

Tactic:
apply MemLp.toLp_congr

Goal state after:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝⁹ : NormedRing 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : IsBoundedSMul 𝕜 E
inst✝⁵ : NormedRing 𝕜'
inst✝⁴ : Module 𝕜' E
inst✝³ : Module 𝕜' 𝕜
inst✝² : IsBoundedSMul 𝕜' E
inst✝¹ : IsBoundedSMul 𝕜' 𝕜
inst✝ : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ c • ↑↑f • ↑↑g =ᵐ[μ] ↑↑f • ↑↑(c • g)
Module: Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂✝ : Type u_2
𝕜₃✝ : Type u_3
inst✝³⁹ : NormedField 𝕜₁
inst✝³⁸ : NormedField 𝕜₂✝
inst✝³⁷ : NormedField 𝕜₃✝
σ : 𝕜₁ →+* 𝕜₂✝
τ : 𝕜₂✝ →+* 𝕜₃✝
ρ : 𝕜₁ →+* 𝕜₃✝
inst✝³⁶ : RingHomCompTriple σ τ ρ
E✝ : Type u_4
F✝ : Type u_5
G✝ : Type u_6
inst✝³⁵ : AddCommGroup E✝
inst✝³⁴ : Module 𝕜₁ E✝
inst✝³³ : AddCommGroup F✝
inst✝³² : Module 𝕜₂✝ F✝
inst✝³¹ : AddCommGroup G✝
inst✝³⁰ : Module 𝕜₃✝ G✝
𝕜 : Type u_7
𝕜₂ : Type u_8
𝕜₃ : Type u_9
𝕜₄ : Type u_10
E : Type u_11
F : Type u_12
G : Type u_13
H : Type u_14
inst✝²⁹ : AddCommGroup E
inst✝²⁸ : AddCommGroup F
inst✝²⁷ : AddCommGroup G
inst✝²⁶ : AddCommGroup H
inst✝²⁵ : NormedField 𝕜
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
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
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁷ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁶ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁵ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁴ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
s : Set F
⊢ s ∈ {S | IsCompact S} ↔ ⇑e₁₂ ⁻¹' s ∈ {S | IsCompact S}

Tactic:
simp [← e₁₂.toHomeomorph.isCompact_preimage]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

Tactic:
rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀] <;> positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)

Tactic:
gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ HasTemperateGrowth _root_.id

Tactic:
apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1)

Goal state after:
case h'f
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ HasTemperateGrowth (fderiv ℝ _root_.id)

case hf
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Differentiable ℝ _root_.id

case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : E), ‖_root_.id x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
x : E
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * (1 + ‖x‖) ^ 1

Tactic:
by simp [mul_add]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⋯
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4 ≤ M

Tactic:
rw [parallelogram_law_with_norm 𝕜 x y, hx, hy]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ M * (2 * (1 ^ 2 + 1 ^ 2)) / 4 ≤ M
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (‖T‖ ^ 2 + ‖T‖ ^ 2) / (2 * ‖T‖) - ε
⊢ ∃ ε > 0, ∀ (x : E), T.rayleighQuotient x ≤ ‖T‖ - ε

Tactic:
refine ⟨ε, hε0, fun x ↦ ?_⟩

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
ε : ℝ
hε0 : ε > 0
hε : ∀ (x : E), T.rayleighQuotient x ≤ (‖T‖ ^ 2 + ‖T‖ ^ 2) / (2 * ‖T‖) - ε
x : E
⊢ T.rayleighQuotient x ≤ ‖T‖ - ε
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i j : n
⊢ (↑(hA.eigenvalues i) • PiLp.single 2 i 1).ofLp j = (PiLp.single 2 i ↑(hA.eigenvalues i)).ofLp j

Tactic:
simp only [PiLp.smul_apply, PiLp.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]

Goal state after:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ hA.eigenvalues = 0 ↔ A = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by ext; simp [h, eigenvalues_eq]⟩
  rw [hA.spectral_theorem, h, Pi.comp_zero, RCLike.ofReal_zero, Function.const_zero,
    Pi.zero_def, diagonal_zero, map_zero]

Goal state after:
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0

Tactic:
rw [← diagonal_zero] at h2

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
h2 : diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩) = diagonal fun x ↦ 0
i : n
hx : hA.eigenvalues i ∈ spectrum ℝ A
⊢ f ⟨hA.eigenvalues i, hx⟩ = 0
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * (A ⊙ B) i j * xj

Tactic:
have hAB : ((A ⊙ B).submatrix (↑) (↑) : Matrix x.support _ _).PosSemidef := by
    have hAs := hA.submatrix ((↑) : x.support → ι)
    have hBs := hB.submatrix ((↑) : x.support → ι)
    rw [submatrix_hadamard, posSemidef_iff_dotProduct_mulVec]
    refine ⟨hAs.isHermitian.hadamard hBs.isHermitian, fun y ↦ ?_⟩
    rw [star_dotProduct_hadamard_mulVec_eq_kronecker]
    exact (hAs.kronecker hBs).dotProduct_mulVec_nonneg _

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAB : ((A ⊙ B).submatrix Subtype.val Subtype.val).PosSemidef
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * (A ⊙ B) i j * xj
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : M.PosSemidef
⊢ ∀ (x y z : Matrix n n 𝕜), (z * M * (x + y)ᴴ).trace = (z * M * xᴴ).trace + (z * M * yᴴ).trace

Tactic:
by simp [mul_add]

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : IsSelfAdjoint A
⊢ Isometry ⇑(cfcHom hA)

Tactic:
rw [← isHermitian_iff_isSelfAdjoint] at hA

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
⊢ Isometry ⇑(cfcHom hA✝)