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

Goal state before:
pp: case cons.refine_1.refine_3
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
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
·

Goal state after:
case cons.refine_1.refine_3
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
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2
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
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)

Tactic:
·

Goal state after:
case cons.refine_2
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
inst✝ : IsOrderedRing R
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_1
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
ha' : a ∈ tail
⊢ head ≠ a

pp: case cons.refine_2.refine_2
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
⊢ tail ≠ [a, a]

Tactic:
·

Goal state after:
case cons.refine_2.refine_1
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
ha' : a ∈ tail
⊢ head ≠ a
Module: Mathlib.Combinatorics.Hall.Finite

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

Tactic:
·

Goal state after:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z ↦ ↑z) s' ≠ univ → #s' < #((image (fun z ↦ ↑z) s').biUnion t)
he : s' = ∅
⊢ #s' ≤ #(s'.biUnion fun x' ↦ (t ↑x').erase a)
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_1.cons.inl
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
    ∀ (a : P), head :: head :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head :: tail)
ha : ∀ (a : P), head :: head :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a]
ha' : head ∈ head :: tail
⊢ False

pp: case cons.refine_2.refine_1.cons.inr
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
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False

Tactic:
·

Goal state after:
case cons.refine_2.refine_1.cons.inl
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head :: tail) ∧ Triplewise (Sbtw R) (head :: tail)) ∧
    ∀ (a : P), head :: head :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head :: tail)
ha : ∀ (a : P), head :: head :: tail ≠ [a, a]
ht' : List.Wbtw R (head :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔ ∀ (a : P), head :: tail ≠ [a, a]
ha' : head ∈ head :: tail
⊢ False
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ Continuous (Prod.map id (Real.toEReal ∘ ⇑re))

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ IsClosed A

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ Continuous (Prod.map id (Real.toEReal ∘ ⇑re))
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ Continuous (Prod.map id (Real.toEReal ∘ ⇑re))

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ IsClosed A

Tactic:
· exact continuous_id.prodMap <| continuous_coe_real_ereal.comp reCLM.cont

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ IsClosed A
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
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ IsClosed A

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ IsClosed A
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_1.cons.inr
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
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False

Tactic:
·

Goal state after:
case cons.refine_2.refine_1.cons.inr
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
inst✝ : IsOrderedRing R
head head2 : P
tail : List P
x✝ :
  (Pairwise (Sbtw R head) (head2 :: tail) ∧ Triplewise (Sbtw R) (head2 :: tail)) ∧
    ∀ (a : P), head :: head2 :: tail ≠ [a, a]
hp : (∀ a' ∈ tail, Sbtw R head head2 a') ∧ Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) (head2 :: tail)
ha : ∀ (a : P), head :: head2 :: tail ≠ [a, a]
ht' : List.Wbtw R (head2 :: tail)
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head2 :: tail) ↔ ∀ (a : P), head2 :: tail ≠ [a, a]
ha' : head ∈ head2 :: tail
hat : head ∈ tail
⊢ False
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_2.refine_2
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
⊢ tail ≠ [a, a]

Tactic:
·

Goal state after:
case cons.refine_2.refine_2
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
inst✝ : IsOrderedRing R
head : P
tail : List P
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
a : P
⊢ tail ≠ [a, a]
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_1
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
⊢ Function.Injective fun z ↦ if h : z = x then y else f' ⟨z, h⟩

pp: case refine_2
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
⊢ ∀ (x_1 : ι), (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) x_1 ∈ t x_1

Tactic:
·

Goal state after:
case refine_1
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
⊢ Function.Injective fun z ↦ if h : z = x then y else f' ⟨z, h⟩
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
⊢ (s.domRestrict (⇑re ∘ ⇑(-c • u)) + const (↑s) (c * re (u x) + a)) z ≤ s.domRestrict φ z

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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
⊢ re ((-c • u) x) + (c * re (u x) + a) = a

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
⊢ (s.domRestrict (⇑re ∘ ⇑(-c • u)) + const (↑s) (c * re (u x) + a)) z ≤ s.domRestrict φ z
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_2
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
⊢ ∀ (x_1 : ι), (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) x_1 ∈ t x_1

Tactic:
·

Goal state after:
case refine_2
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
⊢ ∀ (x_1 : ι), (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) x_1 ∈ t x_1
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_1
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
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ List.Wbtw R l

pp: case refine_2
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
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
·

Goal state after:
case refine_1
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
l : List P
hl : l ≠ []
x✝ : ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ List.Wbtw R l
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2
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
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
·

Goal state after:
case refine_2
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
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case pos
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
hz : z = x
⊢ y ∈ t z

pp: case neg
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
hz : ¬z = x
⊢ f' ⟨z, hz⟩ ∈ t z

Tactic:
·

Goal state after:
case pos
ι : 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 ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z : ι
hz : z = x
⊢ y ∈ t z