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

Goal state before:
pp: case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f

Tactic:
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α

Goal state after:
case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, s.Countable ∧ Dense s
⊢ ∃ f, Isometry f
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
packingNumber

Goal state after:
case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard ≠ ⊤
hA : A.Nonempty
this : Nonempty { s // s ⊆ A ∧ IsSeparated (↑ε) s }
h_exists : ⨆ i, (↑i).encard < ⊤ → ∃ i, (↑i).encard = ⨆ i, (↑i).encard := ENat.exists_eq_iSup_of_lt_top
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε) C), C.encard
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (⇑toSnowflaking '' s) = ediam s ^ α

Tactic:
simp [image_toSnowflaking_eq_preimage]

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := ⋯
U : Set α
⊢ IsOpen[scott α univ] U ↔ IsOpen[upper α] U

Tactic:
@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
    ({ topology_eq_upperTopology := rfl }) U

Goal state after:
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen[scott α univ] U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (x, r), ⋯⟩

Tactic:
· simp [Prod.Lex.lt_iff, hs, hs']

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this✝ : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
this : z ∈ range Φ
x : X
hx : Φ x = z
⊢ dist (Φ x) (Ψ y) = dist z (f (inr y))

Tactic:
by rw [hx]

Goal state after:
Module: Mathlib.Topology.Order.PartialSups

Goal state before:
pp: L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((partialSups f) n) l (𝓝 ((partialSups g) n))

Tactic:
by
  simp only [partialSups_eq_sup'_range]
  refine finset_sup'_nhds _ ?_
  simpa [Nat.lt_succ_iff]

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

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∃ x, x✝.IsAmalgamation x

pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1

Tactic:
· refine ⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩
      rwa [le_bot_iff.1 hU.le]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
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)
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))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε

Tactic:
have Aq : (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ := by
        simp [← this, *]

Goal state after:
case refine_3
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
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)
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))
this✝ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise ι)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          Y =
      Opposite.rec
          (fun x ↦
            Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
              c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
          X_1 ≫
        ((diagram U).op ⋙ F).map f

Tactic:
intro x y f
        induction x with | op x => ?_
        induction y with | op y => ?_
        have ef : f = f.unop.op := rfl
        revert ef
        generalize f.unop = f'
        rintro rfl
        rcases x with (⟨i⟩ | ⟨⟩) <;> rcases y with (⟨⟩ | ⟨j, j⟩) <;> rcases f' with ⟨⟩
        · dsimp
          rw [F.map_id]
          simp
        · dsimp
          simp only [Category.id_comp, Category.assoc]
          have h := c.π.naturality WalkingParallelPairHom.left
          dsimp [SheafConditionEqualizerProducts.leftRes] at h
          simp only [Category.id_comp] at h
          have h' := h =≫ Pi.π _ (i, j)
          rw [h']
          simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
          rfl
        · dsimp
          simp only [Category.id_comp, Category.assoc]
          have h := c.π.naturality WalkingParallelPairHom.right
          dsimp [SheafConditionEqualizerProducts.rightRes] at h
          simp only [Category.id_comp] at h
          have h' := h =≫ Pi.π _ (j, i)
          rw [h']
          simp
          rfl
        · dsimp
          rw [F.map_id]
          simp

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

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
⊢ ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

Tactic:
have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) :=
      ciInf_le (by simpa using HD_below_aux2 0) default

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ
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
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
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := ⋯
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
hz'2 : sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ sublevelLeft X f b ↑⟨↑z', hz'Y⟩ ⊆ ∅

Tactic:
← (disjoint_sublevelLeft ha hb').inter_eq

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
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
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
hz'2 : sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y'
hz'Y : ↑z' ∈ Y
⊢ sublevelLeft X f b ↑⟨↑z', hz'Y⟩ ⊆ sublevelLeft X f b' ↑y ∩ sublevelLeft X f b' ↑y'
Module: Mathlib.Topology.Subpath

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

Tactic:
by
  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.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ x ∈ s ∧ IsClopen s) id

Tactic:
refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ i', (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)

case refine_2
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x
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
y : F
hy : y ∈ Y
⊢ SemicontinuousWithinAt (fun x1 x2 ↦ (fun y ↦ ⨅ x ∈ X, f x y) x1 < x2) Y y

Tactic:
apply upperSemicontinuousWithinAt_iInf
    intro i
    exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy

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
y : F
hy : y ∈ Y
⊢ LowerSemicontinuousOn (fun x ↦ φ x y) X

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

Goal state after: