mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
rcases exists_countable_dense E with ⟨D, D_count, D_dense⟩

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f₂ - f₁
hr : 1 ≤ r
⊢ 0 ≤ logCounting f₂ r - logCounting f₁ r

Tactic:
simpa using logCounting_nonneg h hr

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
yx : y ≤ x
u : ℝ
xu : x ≤ u
uz : u ≤ z
v : ℝ
xv : x ≤ v
vz : v ≤ z
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal (↑l * (v - u))

Tactic:
rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
      hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc, sup_of_le_right (yx.trans xu),
      inf_of_le_right vz]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p₃ p₄ : P
⊢ List.Wbtw R [p₁, p₂, p₃, p₄] ↔ Wbtw R p₁ p₂ p₃ ∧ Wbtw R p₁ p₂ p₄ ∧ Wbtw R p₁ p₃ p₄ ∧ Wbtw R p₂ p₃ p₄

Tactic:
simp [List.Wbtw, triplewise_cons, and_assoc]

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset ↑{x' | x' ≠ x}
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this : Nonempty ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
⊢ #s' ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

Tactic:
have := Classical.decEq ι

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
⊢ #s' ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ p -ᵥ z ∈ (fun x ↦ p -ᵥ x) '' affineSegment R x y ↔ z ∈ affineSegment R x y

