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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed (⋂ i ∈ s, ↑(dual p {i}))

Tactic:
dual_singleton

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : PartialOrder R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : ClosedIciTopology R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
hp : ∀ (x : M), Continuous ⇑(p x)
⊢ IsClosed (⋂ i ∈ s, ↑(comap (p i) (positive R R)))
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
⊢ dual p univ = ⊥

Tactic:
by
  refine le_antisymm (fun y hy ↦ (_root_.map_eq_zero_iff _ p.flip.toContPerfPair.injective).1 ?_)
    (by simp)
  ext x
  exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

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

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
x y : P
⊢ Wbtw R x (midpoint R x y) y

Tactic:
convert! wbtw_pointReflection R (midpoint R x y) x

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✝ : AddTorsor V P
x y : P
⊢ y = (pointReflection R (midpoint R x y)) x
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : LinearOrder R
inst✝⁸ : IsStrictOrderedRing R
G : Type u_2
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
H : Type u_3
inst✝⁵ : AddCommGroup H
inst✝⁴ : Module R H
G' : Type u_4
H' : Type u_5
inst✝³ : AddCommGroup G'
inst✝² : Module R G'
inst✝¹ : AddCommGroup H'
inst✝ : Module R H'
f : G →ₗ[R] G'
g : H →ₗ[R] H'
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
φ : Dual R G'
hφ : φ ∈ dual (Dual.eval R G') ↑(map f C₁)
ψ : Dual R H'
hψ : ψ ∈ dual (Dual.eval R H') ↑(map g C₂)
x : G
y : H
⊢ ((dualDistrib R G' H') (φ ⊗ₜ[R] ψ) ∘ₗ TensorProduct.map f g) (x ⊗ₜ[R] y) =
    ((dualDistrib R G H) ((φ ∘ₗ f) ⊗ₜ[R] (ψ ∘ₗ g))) (x ⊗ₜ[R] y)

Tactic:
by simp [map_tmul]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).toFun

Tactic:
by apply continuous_gaugeRescale <;> assumption

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ Continuous[inst✝³, inst✝³] (gaugeRescaleEquiv s t ⋯ hsb ⋯ htb).invFun

Tactic:
by apply continuous_gaugeRescale <;> assumption

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)

Tactic:
by
        have h := hf.2 hy' hz (by positivity) (by positivity) hab
        simp only [← hxyz, smul_eq_mul, a, b] at h
        field_simp at h
        linear_combination h

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

Goal state before:
pp: case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y ↦ 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f (2 • x₀ - y) ≤ |r|

Tactic:
exact hfr'.trans (le_abs_self _)

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (fun a ↦ ↑a) '' (closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) =
    intrinsicInterior 𝕜 s

Tactic:
rw [closure_sdiff_frontier, intrinsicInterior]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
⊢ x ∈ f ∘ Subtype.val ⁻¹' f '' s ↔ x ∈ Subtype.val ⁻¹' s

Tactic:
refine ⟨fun ⟨_, hy, hfy⟩ ↦ ?_ , fun hx ↦ ⟨_, hx, rfl⟩⟩

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
x : ↥(affineSpan 𝕜 s)
x✝ : x ∈ f ∘ Subtype.val ⁻¹' f '' s
w✝ : P
hy : w✝ ∈ s
hfy : f w✝ = (f ∘ Subtype.val) x
⊢ x ∈ Subtype.val ⁻¹' s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ _root_.affineSpan ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s) = ⊤

pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s)

Tactic:
AffineIsometryEquiv.coe_toHomeomorph,

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ _root_.affineSpan ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm ⁻¹' Subtype.val ⁻¹' s) = ⊤

V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' Subtype.val ⁻¹' s)
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
ι : Sort u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
s : ι → Set X
hs : ∀ (i : ι), IsStarConvexSet R x (s i)
⊢ IsStarConvexSet R x (⋂ i, s i)

Tactic:
simp +contextual [IsStarConvexSet, hs _ _]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ((convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t).Nonempty ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑(s ∩ t)

Tactic:
rw [coe_inter, convexHull_inter_convexHull hs ht]

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

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤ iConvexComb f fun x ↦ dist x.1 x.2

Tactic:
simp only [AddTorsor.iConvexComb_eq_affineCombination]

Goal state after:
I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
⊢ dist ((Finset.affineCombination ℝ f.weights.support Prod.fst) ⇑f.weights)
      ((Finset.affineCombination ℝ f.weights.support Prod.snd) ⇑f.weights) ≤
    iConvexComb f fun x ↦ dist x.1 x.2
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: case inr
ι : 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
⊢ (⋂ i, F i).Nonempty

Tactic:
have i0 : ι := Nonempty.some h_nonempty

Goal state after:
case inr
ι : 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, F i).Nonempty
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ 0

pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p

Tactic:
· simpa only [rpow_zero] using! concaveOn_const (c := 1) (convex_Ici _)

Goal state after:
case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ ConcaveOn ℝ (Ici 0) fun x ↦ x ^ p
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ Gᶜ.IsIsolated v ↔ G.IsUniversal v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simpa using isUniversal_compl_iff_isIsolated.mpr h
  · exact isUniversal_compl_iff_isIsolated.mp (by simpa)

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 c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c

Tactic:
← ne_iff_lt_iff_le.mpr (dist_triangle _ _ _),

Goal state after:
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 c ≠ dist a b + dist b c ↔ ¬Wbtw ℝ a b c
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
⊢ dist x y + dist y z = dist x z

Tactic:
hxy,

Goal state after:
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
⊢ r * dist x z + dist y z = dist x z
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case inr
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left✝¹ : 0 ≤ a
hb : 0 ≤ b
left✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b * dist x z = dist x y
⊢ y = (AffineMap.lineMap x z) r

Tactic:
hxy,

Goal state after:
case inr
E : Type u_3
PE : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : StrictConvexSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left✝¹ : 0 ≤ a
hb : 0 ≤ b
left✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b * dist x z = r * dist x z
⊢ y = (AffineMap.lineMap x z) r
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: R : Type u_1
V : Type u_2
ι : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : TopologicalSpace V
inst✝¹ : AddCommGroup V
inst✝ : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi✝¹ : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
hi✝ : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι), i'' ∈ t → j'' ∈ t → z i'' ≠ z j'' → w i'' ≠ 0 → w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
hi : i = i' ∨ i = j'
⊢ t.centerMass w z = z i''

Tactic:
rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]

Goal state after:
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 z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ht : t ≠ 1
hy' : z -ᵥ x ∈ s.direction
⊢ x ∈ s

Tactic:
vadd_mem_iff_mem_of_mem_direction (Submodule.smul_mem _ _ hy')

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✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∉ s
hz : z ∈ s
t : R
ht0 : 0 ≤ t
ht1 : t ≤ 1
hy : x ∈ s
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ht : t ≠ 1
hy' : z -ᵥ x ∈ s.direction
⊢ x ∈ s
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 μ)
x : α
hx : ↑(↑f₁ + ↑f₂) x = (↑↑f₁ + ↑↑f₂) x
⊢ (B (↑↑(f₁ + f₂) x)) (↑↑g x) = ((fun x ↦ (B (↑↑f₁ x)) (↑↑g x)) + fun x ↦ (B (↑↑f₂ x)) (↑↑g x)) x

Tactic:
simp [hx]

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 : ↥(Lp E p μ)
g₁ g₂ : ↥(Lp F q μ)
x : α
hx : ↑(↑g₁ + ↑g₂) x = (↑↑g₁ + ↑↑g₂) x
⊢ (B (↑↑f x)) (↑↑(g₁ + g₂) x) = ((fun x ↦ (B (↑↑f x)) (↑↑g₁ x)) + fun x ↦ (B (↑↑f x)) (↑↑g₂ x)) x

Tactic:
simp [hx]

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
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
x : α
hx : ↑↑(c • f) x = (c • ↑↑f) x
⊢ (B (↑↑(c • f) x)) (↑↑g x) = (c • fun x ↦ (B (↑↑f x)) (↑↑g x)) x

Tactic:
simp [hx]

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
c : 𝕜
f : ↥(Lp E p μ)
g : ↥(Lp F q μ)
x : α
hx : ↑↑(c • g) x = (c • ↑↑g) x
⊢ (B (↑↑f x)) (↑↑(c • g) x) = (c • fun x ↦ (B (↑↑f x)) (↑↑g x)) x

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : g =ᵐ[volume.restrict (Ioi 0)] 0
A : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ (fun t ↦ μ {a | t ≤ f a} * ENNReal.ofReal (g t)) =ᵐ[volume.restrict (Ioi 0)] 0

Tactic:
filter_upwards [H1] with t ht using by simp [ht]

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

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
⊢ iteratedFDeriv ℝ n (f + g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ max k₁ k₂

Tactic:
iteratedFDeriv_add (hf.1.of_le <| mod_cast le_top) (hg.1.of_le <| mod_cast le_top)

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
⊢ (iteratedFDeriv ℝ n f + iteratedFDeriv ℝ n g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ max k₁ k₂
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r

Tactic:
set t := {y : ℝ | 1 / 2 < y}

Goal state after:
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
⊢ HasTemperateGrowth fun x ↦ (1 + ‖x‖ ^ 2) ^ r
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
simp [hx]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
t : ℝ
ht : 0 < t
hT' : (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T
hT0 : ¬T = 0
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖((algebraMap 𝕜 (E →L[𝕜] E)) ((algebraMap ℝ 𝕜) t) - T) x‖
x : E
hx : x = 0
⊢ T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - min (c ^ 2 / (2 * t)) ((t ^ 2 + ‖T‖ ^ 2) / (2 * t))

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs

Goal state before:
pp: case inr
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
B : Matrix n n R
inst✝ : IsDomain R
hAps : B.charpoly.Splits
h✝ : Nonempty n
⊢ B.trace = B.charpoly.roots.sum

Tactic:
· rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg,
      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic B.charpoly_monic]

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
⊢ (spectrum ℝ A).Finite

Tactic:
rw [← spectrum.preimage_algebraMap 𝕜]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
⊢ (⇑(algebraMap ℝ 𝕜) ⁻¹' spectrum 𝕜 A).Finite
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
⊢ A.rank = (diagonal hA.eigenvalues).rank

Tactic:
by
  conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]
  simp [-isUnit_iff_ne_zero, -coe_star, rank_diagonal]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ ⟪((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩, ((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩⟫ = 0

Tactic:
have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : (starRingEnd 𝕜) μ = μ
⊢ ⟪((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) μ) ⟨v, hv⟩, ((fun μ ↦ (eigenspace T μ).subtypeₗᵢ) ν) ⟨w, hw⟩⟫ = 0