mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f : 𝕜 → 𝕜
⊢ logCounting f⁻¹ ⊤ = logCounting f 0

Tactic:
simp [logCounting_zero, logCounting_top]

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
hl : Triplewise p l
⊢ Triplewise q l

Tactic:
induction hl with

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

Goal state before:
pp: case neg
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : ((∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2))) l'' = head2 :: tail
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2))) l' = head :: head2 :: tail

Tactic:
have hw := h.1.1 _ (getLast_mem ht2)

Goal state after:
case neg
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : ((∀ a' ∈ tail, Wbtw R head head2 a') ∧ Pairwise (Wbtw R head) tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
ht2 : ¬tail = []
hl'' : map (⇑(lineMap head2 (tail.getLast ht2))) l'' = head2 :: tail
hw : Wbtw R head head2 (tail.getLast ht2)
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head (tail.getLast ht2))) l' = head :: head2 :: tail
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ BddAbove 𝓕

Tactic:
· exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
⊢ f = f'

Tactic:
ext a

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
g : ↑(hallMatchingsOn t ι') → ↥ι' → ↥(ι'.biUnion t) := fun f i ↦ ⟨↑f i, ⋯⟩
f f' : ↑(hallMatchingsOn t ι')
h : g f = g f'
a : ↥ι'
⊢ ↑f a = ↑f' a
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (f.symm val✝) = x

Tactic:
(eq_some_iff f).2 hfx

Goal state after:
case some
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
val✝ : β
hfx : f x = some val✝
⊢ Option.rec a₂ id (some x) = x
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b

Tactic:
split_ifs with hb ha ha

Goal state after:
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : b ∈ s
ha : a ∈ s
⊢ some b = some a ↔ some a = some b

case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : b ∈ s
ha : ¬a ∈ s
⊢ some b = some a ↔ False

case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : ¬b ∈ s
ha : a ∈ s
⊢ False ↔ some a = some b

case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
hb : ¬b ∈ s
ha : ¬a ∈ s
⊢ False ↔ False
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
⊢ f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id

Tactic:
by
  ext i j
  rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ ((reindex e₁ e₂) M)ᵀᵀ ∈ colStochastic R m ↔ M ∈ colStochastic R n

Tactic:
transpose_reindex,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
⊢ ((reindex e₂ e₁) Mᵀ)ᵀ ∈ colStochastic R m ↔ M ∈ colStochastic R n
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
i : n
⊢ ∑ j ∈ f i, M i j = s

Tactic:
simp [f, sum_subset (filter_subset _ _), hM.2.1]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0

Tactic:
have hf (A : Finset n) : #A ≤ #(A.biUnion f) := by
    have (i : _) : ∑ j ∈ f i, M i j = s := by simp [f, sum_subset (filter_subset _ _), hM.2.1]
    have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [this]
    have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = #(A.biUnion f) * s := by
      simp [sum_comm (t := A.biUnion f), hM.2.2]
    suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs
    rw [← h₁, ← h₂]
    trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
    · refine sum_le_sum fun i hi => ?_
      exact sum_le_sum_of_subset_of_nonneg (subset_biUnion_of_mem f hi) (by simp [*])
    · exact sum_le_sum_of_subset_of_nonneg (by simp) fun _ _ _ => sum_nonneg fun j _ => hM.1 _ _

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
hf : ∀ (A : Finset n), #A ≤ #(A.biUnion f)
⊢ ∃ σ, ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ * g e ≤ f e

Tactic:
← le_div_iff₀ hge

Goal state after:
case pos
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ ≤ f e / g e
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
⊢ 0 < ε → ∃ b ∈ ↑K, ‖x - b‖ < ε

Tactic:
hε

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
⊢ ∃ b ∈ ↑K, ‖x - b‖ < ε
Module: Mathlib.Analysis.Convex.Body

Goal state before:
pp: case refine_2
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ↑K
⊢ x ∈ ⋂ n, (1 + ↑(u n)) • ↑K

Tactic:
refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)
    exact le_add_of_nonneg_right (by positivity)

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
⊢ (t.erase ↑⟨i₀, hi₀⟩).centerMass k id = t.centerMass f id

Tactic:
rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
g : E → 𝕜
gcombo : ∑ e ∈ t, g e • e = 0
gsum : ∑ e ∈ t, g e = 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
⊢ ∑ i ∈ t.erase i₀, k i • id i = t.centerMass f id
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:

Tactic:
∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
      _ = t.centerMass f id := by
        simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₂ ≤ 0
⊢ Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)

Tactic:
by
  rw [wbtw_comm]
  exact wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' interior s = (fun x ↦ y +ᵥ x) '' ⇑h '' (fun x_1 ↦ -x +ᵥ x_1) '' interior s

Tactic:
image_image,

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' interior s = (fun x_1 ↦ y +ᵥ h (-x +ᵥ x_1)) '' interior s
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_2
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 : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (range ⇑b) + (convexHull ℝ) ↑u ⊆ t

Tactic:
hu₁,

Goal state after:
case refine_2
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 : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ (convexHull ℝ) (range ⇑b) + (convexHull ℝ) s ⊆ t
Module: Mathlib.Analysis.Convex.GaugeRescale

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' closure[inst✝³] s = (fun x ↦ y +ᵥ x) '' ⇑h '' (fun x_1 ↦ -x +ᵥ x_1) '' closure[inst✝³] s

Tactic:
image_image,

Goal state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (fun a ↦ y + h (-x + a)) '' closure[inst✝³] s = (fun x_1 ↦ y +ᵥ h (-x +ᵥ x_1)) '' closure[inst✝³] s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [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
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  · have : Nonempty s := hs.to_subtype
    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]; rfl

Goal state after:
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
⊢ x ∈ intrinsicClosure 𝕜 s ↔ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
simp only [mem_closure_iff, mem_intrinsicClosure]

Goal state after:
𝕜 : 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
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x : N
⊢ map (fun x_1 ↦ x) f = single x

Tactic:
ext a

Goal state after:
R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
N : Type u_10
inst✝ : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
⊢ (map (fun x_1 ↦ x) f).weights a = (single x).weights a
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case refine_2
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.snd w).weights.support ⊆ t

Tactic:
· grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]

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

Goal state before:
pp: case cons
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ sConvexComb w ∈ s

Tactic:
rw [← w.convexCombPair_restrict_restrict_compl {x} (by simpa) hwx']

Goal state after:
case cons
K : Type u_4
X : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t✝ : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄, ↑t ⊆ s → t = w.weights.support → sConvexComb w ∈ s
w : StdSimplex K X
hw : ↑(Finset.cons x t hx) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : w.weights x ≠ 0
hwx' : ∃ y, y ≠ x ∧ w.weights y ≠ 0
⊢ sConvexComb
      (convexCombPair ((filter (fun x_1 ↦ x_1 ∈ {x}) w.weights).sum fun _x k ↦ k)
        ((filter (fun x_1 ↦ x_1 ∉ {x}) w.weights).sum fun _x k ↦ k) ⋯ ⋯ ⋯ (w.restrict {x} ⋯) (w.restrict {x}ᶜ hwx')) ∈
    s
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
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := {i ∈ s | 0 ≤ w i}
J : Finset ι := {i ∈ s | w i < 0}
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
⊢ ∑ i ∈ J, w i • f i + ∑ i ∈ I, w i • f i = 0

Tactic:
simpa only [← h_vsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) _

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

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s✝ t✝ : ℝ
hs✝ : 0 ≤ s✝
ht✝ : 0 ≤ t✝
h✝ : s✝ + t✝ = 1
x✝ y✝ : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y

Tactic:
grw [convexCombPair, dist_sConvexComb_left_le]

Goal state after:
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s✝ t✝ : ℝ
hs✝ : 0 ≤ s✝
ht✝ : 0 ≤ t✝
h✝ : s✝ + t✝ = 1
x✝ y✝ : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ (iConvexComb (StdSimplex.duple x y hs ht h) fun x_1 ↦ dist x_1 x) ≤ t * dist x y
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : 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
hss' : s' ≤ s
⊢ ((Finsupp.equivFunOnFinite.symm ![s', s - s', t]).sum fun x r ↦ r) = 1

Tactic:
by simp [Finsupp.sum_fintype, Fin.sum_univ_succ, ← add_assoc, h]

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

Goal state before:
pp: case e'_3.e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : 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
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ StdSimplex.duple x y hs ht h = StdSimplex.map ![x, x, y] f

Tactic:
ext a

Goal state after:
case e'_3.e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : 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
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
a : X
⊢ (StdSimplex.duple x y hs ht h).weights a = (StdSimplex.map ![x, x, y] f).weights a
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: case e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : 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
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
⊢ StdSimplex.duple x y hs' ht' h' = StdSimplex.map ![x, y, y] f

Tactic:
ext a

Goal state after:
case e_a
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : 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
hss' : s' ≤ s
f : StdSimplex ℝ (Fin 3) := { weights := Finsupp.equivFunOnFinite.symm ![s', s - s', t], nonneg := ⋯, total := ⋯ }
a : X
⊢ (StdSimplex.duple x y hs' ht' h').weights a = (StdSimplex.map ![x, y, y] f).weights a