Tactic:
(vsub_right_injective p).mem_set_image

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case pos
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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
hl : l = []
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l

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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
· rcases exists_pair_ne P with ⟨p₁, p₂, hp₁p₂⟩
      exact ⟨p₁, p₂, hp₁p₂, by simp [hl, sortedLT_iff_pairwise]⟩

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
inst✝ : Nontrivial P
l : List P
h : List.Sbtw R l
hl : ¬l = []
⊢ ∃ p₁ p₂, p₁ ≠ p₂ ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap p₁ p₂)) l' = l
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite (F.obj j)
hne : ∀ (j : J), Nonempty (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this✝¹ : ∀ (j : J), DiscreteTopology ↑(F'.obj j)
this✝ : ∀ (j : J), Finite ↑(F'.obj j)
this : ∀ (j : J), Nonempty ↑(F'.obj j)
⊢ F.sections.Nonempty

Tactic:
obtain ⟨⟨u, hu⟩⟩ := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} F'

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite (F.obj j)
hne : ∀ (j : J), Nonempty (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this✝¹ : ∀ (j : J), DiscreteTopology ↑(F'.obj j)
this✝ : ∀ (j : J), Finite ↑(F'.obj j)
this : ∀ (j : J), Nonempty ↑(F'.obj j)
u : (j : J) → ↑(F'.obj j)
hu : u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F'.map f)) (u i) = u j}
⊢ F.sections.Nonempty
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range ⇑(ConcreteCategory.hom (F.map f ≫ F.map g)) ⊆ range ⇑(ConcreteCategory.hom (F.map g))

Tactic:
types_comp

Goal state after:
case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range (⇑(ConcreteCategory.hom (F.map g)) ∘ ⇑(ConcreteCategory.hom (F.map f))) ⊆
    range ⇑(ConcreteCategory.hom (F.map g))
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range ⇑(ConcreteCategory.hom (F.map g' ≫ F.map f')) ⊆ range ⇑(ConcreteCategory.hom (F.map f'))

Tactic:
types_comp

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : i ⟶ j
h : ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ range (⇑(ConcreteCategory.hom (F.map f')) ∘ ⇑(ConcreteCategory.hom (F.map g'))) ⊆
    range ⇑(ConcreteCategory.hom (F.map f'))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
h : ∀ (A : Finset α), {b | ∃ a ∈ A, r a b} = A.biUnion r'
⊢ (∀ (A : Finset α), #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
have h' : ∀ (f : α → β) (x), r x (f x) ↔ f x ∈ r' x := by simp [r']

Goal state after:
α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
h : ∀ (A : Finset α), {b | ∃ a ∈ A, r a b} = A.biUnion r'
h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x
⊢ (∀ (A : Finset α), #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)
Module: Mathlib.Analysis.Convex.Caratheodory

Goal state before:
pp: 𝕜 : 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
⊢ f i₀ / g i₀ * g e ≤ 0

Tactic:
apply mul_nonpos_of_nonneg_of_nonpos

Goal state after:
case ha
𝕜 : 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 := ⋯
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 → 𝕜 := ⋯
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∉ s
⊢ 0 ≤ f i₀ / g i₀

case hb
𝕜 : 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 := ⋯
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 → 𝕜 := ⋯
hk : k i₀ = 0
ksum : ∑ e ∈ t.erase i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∉ s
⊢ g e ≤ 0
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
⊢ ∀ a ∈ univ, N a.1 a.2 ≠ 0 → M a.1 a.2 ≠ 0

Tactic:
rintro ⟨i', j'⟩ _ hN' hM'

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
this : ∃ M' ∈ doublyStochastic R n, N = s' • M'
i' j' : n
a✝ : (i', j') ∈ univ
hN' : N (i', j').1 (i', j').2 ≠ 0
hM' : M (i', j').1 (i', j').2 = 0
⊢ False
Module: Mathlib.Analysis.Convex.Extrema

Goal state before:
pp: E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}

Tactic:
have h_maps : MapsTo g (Icc 0 1) s := by
    simpa only [g, mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
      using h_conv.1.segment_subset a_in_s x_in_s

Goal state after:
E : Type u_1
β : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
s : Set E
f : E → β
a : E
a_in_s : a ∈ s
h_localmin : IsLocalMinOn f s a
h_conv : ConvexOn ℝ s f
x : E
x_in_s : x ∈ s
g : ℝ →ᵃ[ℝ] E := AffineMap.lineMap a x
hg0 : g 0 = a
hg1 : g 1 = x
hgc : Continuous[_, inst✝⁹] ⇑g
h_maps : MapsTo (⇑g) (Icc 0 1) s
⊢ x ∈ {x | (fun x ↦ f a ≤ f x) x}
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‖
hcnorm : range ⇑c ⊆ closedBall 0 (cnorm + 1)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s

Tactic:
have hε' : 0 < ε' := by positivity

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)
ε : ℝ
hε : ε > 0
hεs : ball 0 ε ⊆ s
ε' : ℝ := ε / 2 / (cnorm + 1)
hc' : 0 < cnorm + 1
hε' : 0 < ε'
⊢ ∃ b, 0 ∈ interior ((convexHull ℝ) (range ⇑b)) ∧ (convexHull ℝ) (range ⇑b) ⊆ s
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 / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
⊢ a + b = 1

Tactic:
simp [field, a, b]

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
htne : (interior t).Nonempty
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t

Tactic:
rcases htne with ⟨y, hy⟩

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
⊢ ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure[inst✝³] s = closure[inst✝³] t
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case refine_2
α : 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 := borel 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
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∑ i ∈ (G n).range, μ.real (⇑(G n) ⁻¹' {i}) = 1

Tactic:
simp_rw [measureReal_def]
    rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,
      ENNReal.toReal_one]
    finiteness

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 α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ)

Tactic:
refine hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
inst✝ : IsFiniteMeasure μ
hfi : Integrable f μ
H : ∀ (t : Set α), MeasurableSet t → μ t ≠ 0 → μ tᶜ ≠ 0 → ⨍ (x : α) in t, f x ∂μ = ⨍ (x : α) in tᶜ, f x ∂μ
t : Set α
ht : MeasurableSet t
ht' : μ t < ∞
⊢ ∫ (x : α) in t, f x ∂μ = ∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: 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
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join

Tactic:
have hR := Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
    f.join.weights.support f.join.weights id f.join.total b

Goal state after:
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
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
⊢ IsConvexSet R (s.pi t)

Tactic:
by
  classical
  refine fun w hw i hi ↦ ht i hi ?_
  grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]

Goal state after: