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

Goal state before:
pp: case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fl '' s
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ

Tactic:
rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩

Goal state after:
case refine_1
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝⁴ : 0 ≤ ε₂
this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this✝³
Fl : X → X ⊕ Y := inl
Fr : Y → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this✝ :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fl '' s
x : X
x_in_s : x ∈ s
xx' : Fl x = x'
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A =
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)

Tactic:
convert_to @skyscraperPresheaf X p₀ (fun U => hd <| (Opens.map <| ofHom <|
      ContinuousMap.const _ p₀).obj U)
    C _ _ A = _

Goal state after:
case e'_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A = skyscraperPresheaf p₀ A

case convert_2
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A : C
hd : (U : Opens ↑(of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)
⊢ skyscraperPresheaf p₀ A =
    (Presheaf.pushforward C (ofHom (ContinuousMap.const (↑(of PUnit.{u + 1})) p₀))).obj
      (skyscraperPresheaf PUnit.unit A)
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: case neg.refine_2.e_s
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ {0} = ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))

Tactic:
eq_comm,

Goal state after:
case neg.refine_2.e_s
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1)) = {0}
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : Preorder X
inst✝³ : Topology.IsUpperSet X
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
F : X ⥤ C
P : (Opens X)ᵒᵖ ⥤ C
η : principals X ⋙ P ⟶ F
inst✝ : P.IsRightKanExtension η
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X) P

Tactic:
let γ : principals X ⋙ principalsKanExtension F ⟶ F :=
    (principals X).pointwiseRightKanExtensionCounit F
  let _ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
  have : P ≅ principalsKanExtension F :=
    @rightKanExtensionUnique _ _ _ _ _ _ _ _ _ _ (by assumption) _ _ (by assumption)
  change TopCat.Presheaf.IsSheaf (X := TopCat.of X) P
  rw [isSheaf_iso_iff this]
  exact isSheaf_principalsKanExtension (X := TopCat.of X) F

Goal state after:
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
⊢ i = j ∨ Nonempty (↑i ⟶ ↑j) ∨ Nonempty (↑j ⟶ ↑i)

Tactic:
grind [Subtype.ext_iff, h i.property j.property]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε

Tactic:
have j' : j = (E q) (Ψ y) := by simp only [j, Ψ, Equiv.apply_symm_apply, Fin.val_cast]

Goal state after:
case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ⋃₀ c ∈ 𝒮

Tactic:
refine ⟨by grind, fun a hac ha ↦ ?_, by grind⟩

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
a : Set (Set X)
hac : a ⊆ ⋃₀ c
ha : a.Finite
⊢ (⋂₀ a).Nonempty
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
⊢ False

Tactic:
let Z := ⋂₀ B'

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
⊢ False
Module: Mathlib.Topology.Subpath

Goal state before:
pp: t₀ t₁ : ↑I
⊢ range (Icc.convexComb t₀ t₁) = uIcc t₀ t₁

Tactic:
rw [range_eq_iff]
  constructor
  · intro s
    exact convex_uIcc (t₀ : ℝ) t₁ left_mem_uIcc right_mem_uIcc
      (one_minus_nonneg s) (nonneg s) (sub_add_cancel _ _)
  · intro t (ht : (t : ℝ) ∈ uIcc (t₀ : ℝ) (t₁ : ℝ))
    rw [← segment_eq_uIcc, segment_eq_image] at ht
    obtain ⟨s, hs, hst⟩ := ht
    use ⟨s, hs⟩
    ext
    exact hst

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : SeparationQuotient.mk c = SeparationQuotient.mk b
⊢ (b, c) ∈ U

Tactic:
eq_comm,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : SeparationQuotient.mk b = SeparationQuotient.mk c
⊢ (b, c) ∈ U
Module: Mathlib.Topology.Sion

Goal state before:
pp: case inr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
x : E
hx : x ∈ X'
y : F
h : t < f x y
hy : y ∈ s
⊢ ∃ y ∈ s, t < f x y

Tactic:
· exact ⟨y, hy, h⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
· enter [1, i, 1, hi]
        rw [(not_specializes_iff_exists_open.1 (mt Specializes.inseparable hi)).elim
          fun S hS => comap_const_of_notMem (hS.1.mem_nhds hS.2.1) hS.2.2]

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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ :=
    exists_isSaddlePointOn' ne_X kX hφy hφy' cY kY hφx hφx' cX ne_Y

Goal state after:
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
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²² : NontriviallyNormedField 𝕜
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₁)
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✝⁸ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁷ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁶ : Finite ι
inst✝⁵ : VectorBundle 𝕜 F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
⊢ ContinuousOn (continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
by
  cases nonempty_fintype ι
  simp +unfoldPartialApp only [continuousAlternatingMapCoordChange,
    ContinuousLinearEquiv.coe_continuousAlternatingMapCongr, ContinuousLinearEquiv.symm_symm]
  refine .clm_comp ?_ ?_
  · refine map_continuous (ContinuousLinearMap.compContinuousAlternatingMapCLM (ι := ι) 𝕜 F₁ F₂ F₂)
      |>.comp_continuousOn ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)
    mfld_set_tac
  · refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_
    exact continuousOn_coordChange 𝕜 e₁' e₁ |>.mono (by mfld_set_tac)

Goal state after: