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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nontrivial N
h : ∃ y, y ≠ Classical.arbitrary N := exists_ne (Classical.arbitrary N)
⊢ ∀ (a b c d : HomotopyGroup N X x), Mul.mul (a * b) (c * d) = Mul.mul a c * Mul.mul b d

Tactic:
by
      rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩
      apply congr_arg Quotient.mk'
      simp only [fromLoop_trans_toLoop, transAt_distrib <| Classical.choose_spec h, coe_toEquiv,
        loopHomeo_apply, coe_symm_toEquiv, loopHomeo_symm_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ ∃ z' ∈ s (n + l + 1), edist (↑z) z' < B n / 2 ^ l

Tactic:
by
          refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
          simp only [ENNReal.inv_pow, div_eq_mul_inv]
          rw [← pow_add]
          apply hs <;> simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    ((((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
          ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
        ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
      ⋂ x, {f | f (x, x) = 0})

X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)})
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
          ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
        ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
      ⋂ x, {f | f (x, x) = 0})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    ((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
        ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
      ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)})

X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, {f | f (x, x) = 0})
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    ((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
        ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
      ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    (((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)})

X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)})
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    (((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed ((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y})

X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, {f | f (x, y) = f (y, x)})
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed ((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y})

X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y})
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos.refine_1
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
⊢ eHolderNorm r f * ↑‖c‖₊ ≤ ↑‖c‖₊ * eHolderNorm r f

Tactic:
mul_comm

Goal state after:
case pos.refine_1
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
⊢ ↑‖c‖₊ * eHolderNorm r f ≤ ↑‖c‖₊ * eHolderNorm r f
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed (⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ ∀ (i : X), IsClosed (⋂ y, {f | f (inl i, inl y) = dist i y})
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
    nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))

Goal state after:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun r ↦ 0 < r ∧ r < R x) fun r ↦ ball x r
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ ∀ (i : X), IsClosed (⋂ y, {f | f (inl i, inl y) = dist i y})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x : X
⊢ IsClosed (⋂ y, {f | f (inl x, inl y) = dist x y})
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x : X
⊢ IsClosed (⋂ y, {f | f (inl x, inl y) = dist x y})

Tactic:
first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

Goal state after:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
x : X
⊢ ∀ (i : X), IsClosed {f | f (inl x, inl i) = dist x i}
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ univ ∉ S

Tactic:
by_contra hUS'

Goal state after:
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ False