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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
⊢ ∃ y, (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑C ∧ ⟪b, y⟫_ℝ < 0

Tactic:
refine ⟨y, fun x hx ↦ ?_, hyb⟩

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
C : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f C
y : F
hxy : ∀ x ∈ map f C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪b, y⟫_ℝ < 0
x : E
hx : x ∈ ↑C
⊢ 0 ≤ ((innerₗ E) x) ((ContinuousLinearMap.adjoint f) y)
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
x : E
hx : x ∈ C
⊢ 0 ≤ f x

Tactic:
by_contra! hx₀

Goal state after:
case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀✝ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
x : E
hx : x ∈ C
hx₀ : f x < 0
⊢ False
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

Tactic:
have hcnorm : range c ⊆ closedBall 0 (cnorm + 1) := by
    simpa only [cnorm, subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right,
      ← sub_le_iff_le_add, Finset.le_sup'_iff, forall_mem_range] using fun i ↦ ⟨i, by simp⟩

Goal state after:
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
inst✝³ : NormedSpace ℝ E✝
s✝ : Set E✝
x : E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : s ∈ 𝓝 0
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.centroid ℝ Finset.univ ⇑b +ᵥ b
hc₀ : 0 ∈ interior ((convexHull ℝ) (range ⇑c))
cnorm : ℝ := Finset.univ.sup' ⋯ fun i ↦ ‖c i‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' ⋯ • c
hε₀ : 0 < ε / 2
hdnorm : range ⇑d ⊆ closedBall 0 (ε / 2)
⊢ 0 ∈ interior ((convexHull ℝ) (range ⇑d))

Tactic:
simpa [d, Pi.smul_def, range_smul, interior_smul₀, convexHull_smul, zero_mem_smul_set_iff,
      hε'.ne']

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 / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ |f x - f y| ≤ K * ‖x - y‖

Tactic:
abs_sub_le_iff

Goal state after:
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 / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ f x - f y ≤ K * ‖x - y‖ ∧ f y - f x ≤ K * ‖x - y‖
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u)

Tactic:
← convexJoin_assoc,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 t s) u
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Tactic:
← convexJoin_assoc,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s t) u) v = convexJoin 𝕜 (convexJoin 𝕜 (convexJoin 𝕜 s u) t) v
Module: Mathlib.Analysis.Convex.KreinMilman

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ ⇑f '' s ∧ ∀ x₁ ∈ ⇑f '' s, ∀ x₂ ∈ ⇑f '' s, f x ∈ openSegment ℝ x₁ x₂ → x₁ = f x ∧ x₂ = f x
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a ↦ f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ f x ∈ openSegment ℝ (f y) (f z)

Tactic:
by
    rw [← this]; exact mem_image_of_mem _ hxyz

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ioc y z) f

Tactic:
· exact hf_cvx.subset Ioc_subset_Icc_self (convex_Ioc y z)

Goal state after:
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 α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ∞
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ∞)
⊢ f =ᵐ[μ.restrict t] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < μ.real t * C

Tactic:
rw [← measureReal_restrict_apply_univ]

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ∞
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ∞)
⊢ f =ᵐ[μ.restrict t] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < (μ.restrict t).real univ * C
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case inr.right
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
⊢ b ⊆ e.toFinset → b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
hb_sub

Goal state after:
case inr.right
ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ⊆ e.toFinset
⊢ b.Nonempty → b ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
a b : V
f : ι → SimpleGraph V
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
simp [iSup]

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

Goal state before:
pp: ι : 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_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
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
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty

Tactic:
have hJ : ∃ J : Finset ι, I ⊆ J ∧ #J = finrank 𝕜 E + 1 := by
    by_cases h : Infinite ι
    · exact Infinite.exists_superset_card_eq _ _ hI_card
    · have : Finite ι := Finite.of_not_infinite h
      have : Fintype ι := Fintype.ofFinite ι
      apply exists_superset_card_eq hI_card
      simp only [ENat.card_eq_coe_fintype_card] at h_card
      rwa [← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at h_card

Goal state after:
ι : 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_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
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
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
hJ : ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
⊢ (⋂ i ∈ I, F i).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s : Set (SimpleGraph V)
⊢ (sSup s).edgeSet = ⋃₀ (edgeSet '' s)

Tactic:
by
  ext ⟨x, y⟩
  simp

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

Goal state before:
pp: V : Type u
ι : Sort u_2
f : ι → SimpleGraph V
⊢ (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet

Tactic:
by
  ext ⟨x, y⟩
  simp

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).WSameSide (f x) (f y) ↔ s.WSameSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
h : (map f s).WSameSide (f x) (f y)
⊢ s.WSameSide x y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.edgeSet = ∅ ↔ G = ⊥

Tactic:
by rw [← edgeSet_bot, edgeSet_inj]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).WOppSide (f x) (f y) ↔ s.WOppSide x y

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : PartialOrder R
inst✝⁶ : IsStrictOrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
h : (map f s).WOppSide (f x) (f y)
⊢ s.WOppSide x y
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:
edgeSet_bot

Goal state after:
ι : 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 ↑∅
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint s G.edgeSet

Tactic:
disjoint_fromEdgeSet,

Goal state after:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet s ↔ Disjoint s G.edgeSet
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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ y) x ↔ s.WSameSide x y

Tactic:
wSameSide_vadd_left_iff hv,

Goal state after:
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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide y x ↔ s.WSameSide x y
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e' ↔ e' = e

Tactic:
refine ⟨fun h' => ?_, ?_⟩

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e

case refine_2
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ G.edgeSet ∧ v ∈ e') ∧ e' ∈ G.edgeSet ∧ Sym2.Mem.other h ∈ e'
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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide (v +ᵥ x) y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s

Tactic:
wSameSide_vadd_left_iff hv,

Goal state after:
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
v : V
hv : v ∈ s.direction
⊢ s.WSameSide x y ∧ v +ᵥ x ∉ s ∧ y ∉ s ↔ s.WSameSide x y ∧ x ∉ s ∧ y ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : w ∈ Gᶜ.neighborSet v
⊢ w ∈ ∅

Tactic:
rw [mem_neighborSet, compl_adj] at h'

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
h : w ∈ G.neighborSet v
h' : v ≠ w ∧ ¬G.Adj v w
⊢ 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✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ p₂ : P
m : V
c₁ c₂ : R
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h₁ : x -ᵥ p₁ = c₁ • m
h₂ : y -ᵥ p₂ = c₂ • m
hc : c₁ * c₂ ≤ 0
⊢ s.WOppSide x y

Tactic:
by
  refine ⟨p₁, hp₁, p₂, hp₂, ?_⟩
  have h₂' : p₂ -ᵥ y = (-c₂) • m := by rw [← neg_vsub_eq_vsub_rev, h₂, neg_smul]
  rw [h₁, h₂']
  exact sameRay_smul_smul_of_mul_nonneg (by rw [mul_neg]; exact neg_nonneg.2 hc)

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

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

Tactic:
zero_smul,

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, 0 + bz • y}
Module: Mathlib.Analysis.Convex.StoneSeparation

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

Tactic:
rw [zero_smul, zero_add, habz, one_smul]

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x ∈ segment 𝕜 u v, x ∈ (convexHull 𝕜) {p, q, y}
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 : bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u (0 • y + bv • q), x_1 ∈ (convexHull 𝕜) {p, q, az • x + bz • y}

Tactic:
zero_smul,

Goal state after:
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 : bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u (0 + bv • q), x_1 ∈ (convexHull 𝕜) {p, q, az • x + bz • y}
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: case neg
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
⊢ (insert i t).centerMass w z ∈ interior s

Tactic:
rw [Finset.centerMass_insert _ _ _ hi hsum_t]

Goal state after:
case neg
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
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ interior s
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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
⊢ s.WSameSide x y ∧ s.WOppSide x y → x ∈ s ∨ y ∈ s

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 y : P
⊢ x ∈ s ∨ y ∈ s → s.WSameSide x y ∧ s.WOppSide x y

Tactic:
· rintro ⟨hs, ho⟩
    rw [wOppSide_comm] at ho
    by_contra h
    rw [not_or] at h
    exact h.1 (wOppSide_self_iff.1 (hs.trans_wOppSide ho h.2))

Goal state after:
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 y : P
⊢ x ∈ s ∨ y ∈ s → s.WSameSide x y ∧ s.WOppSide x y
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
h_int'' : ∀ t ∈ Ioi 1, f t = 0
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ∞

Tactic:
setLIntegral_congr_fun measurableSet_Ioi h_int'',

Goal state after:
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
h_int'' : ∀ t ∈ Ioi 1, f t = 0
⊢ ∫⁻ (x : ℝ) in Ioi 1, 0 ∂volume < ∞