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

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hlsc : LowerSemicontinuousOn (fun x ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn (fun y ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ ⨅ x ∈ X, f x y) Y b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha, b, hb

Goal state after:
case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
X : Set E
Y : Set F
f : E → F → β
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hlsc : LowerSemicontinuousOn (fun x ↦ ⨆ y ∈ Y, f x y) X
husc : UpperSemicontinuousOn (fun y ↦ ⨅ x ∈ X, f x y) Y
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ ⨆ y ∈ Y, f x y) X a
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ ⨅ x ∈ X, f x y) Y b
⊢ IsSaddlePointOn X Y f a b
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹⁶ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁵ : TopologicalSpace E
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module ℝ E
inst✝¹² : IsTopologicalAddGroup E
inst✝¹¹ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module ℝ F
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝⁵ : TopologicalSpace β
inst✝⁴ : OrderTopology β
γ : Type u_5
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
ι : β ↪o γ
hι : Continuous ⇑ι
φ : E → F → γ := fun x y ↦ ι (f x y)
x : E
hx : x ∈ X
⊢ UpperSemicontinuousOn (fun y ↦ φ x y) Y

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

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹⁶ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁵ : TopologicalSpace E
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module ℝ E
inst✝¹² : IsTopologicalAddGroup E
inst✝¹¹ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module ℝ F
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝⁵ : TopologicalSpace β
inst✝⁴ : OrderTopology β
γ : Type u_5
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
ι : β ↪o γ
hι : Continuous ⇑ι
φ : E → F → γ := fun x y ↦ ι (f x y)
hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ φ x y) Y
hφx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ φ x y
hφy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ φ x y) X
hφy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ φ x y
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
hab : IsSaddlePointOn X Y φ a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha, b, hb

Goal state after:
case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹⁶ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝¹⁵ : TopologicalSpace E
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module ℝ E
inst✝¹² : IsTopologicalAddGroup E
inst✝¹¹ : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module ℝ F
inst✝⁷ : IsTopologicalAddGroup F
inst✝⁶ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝⁵ : TopologicalSpace β
inst✝⁴ : OrderTopology β
γ : Type u_5
inst✝³ : CompleteLinearOrder γ
inst✝² : DenselyOrdered γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
ι : β ↪o γ
hι : Continuous ⇑ι
φ : E → F → γ := ⋯
hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ φ x y) Y
hφx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ φ x y
hφy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ φ x y) X
hφy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ φ x y
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
hab : IsSaddlePointOn X Y φ a b
⊢ IsSaddlePointOn X Y f a b
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : Fintype ι
B : Type u_3
inst✝¹⁸ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁷ : NormedAddCommGroup F₁
inst✝¹⁶ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁵ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹² : (x : B) → TopologicalSpace (E₁ x)
inst✝¹¹ : FiberBundle F₁ E₁
inst✝¹⁰ : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝⁷ : (x : B) → AddCommGroup (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
⊢ ∀
    e ∈
      {e |
        ∃ e₁ e₂,
          ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂), e = continuousAlternatingMap 𝕜 ι e₁ e₂},
    ∀
      e' ∈
        {e |
          ∃ e₁ e₂,
            ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂),
              e = continuousAlternatingMap 𝕜 ι e₁ e₂},
      ∃ f,
        ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F₁ [⋀^ι]→L[𝕜] F₂), (f b) v = (↑e' { proj := b, snd := e.symm b v }).2

Tactic:
by
    rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
    exact ⟨continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂',
      continuousOn_continuousAlternatingMapCoordChange,
      continuousAlternatingMapCoordChange_apply⟩

Goal state after: