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

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
⊢ IsCompact A

Tactic:
by
  refine isCompact_of_finite_subcover fun {ι} U hUo hAU => ?_
  by_cases! h : Nonempty ι
  · obtain ⟨f, hf⟩ := hl.indexed_countable_subcover U hUo hAU
    obtain ⟨t, ht⟩ := isCountablyCompact_iff_countable_open_cover.1 hA (U ∘ f)
      (fun n => hUo (f n)) hf
    classical
    exact ⟨t.image f, by simp_all⟩
  · exact ⟨∅, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ u ∈ ⋃ i, {s | IsOpen[induced (fun x ↦ x ∈ i) sierpinskiSpace] s}

Tactic:
simp only [Set.mem_iUnion, Set.mem_ofPred_eq, isOpen_induced_iff]

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x ↦ x ∈ i) ⁻¹' t_1 = u
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑F),
    (∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑F)),
    IsClosed s → IsClosed[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
exact fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∀ x ∈ Finset.range #J,
    {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c} ⊆
      J

Tactic:
intro i _

Goal state after:
case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝¹ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
i : ℕ
a✝ : i ∈ Finset.range #J
⊢ {x ∈ (logSizeBallSeq J hJ a c i).finset |
      edist (logSizeBallSeq J hJ a c i).point x ≤ (↑(logSizeBallSeq J hJ a c i).radius - 1) * c} ⊆
    J
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
h :
  ((3 ^ n1)⁻¹ * ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((3 ^ n1)⁻¹ * ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * (3⁻¹ * (3 ^ n1)⁻¹)
⊢ (ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ = (ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹

Tactic:
rw [← mul_right_inj' (show ((3 : ℝ) ^ n1)⁻¹ ≠ 0 by positivity)]

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
h :
  ((3 ^ n1)⁻¹ * ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((3 ^ n1)⁻¹ * ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * (3⁻¹ * (3 ^ n1)⁻¹)
⊢ (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹) =
    (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
this : List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)

Tactic:
simpa only [functor_norm] using! this

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
this : ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v ∧ sequence v ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y

Tactic:
rcases this with ⟨v, hv, hvs⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u : List (Set α)
hu : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u
hus : sequence u ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
⊢ ∀ᶠ (y : List α) in traverse 𝓝 l, s ∈ traverse 𝓝 y
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertIdx a i ⟨l, hl⟩))

Tactic:
by
    rw [insertIdx, tendsto_subtype_rng]
    simp only [insertIdx_val]
    exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
| 1

Tactic:
rw [← one_pow n]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
| 1 ^ n
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ 1 ≤ #J

Tactic:
· rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]

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

Goal state before:
pp: case mpr.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ eHolderNorm r f = 0

Tactic:
← eHolderNorm_const X r (f hX.some)

Goal state after:
case mpr.inr
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (x₁ x₂ : X), f x₁ = f x₂
hX : Nonempty X
⊢ eHolderNorm r f = eHolderNorm r (Function.const X (f hX.some))
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ ‖c‖₊ • edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r

Tactic:
← edist_smul₀,

Goal state after:
case pos.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (c • f x₁) (c • f x₂) ≤ ↑(nnHolderNorm r (c • f)) * edist x₁ x₂ ^ ↑r
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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝ : IsCompact s
this : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
⊢ hausdorffDist (Subtype.val '' range Φ') (range (Subtype.val ∘ Ψ')) = hausdorffDist (range Φ') (range Ψ')

Tactic:
range_comp

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝ : IsCompact s
this : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
⊢ hausdorffDist (Subtype.val '' range Φ') (Subtype.val '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ OrderDual.instTopologicalSpace = lowerSet αᵒᵈ

Tactic:
by ext; rw [IsUpperSet.topology_eq α]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[inst✝¹] sᶜ ↔ IsLowerSet s

Tactic:
isOpen_iff_isUpperSet,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsUpperSet sᶜ ↔ IsLowerSet s
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

Tactic:
simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
    toUpperSet_le_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen[inst✝²] u
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Tactic:
exact ⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD),
      fun t h₀ hd₁ hd₂ a hd₃ ha ↦ image_inter_nonempty_iff.mp <|
        (isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
        (directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
rcases eq_empty_or_nonempty Uᶜ with eUc | neUc

Goal state after:
case mp.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
eUc : Uᶜ = ∅
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U

case mp.inr
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
hU : IsOpen[inst✝¹] U
neUc : Uᶜ.Nonempty
⊢ U = univ ∨ ∃ a, (Iic a)ᶜ = U
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

pp: case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
· convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]

Goal state after:
case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z
⊢ dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) = dist x y + dist y z

Tactic:
rw [x.toGHSpace_rep, y.toGHSpace_rep, z.toGHSpace_rep]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h :
  ∀ (U : Opens ↑X) (t : ToType (𝒢.obj (op U))),
    ∀ x ∈ U, ∃ V, ∃ (x_1 : V ≤ U), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V
U✝ : Opens ↑X
s : ToType (𝒢.obj (op U✝))
x : ↑X
hx : x ∈ U✝
⊢ ∃ U f, (Presheaf.imageSieve T s).arrows f ∧ x ∈ U

Tactic:
obtain ⟨V, Vle, hV⟩ := h _ s x hx
    exact ⟨V, homOfLE Vle, hV⟩

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

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∉ unop U
⊢ Epi ((skyscraperSheaf p₀ A).obj.map r)

Tactic:
· have h2 : p₀ ∉ unop V := fun hV => h1 (r.unop.le hV)
      have := isIso_of_isTerminal (isTerminalSkyscraperSheafObjObjOfNotMem h1)
        (isTerminalSkyscraperSheafObjObjOfNotMem h2) ((skyscraperSheaf p₀ A).obj.map r)
      infer_instance

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

Goal state before:
pp: case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (id i.1 ∩ id i.2)

Tactic:
· dsimp
    rintro _ ⟨⟨_, _, _⟩, _, _, _⟩
    infer_instance

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

Goal state before:
pp: case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (id i.1 ∩ id i.2)

Tactic:
· dsimp
    rintro _ ⟨⟨_, _, _⟩, _, _, _⟩
    infer_instance

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
x✝¹ : SetRel X X
x✝ : x✝¹ ∈ 𝓤 X ∧ x✝¹.IsSymm ∧ x✝¹.IsTrans
left✝ : x✝¹ ∈ 𝓤 X
hU : x✝¹.IsSymm
right✝ : x✝¹.IsTrans
⊢ SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id x✝¹)

Tactic:
rw [id_eq]; infer_instance

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
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
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha

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
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
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b