awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
right : LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)
⊢ IsSaddlePointOn X Y f a b

Tactic:
rw [isSaddlePointOn_iff' ha hb]

Premises used: isSaddlePointOn_iff'
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
le_trans (le_iInf₂ ha') ?_

Premises used: le_iInf₂, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
right : LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨅ x ∈ X, f x b)
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, f a y) (⨅ x ∈ X, f x b)

Tactic:
refine le_trans (le_iInf₂ ha') ?_

Premises used: le_iInf₂, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
⊢ LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨅ x ∈ X, f x b)

Tactic:
le_trans ?_ (iSup₂_le_iff.mpr hb')

Premises used: Iff.mpr, iSup₂_le_iff, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
right :
  LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i)
    (⨆ i ∈ Y, (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) i)
⊢ LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i) (⨅ x ∈ X, f x b)

Tactic:
refine le_trans ?_ (iSup₂_le_iff.mpr hb')

Premises used: Iff.mpr, iSup₂_le_iff, le_trans
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_7 : TopologicalSpace F
inst_8 : AddCommGroup F
inst_9 : Module ℝ F
inst_10 : IsTopologicalAddGroup F
inst_11 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
hlsc : LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn.{u_1, u_3} (β := β) (fun (x : E) ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn.{u_2, u_3} (β := β) (fun (y : F) ↦ ⨅ x ∈ X, f x y) Y b
right right₁ : LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨆ y ∈ Y, ⨅ x ∈ X, f x y)
⊢ LE.le.{u_3} (α := β) (⨅ i ∈ X, (fun (x : E) ↦ (⨆ y ∈ Y, f x y : β)) i)
    (⨆ i ∈ Y, (fun (y : F) ↦ (⨅ x ∈ X, f x y : β)) i)

Tactic:
rw [minimax' ne_X cX kX hfy hfy' cY hfx hfx']

Premises used: Sion.minimax'
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
x : E
hx : x ∈ X
⊢ UpperSemicontinuousOn.{u_2, u_5} (β := γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := β) (⇑ι : (a : β) → γ) fun (y : F) ↦ f x y) Y

Tactic:
Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone

Premises used: OrderEmbedding.monotone, Continuous.comp_upperSemicontinuousOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
x : E
hx : x ∈ X
⊢ UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y

Tactic:
convert! Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone

Premises used: OrderEmbedding.monotone, Continuous.comp_upperSemicontinuousOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
⊢ ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y

Tactic:
have hφx (x) (hx : x ∈ X) : UpperSemicontinuousOn (fun y ↦ φ x y) Y := by
    convert! Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
x : E
hx : x ∈ X
⊢ QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := β) (⇑ι : (a : β) → γ) fun (y : F) ↦ f x y)

Tactic:
(hfx' x hx).monotone_comp ι.monotone

Premises used: OrderEmbedding.monotone, QuasiconcaveOn.monotone_comp
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
x : E
hx : x ∈ X
⊢ QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y

Tactic:
convert! (hfx' x hx).monotone_comp ι.monotone

Premises used: OrderEmbedding.monotone, QuasiconcaveOn.monotone_comp
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
⊢ ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y

Tactic:
have hφx' (x) (hx : x ∈ X) : QuasiconcaveOn ℝ Y fun y ↦ φ x y := by
    convert! (hfx' x hx).monotone_comp ι.monotone
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
y : F
hy : y ∈ Y
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := γ)
    (Function.comp.{u_1 + 1, u_3 + 1, u_5 + 1} (β := β) (⇑ι : (a : β) → γ) fun (x : E) ↦ f x y) X

Tactic:
Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone

Premises used: OrderEmbedding.monotone, Continuous.comp_lowerSemicontinuousOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
y : F
hy : y ∈ Y
⊢ LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X

Tactic:
convert! Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone

Premises used: OrderEmbedding.monotone, Continuous.comp_lowerSemicontinuousOn
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
⊢ ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X

Tactic:
have hφy (y) (hy : y ∈ Y) : LowerSemicontinuousOn (fun x ↦ φ x y) X := by
    convert! Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
y : F
hy : y ∈ Y
⊢ QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X
    (Function.comp.{u_1 + 1, u_3 + 1, u_5 + 1} (β := β) (⇑ι : (a : β) → γ) fun (x : E) ↦ f x y)

Tactic:
(hfy' y hy).monotone_comp ι.monotone

Premises used: OrderEmbedding.monotone, QuasiconvexOn.monotone_comp