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

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
⊢ (TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z) ∈
    ↑(ProperCone.dual (topDualPairing ℝ F) ↑(ProperCone.dual (topDualPairing ℝ F).flip ↑C₂))

Tactic:
intro f

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
f : F →L[ℝ] ℝ
⊢ f ∈ ↑(ProperCone.dual (topDualPairing ℝ F).flip ↑C₂) →
    0 ≤ ((topDualPairing ℝ F) f) ((TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z))
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
x : P
⊢ intrinsicFrontier 𝕜 {x} = ∅

Tactic:
intrinsicFrontier,

Goal state after:
𝕜 : 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
x : P
⊢ Subtype.val '' frontier (Subtype.val ⁻¹' {x}) = ∅
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: case inr
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
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty ↑F
⊢ (⋂ i, ↑i).Nonempty

Tactic:
refine IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun t u => ?_)
    (fun t => (hFS t.mem).1)
    (fun t => hscomp.of_isClosed_subset (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t =>
      (hFS t.mem).2.1

Goal state after:
case inr
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
hsnemp : s.Nonempty
S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x1 x2 ↦ x1 ⊆ x2) F
hFnemp : F.Nonempty
this : Nonempty ↑F
t u : ↑F
⊢ ∃ z, (fun x1 x2 ↦ x1 ⊇ x2) ↑t ↑z ∧ (fun x1 x2 ↦ x1 ⊇ x2) ↑u ↑z
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨
    ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ

Tactic:
refine or_iff_not_imp_right.mpr fun H => ?_

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ¬∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ)
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior s ∩ interior (B n)

Tactic:
isOpen_ball.interior_eq

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (↑n + 1)
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
intrinsicFrontier,

Goal state after:
case inr
𝕜 : 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 : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ Subtype.val '' frontier (Subtype.val ⁻¹' f '' s) = f '' intrinsicFrontier 𝕜 s
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
d : ℕ := finrank ℝ E
this✝ :
  ∀ (r : ℝ≥0), 1 < r → μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ↑(r ^ d) * μ (interior s)
this :
  ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ↑(r ^ d) * μ (interior s)
⊢ Tendsto (fun c ↦ ↑(c ^ d) * μ (interior s)) (𝓝[>] 1) (𝓝 (μ (interior s)))

Tactic:
refine (((ENNReal.continuous_mul_const hb).comp
    (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ ?_).mono_left nhdsWithin_le_nhds

Goal state after:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : μ (interior s) ≠ ∞
d : ℕ := finrank ℝ E
this✝ :
  ∀ (r : ℝ≥0), 1 < r → μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ↑(r ^ d) * μ (interior s)
this :
  ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤ ↑(r ^ d) * μ (interior s)
⊢ ((fun x ↦ x * μ (interior s)) ∘ ENNReal.ofNNReal ∘ fun a ↦ a ^ d) 1 = μ (interior s)
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁹ : PartialOrder R
inst✝⁸ : Semiring R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : ConvexSpace R M
inst✝⁵ : ConvexSpace R N
inst✝⁴ : ConvexSpace R P
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, w.weights x ≠ 0
hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ 0 ≤ (filter (fun x ↦ x ∈ s) w.weights).sum fun _x k ↦ k

Tactic:
exact restrict_nonneg_aux

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst✝⁹ : PartialOrder R
inst✝⁸ : Semiring R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : ConvexSpace R M
inst✝⁵ : ConvexSpace R N
inst✝⁴ : ConvexSpace R P
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, w.weights x ≠ 0
hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ 0 ≤ (filter (fun x ↦ x ∉ s) w.weights).sum fun _x k ↦ k

Tactic:
exact restrict_nonneg_aux

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case f
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
d : StdSimplex R P
| f.weights d • ((Finset.affineCombination R d.weights.support id) ⇑d.weights -ᵥ b)

Tactic:
rw [d.weights.support.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
        _ _ d.total b, vadd_vsub, Finset.weightedVSubOfPoint_apply]

Goal state after:
case f
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
d : StdSimplex R P
| f.weights d • ∑ i ∈ d.weights.support, (fun x r ↦ r) i (d.weights i) • (id i -ᵥ b)
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
S : Set (Set X)
hS : ∀ s ∈ S, IsStarConvexSet R x s
y : X
s : Set X
hs : s ∈ S
hy : y ∈ s
a ha : R
b : 0 ≤ a
hb : 0 ≤ ha
hab : a + ha = 1
⊢ convexCombPair a ha b hb hab x y ∈ ⋃₀ S

Tactic:
exact ⟨s, hs, hS _ hs hy _ ..⟩

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

Goal state before:
pp: case inr
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ |s' - s| * dist x y = |s - s'| * dist x y

pp: case inr.hss'
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ s ≤ s'

Tactic:
abs_sub_comm

Goal state after:
case inr
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ |s - s'| * dist x y = |s - s'| * dist x y

case inr.hss'
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
x y : X
this :
  ∀ {s t s' t' : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1),
    s' ≤ s → dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y
hss' : ¬s' ≤ s
⊢ s ≤ s'
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
⊢ p ∈ F ↑i

Tactic:
by_cases h : i ∈ I
    · exact this I h hp_Ic
    · apply this Iᶜ h; rwa [compl_compl]

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

Goal state before:
pp: case refine_1
𝕜 : 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
⊢ (s ∩ t).Nonempty

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:
· simpa [← coe_inter] using convexHull_nonempty_iff.1 (h.1.mono (K.inter_subset_convexHull hs ht))

Goal state after:
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)
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s

Tactic:
classical
  have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
  by_contra H
  rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t

Tactic:
refine ⟨fun hs' : ¬(_ ∧ _) => ?_, ?_⟩
  · push Not at hs'
    obtain ⟨t, ht⟩ := hs' hs
    exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
  · rintro ⟨t, ht⟩ ⟨hs, hs'⟩
    have := hs' ht.1 ht.2.1
    rw [this] at ht
    exact ht.2.2 (Subset.refl t)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
⊢ Fintype ↑⊥.edgeSet

Tactic:
by
  rw [edgeSet_bot]
  infer_instance

Goal state after:
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid A
inst✝¹ : Module 𝕜 A
inst✝ : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
⊢ C \ interior C ⊆ extremePoints 𝕜 C

Tactic:
by
  refine fun x hx ↦ ⟨hx.1, fun y hy z hz ⟨a, b, ha, hb, hab, hxab⟩ ↦ ?_⟩
  have hyz : y = z := by
    by_contra
    exact hx.2 <| hxab ▸ hc hy hz this ha hb hab
  rwa [← hyz, ← add_smul, hab, one_smul] at hxab

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

Goal state before:
pp: case mpr
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 : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ (∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y) → s.WSameSide x y

Tactic:
rintro ⟨t, ht, p', hp', rfl⟩
    exact wSameSide_smul_vsub_vadd_right x hp hp' ht

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

Goal state before:
pp: case h
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    ‖iteratedFDeriv ℝ n (fun x ↦ (B (f x)) (g x)) x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (fun a ↦ ↑(n.choose i) * (‖iteratedFDeriv ℝ i f a‖ * ‖iteratedFDeriv ℝ (n - i) g a‖)) =O[⊤] fun x ↦
    (1 + ‖x‖) ^ k1 * (1 + ‖x‖) ^ k2

Tactic:
refine .const_mul_left (.mul (h1 i ?_).norm_left (h2 (n - i) ?_).norm_left) _

Goal state after:
case h.refine_1
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    ‖iteratedFDeriv ℝ n (fun x ↦ (B (f x)) (g x)) x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n

case h.refine_2
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
hf : HasTemperateGrowth f
hg : HasTemperateGrowth g
n k1 : ℕ
h1 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k1
k2 : ℕ
h2 : ∀ n_1 ≤ n, iteratedFDeriv ℝ n_1 g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k2
estimate :
  ∀ (x : D),
    ‖iteratedFDeriv ℝ n (fun x ↦ (B (f x)) (g x)) x‖ ≤
      ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i f x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ≤ n
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
hk' : 0 < ↑n
⊢ (fderiv ℝ (⇑f) x) v = lineDeriv ℝ (⇑f) x v

Tactic:
(f.contDiff.differentiable hk'.ne').differentiableAt.lineDeriv_eq_fderiv

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
hk' : 0 < ↑n
⊢ (fderiv ℝ (⇑f) x) v = (fderiv ℝ (⇑f) x) v
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 : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
⊢ ‖T‖ = M

Tactic:
have hM x : |re ⟪T x, x⟫| ≤ M * ‖x‖ ^ 2 := by
    have hM : |T.rayleighQuotient x| ≤ M := le_ciSup T.bddAbove_rayleighQuotient x
    by_cases hx : 0 < ‖x‖ ^ 2
    · rwa [rayleighQuotient, abs_div, abs_sq, reApplyInnerSelf, div_le_iff₀ hx] at hM
    · simp_all

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
⊢ ‖T‖ = M