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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
⊢ ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t

Tactic:
rcases hs₂.elim_finite_subcover_image (b := s)
      (c := fun x => interior (convexHull ℝ (Set.range b)) + {x})
      (fun _ _ => isOpen_interior.add_right)
      (fun x hx => Set.mem_iUnion₂_of_mem hx <| by simpa using hb₁)
    with ⟨u, hu₁, hu₂, hu₃⟩

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Set E
hu₁ : u ⊆ s
hu₂ : u.Finite
hu₃ : s ⊆ ⋃ i ∈ u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ ∃ u, s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t
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 α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᵐ[μ] g
this : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
x : α
hx : g x ∈ s
⊢ g x ∈ range g ∩ s

Tactic:
exact ⟨mem_range_self _, hx⟩

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
x : P
⊢ intrinsicInterior 𝕜 {x} = {x}

Tactic:
simp only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ,
    Subtype.range_coe_subtype, mem_affineSpan_singleton, ofPred_eq_eq_singleton]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
w : StdSimplex R M
⊢ iConvexComb w id = sConvexComb w

Tactic:
by
  simp [iConvexComb]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x : M
⊢ convexCombPair s t hs ht h x x = x

Tactic:
unfold convexCombPair
  convert sConvexComb_single x
  simp only [StdSimplex.duple, StdSimplex.single, ← single_add, h]

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

Goal state before:
pp: case neg
𝕜 : 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
h : i ∉ I
⊢ p ∈ F ↑i

Tactic:
apply this Iᶜ h; rwa [compl_compl]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
f : M → N
hf : IsAffineMap R f
w : StdSimplex R M
⊢ (-f) (sConvexComb w) = sConvexComb (StdSimplex.map (-f) w)

Tactic:
simp [hf.map_sum_weights, Finsupp.sum_mapDomain_index, add_smul]

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 t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨
    ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u

Tactic:
by_contra! h

Goal state after:
𝕜 : 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 :
  ¬Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∧
    ∀ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ≠ (convexHull 𝕜) ↑u
⊢ False
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.SSameSide x y ↔ s.SSameSide y x

Tactic:
rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]

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
inst✝ : DecidableEq V
v : V
x✝ : ↑(G.neighborSet v)
w : V
hw : w ∈ G.neighborSet v
⊢ (fun e ↦ ⟨G.otherVertexOfIncident ⋯, ⋯⟩) ((fun w ↦ ⟨s(v, ↑w), ⋯⟩) ⟨w, hw⟩) = ⟨w, hw⟩

Tactic:
simp only [Subtype.mk.injEq]

Goal state after:
ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v✝ w✝ : V
e : Sym2 V
inst✝ : DecidableEq V
v : V
x✝ : ↑(G.neighborSet v)
w : V
hw : w ∈ G.neighborSet v
⊢ G.otherVertexOfIncident ⋯ = w
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hy : y ∈ s
⊢ s.WOppSide x z

Tactic:
by
  rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
  refine ⟨_, hy, _, hy, ?_⟩
  rcases ht1.lt_or_eq with (ht1' | rfl); swap
  · simp
  rcases ht0.lt_or_eq with (ht0' | rfl); swap
  · simp
  refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)
  rw [lineMap_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← neg_vsub_eq_vsub_rev z, vsub_self]
  module

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 y p₁ : P
h : p₁ ∈ s
⊢ s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
constructor
  · rintro ⟨p₁', hp₁', p₂', hp₂', h0 | h0 | ⟨r₁, r₂, hr₁, hr₂, hr⟩⟩
    · rw [vsub_eq_zero_iff_eq] at h0
      rw [h0]
      exact Or.inl hp₁'
    · refine Or.inr ⟨p₂', hp₂', ?_⟩
      rw [h0]
      exact SameRay.zero_right _
    · refine Or.inr ⟨(r₁ / r₂) • (p₁ -ᵥ p₁') +ᵥ p₂', s.smul_vsub_vadd_mem _ h hp₁' hp₂',
        Or.inr (Or.inr ⟨r₁, r₂, hr₁, hr₂, ?_⟩)⟩
      rw [vsub_vadd_eq_vsub_sub, smul_sub, ← hr, smul_smul, mul_div_cancel₀ _ hr₂.ne.symm,
        ← smul_sub, vsub_sub_vsub_cancel_right]
  · rintro (h' | ⟨h₁, h₂, h₃⟩)
    · exact wSameSide_of_left_mem y h'
    · exact ⟨p₁, h, h₁, h₂, h₃⟩

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 y p₂ : P
h : p₂ ∈ s
⊢ s.SSameSide y x ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
sSameSide_iff_exists_left h,

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 y p₂ : P
h : p₂ ∈ s
⊢ (y ∉ s ∧ x ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔
    x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
⊢ ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty

Tactic:
by_contra! h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅
⊢ False
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
⊢ x ∈ s

Tactic:
have hy' := vsub_mem_direction hy hz

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 : t • (z -ᵥ x) +ᵥ x ∈ s
hyx : (lineMap x z) t ≠ x
hyz : (lineMap x z) t ≠ z
ht : t ≠ 1
hy' : (t • (z -ᵥ x) +ᵥ x) -ᵥ z ∈ s.direction
⊢ x ∈ s
Module: Mathlib.Analysis.Convex.Visible

Goal state before:
pp: V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed[inst✝²] s
hy : y ∈ s
x : V
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
by
  let t : Set ℝ := Ici 0 ∩ lineMap x y ⁻¹' s
  have ht₁ : 1 ∈ t := by simpa [t]
  have ht : BddBelow t := bddBelow_Ici.inter_of_left
  let δ : ℝ := sInf t
  have hδ₁ : δ ≤ 1 := csInf_le ht ht₁
  obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
    (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht
  refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩
  rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, -, h⟩
  replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h
  replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
  rw [lineMap_lineMap_right] at hε
  exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_gt <| mul_lt_of_lt_one_left hδ₀ hε₁

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

Goal state before:
pp: case inr.inl
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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
h' : w₁ i < 0
⊢ False

Tactic:
rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at hs

Goal state after:
case inr.inl
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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs : 0 < w₂ i
h' : w₁ i < 0
⊢ False
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_2.inl
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)
x✝ : SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
hs : SignType.sign (w₁ i) = -SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h' : w₁ i < 0
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at hs

Goal state after:
case refine_2.inl
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)
x✝ : SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
hs : 0 < w₂ i
h0 : w₁ i ≠ 0
h' : w₁ i < 0
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)
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
s : ℝ
s_pos : s > 0
hs : 0 < ∫ (x : ℝ) in Ioc 0 s, g x ∂volume
h's : μ {a | s < f a} = ∞
A : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) = ∞
⊢ ∞ = ∫⁻ (x : α) in {a | s < f a}, ENNReal.ofReal (∫ (t : ℝ) in 0..s, g t) ∂μ

Tactic:
by
          simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            h's]
          rw [ENNReal.mul_top]
          simpa [intervalIntegral.integral_of_le s_pos.le] using hs

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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := ⋯
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := ⋯
u : ℕ → ℝ
uM : ∀ (n : ℕ), M < u n
ulim : Tendsto u atTop (𝓝 M)
n : ℕ
I : ν {a | f a ≤ M} = 0
J : μ {a | u n < f a} < ∞
⊢ ν {a | u n < f a} ≤ μ {a | u n < f a}

Tactic:
exact restrict_le_self _

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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
s : α
hs : s ∈ {a | M < f a}ᶜ
⊢ ∫ (t : ℝ) in 0..f s, g t = ∫ (t : ℝ) in 0..f s, 0

Tactic:
intervalIntegral.integral_of_le (f_nonneg s)

Goal state after:
α : 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
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
s : α
hs : s ∈ {a | M < f a}ᶜ
⊢ ∫ (t : ℝ) in Ioc 0 (f s), g t ∂volume = ∫ (t : ℝ) in Ioc 0 (f s), 0 ∂volume
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 → F
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (-f)

Tactic:
by
  refine ⟨hf.1.neg, fun n ↦ ?_⟩
  obtain ⟨k, C, h⟩ := hf.2 n
  exact ⟨k, C, fun x ↦ by simpa [iteratedFDeriv_neg_apply] using h x⟩

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)
  · convert Function.HasTemperateGrowth.const (ContinuousLinearMap.id ℝ E)
    exact fderiv_fun_id
  · apply differentiable_id
  · simp

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
f_bdd : f ≤ᵐ[μ] fun x ↦ M
⊢ ∫ (t : ℝ) in Ioi 0, μ.real {a | t ≤ f a} = ∫ (t : ℝ) in Ioc 0 M, μ.real {a | t ≤ f a}

Tactic:
setIntegral_eq_of_subset_of_ae_sdiff_eq_zero
      nullMeasurableSet_Ioi Ioc_subset_Ioi_self ?_

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
f_bdd : f ≤ᵐ[μ] fun x ↦ M
⊢ ∫ (x : ℝ) in Ioc 0 ?m.75, μ.real {a | x ≤ f a} = ∫ (t : ℝ) in Ioc 0 M, μ.real {a | t ≤ f a}

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
f_bdd : f ≤ᵐ[μ] fun x ↦ M
⊢ ℝ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
f_bdd : f ≤ᵐ[μ] fun x ↦ M
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 ?m.75 → μ.real {a | x ≤ f a} = 0
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
inst✝ : CompleteSpace E
hT : IsSelfAdjoint T
a✝ : Nontrivial E
⊢ (algebraMap ℝ 𝕜) ‖T‖ ∉ resolventSet 𝕜 T ∨ -(algebraMap ℝ 𝕜) ‖T‖ ∉ resolventSet 𝕜 T

Tactic:
by_contra! h

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsSelfAdjoint T
a✝ : Nontrivial E
h : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T ∧ -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
⊢ False
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j

Tactic:
rw [eq_sort_iff']

Goal state after:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f)) ↔
    Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
⊢ False

Tactic:
have hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖ := by
    have : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖ := by grind [symm_def, norm_sub_rev]
    apply Pairwise.of_lt
    intro m n hmn
    let u : X := μ⁻¹ • (S (f n) - S (f m) + μ • f n)
    have hu : μ • (f m - u) = T (f m) - T (f n) := by
      rw [smul_sub, smul_inv_smul₀ hμ]
      simp [S]
      linear_combination (norm := module)
    have : u ∈ ((S : End 𝕜 X) ^ (m + 1)).range := by
      apply Submodule.smul_mem _ _ (Submodule.add_mem _ _ _)
      · exact Submodule.sub_mem _ (hf_mem' hmn.le) (hf_mem' le_rfl)
      · exact Submodule.smul_mem _ μ (hf_mem hmn)
    grw [← hu, norm_smul, mul_comm, ← hf_far _ u this, one_mul]

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
hp : Pairwise fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
⊢ False
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ ∀ i ∈ Finset.univ, 0 ≤ (RCLike.ofReal ∘ ⋯.eigenvalues) i

Tactic:
by simp [hA.eigenvalues_nonneg]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
⊢ x = 0

Tactic:
by_contra! h

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
h : x ≠ 0
⊢ False
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
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
μ : 𝕜
hμ : ¬HasEigenvalue T μ
⊢ {i | ↑(hT.unsortedEigenvalues hn i) = μ}.card = finrank 𝕜 ↥(eigenspace T μ)

Tactic:
· rw [Module.End.hasEigenvalue_iff.not_left.mp hμ, finrank_bot, Finset.card_filter_eq_zero_iff]
    intro i _ rfl
    exact hμ (hT.hasEigenvalue_unsortedEigenvalues hn i)

Goal state after: