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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
ext; simp [forall_comm (α := M)]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: case smul
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
x : N
hx : x ∈ dual p s
y✝ : M
t : R≥0
y : M
_hy : y ∈ Submodule.span R≥0 s
hy : 0 ≤ (p y) x
⊢ 0 ≤ (p (t • y)) x

Tactic:
rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s₁ s₂ t : Set E
⊢ ⋃ x, ⋃ (_ : x ∈ s₁ ∨ x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y =
    (⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y

Tactic:
iUnion_or,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s₁ s₂ t : Set E
⊢ ⋃ x, (⋃ (_ : x ∈ s₁), ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ (_ : x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y =
    (⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y
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
⊢ intrinsicInterior 𝕜 s ∪ intrinsicFrontier 𝕜 s = intrinsicClosure 𝕜 s

Tactic:
by
  simp [intrinsicClosure, intrinsicInterior, intrinsicFrontier, closure_eq_interior_union_frontier,
    image_union]

Goal state after:
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
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
have : Nonempty s := hs.to_subtype
    rw [intrinsicFrontier, ← image_frontier_preimage_comp e he_homeo,
      (funext he : (↑) ∘ e = f ∘ (↑)),
      preimage_image_eq_of_homeomorph_affineSpan e he_homeo he, image_comp]; rfl

Goal state after:
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
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
rw [intrinsicClosure, ← image_closure_preimage_comp e he_homeo,
      (funext he : (↑) ∘ e = f ∘ (↑)),
      preimage_image_eq_of_homeomorph_affineSpan e he_homeo he, image_comp]

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
⊢ f '' Subtype.val '' closure[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s) = f '' intrinsicClosure 𝕜 s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y,
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧
        ↑y = x) ↔
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty

Tactic:
refine ⟨?_, fun h => ⟨⟨x, _⟩, ?_, Subtype.coe_mk _ ?_⟩⟩

Goal state after:
case refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y,
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧
        ↑y = x) →
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty

case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ ∀ (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o → ⟨x, ?refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty

case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 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
hsne : s.Nonempty
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
have := hsne.coe_sort
  obtain ⟨p, hp⟩ := hsne
  let p' : _root_.affineSpan ℝ s := ⟨p, subset_affineSpan _ _ hp⟩
  rw [intrinsicInterior, image_nonempty,
    aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
    Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
    AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]
  exact hscv.affine_preimage
    ((_root_.affineSpan ℝ s).subtype.comp
      (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)

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

Goal state before:
pp: I : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst✝¹ : Zero X
inst✝ : ConvexSpace R X
i✝ : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : i ∉ w.weights.support.biUnion support
⊢ (iConvexComb w fun x ↦ x i) = 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
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
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
⊢ ∑ x ∈ d.weights.support, (f.weights d * d.weights x) • (x -ᵥ b) =
    ∑ a ∈ (f.weights d • d.weights).support, h a (f.weights d * d.weights a)

Tactic:
· refine Finset.sum_congr ?_ (fun _ _ => rfl)
    ext p
    simp only [Finsupp.mem_support_iff, ne_eq]
    constructor
    · intro hp
      exact (mul_pos ((f.nonneg d).lt_of_ne' hd) ((d.nonneg p).lt_of_ne' hp)).ne'
    · intro hp hp'
      simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, hp', mul_zero,
        not_true_eq_false] at hp

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

Goal state before:
pp: case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ 0 = w.weights y

Tactic:
simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : LinearOrder β
inst✝ : SMul 𝕜 E
s : Set E
f : E → β
⊢ ((∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)) ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → min (f x) (f y) ≤ f (a • x + b • y)) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ∈ uIcc (f x) (f y)

Tactic:
simp_rw [← forall_and, ← Icc_min_max, mem_Icc, and_comm]

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

Goal state before:
pp: case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * dist x.1 y.1 + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)

Tactic:
nth_grw 1 [le_max_left (dist x.1 y.1) (dist x.2 y.2)]

Goal state after:
case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ ↑i * max (dist x.1 y.1) (dist x.2 y.2) + (1 - ↑i) * dist x.2 y.2 ≤ max (dist x.1 y.1) (dist x.2 y.2)

case ha
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
i : ↑(Set.Icc 0 1)
x y : X × X
⊢ 0 ≤ ↑i
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : f t ∈ Set.Ioo 0 1
⊢ ∀ (x : ↑(f ⁻¹' Set.Ioo 0 1)), ↑x ∈ f ⁻¹' {0}ᶜ

Tactic:
simp_all

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 0
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht : f t ∈ Set.Ioo 0 1
⊢ ∀ (x : ↑(f ⁻¹' Set.Ioo 0 1)), ↑x ∈ f ⁻¹' {1}ᶜ

Tactic:
simp_all

Goal state after:
X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
D : ℝ
t : T
hx : ContinuousOn x (f ⁻¹' {0})ᶜ
hy : ContinuousOn y (f ⁻¹' {1})ᶜ
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
ht : 0 < f t ∧ f t < 1
⊢ ∀ (a : T), 0 < f a → f a < 1 → ¬f a = 1
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case hs
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ AffineIndependent 𝕜 Subtype.val

pp: case ht₁
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

pp: case ht₂
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t

Tactic:
· apply indep.mono
      simp only [Finset.coe_union]
      exact Set.union_subset (Set.subset_biUnion_of_mem hs) (Set.subset_biUnion_of_mem ht)

Goal state after:
case ht₁
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

case ht₂
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
s : Set (Set (Sym2 V))
u v : V
⊢ (fromEdgeSet (⋂₀ s)).Adj u v ↔ (sInf (fromEdgeSet '' s)).Adj u v

Tactic:
simp_all

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

Goal state before:
pp: V : Type u
ι : Sort u_2
f : ι → Set (Sym2 V)
u v : V
⊢ (fromEdgeSet (⋂ i, f i)).Adj u v ↔ (⨅ i, fromEdgeSet (f i)).Adj u v

Tactic:
simp_all

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

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

pp: case mpr
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 → s.WSameSide (v +ᵥ x) y

Tactic:
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
    refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
    rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]

Goal state after:
case mpr
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 → s.WSameSide (v +ᵥ x) y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mp
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.WOppSide (v +ᵥ x) y → s.WOppSide x y

pp: case mpr
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.WOppSide x y → s.WOppSide (v +ᵥ x) y

Tactic:
· rintro ⟨p₁, hp₁, p₂, hp₂, h⟩
    refine
      ⟨-v +ᵥ p₁, AffineSubspace.vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) hp₁, p₂, hp₂, ?_⟩
    rwa [vsub_vadd_eq_vsub_sub, sub_neg_eq_add, add_comm, ← vadd_vsub_assoc]

Goal state after:
case mpr
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.WOppSide x y → s.WOppSide (v +ᵥ x) y
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
⊢ -(y -ᵥ p₂) = -c₂ • m

Tactic:
h₂,

Goal state after:
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
⊢ -(c₂ • m) = -c₂ • m
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < max (dist p₂ p) r
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
lt_max_iff,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₂ p₃ p₁
hp₃p₂ : ¬p₃ = p₂
hs : Sbtw ℝ p₂ p₃ p₁
hs' : r < dist p₂ p ∨ r < r
⊢ Wbtw ℝ p₁ p₂ p₃
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < max r (dist p₂ p)
⊢ Wbtw ℝ p₁ p₂ p₃

Tactic:
lt_max_iff,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
r : ℝ
h : Collinear ℝ {p₁, p₂, p₃}
hp₁ : dist p₁ p = r
hp₂ : dist p₂ p ≤ r
hp₃ : dist p₃ p = r
hp₁p₃ : p₁ ≠ p₃
hw : Wbtw ℝ p₃ p₁ p₂
hp₁p₂ : ¬p₁ = p₂
hs : Sbtw ℝ p₃ p₁ p₂
hs' : r < r ∨ r < dist p₂ p
⊢ Wbtw ℝ p₁ p₂ p₃
Module: Mathlib.Analysis.Convex.StrictCombination

Goal state before:
pp: case inl
V : Type u_2
ι : Type u_4
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p 0
⊢ t.centerMass w z ∈ ball p 0

Tactic:
simp_all

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

Goal state before:
pp: case mpr.inr
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
h : y ∈ s
⊢ s.WSameSide x y ∧ s.WOppSide x y

Tactic:
· exact ⟨wSameSide_of_right_mem x h, wOppSide_of_right_mem x h⟩

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

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
r : ℝ
p₀ : P
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : ∀ (i : Fin (n + 1)), (affineCombination ℝ univ s.points) w ≠ s.points i
hij : ∀ (i : Fin (n + 1)), w i = 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case inl
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i = 1
⊢ IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)

Tactic:
convert! hw
    rw [← one_smul 𝕜 (a i), ← hwi, eq_comm]
    rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁
    refine sum_eq_single _ (fun j hj hji ↦ ?_) (by simp [hi])
    rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]

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

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsConnected {y | s.WOppSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
  have : Nonempty s := ⟨⟨p, hp⟩⟩
  by_cases hx : x ∈ s
  · simp only [wOppSide_of_left_mem, hx]
    have := AddTorsor.connectedSpace V P
    exact isConnected_univ
  · rw [setOfPred_wOppSide_eq_image2 hx hp, ← Set.image_prod]
    refine (isConnected_Iic.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
    convert! AddTorsor.connectedSpace s.direction s

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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h : w₂ i = 0
⊢ False

Tactic:
simp_all

Goal state after: