mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent (ι := ↑(MaxProducts C ho')) ℤ
    (⇑(CategoryTheory.ConcreteCategory.hom
          { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
              X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho') ℤ),
              f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho'), zero := ⋯ }.g) ∘
      SumEval C ho' ∘ Sum.inr)

Tactic:
· exact linearIndependent_comp_of_eval C hC hsC ho' (span (π C (ord I · < o))
      (isClosed_proj C o hC)) (h (le_of_lt ho') (C' C ho') (isClosed_C' C hC ho')
      (contained_C' C ho'))

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

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
simp [image_eq_zero_of_notMem_tsupport hy]

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflLeft p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((const (Path x x) (refl x)).prodMk (ContinuousMap.id (Path x x))))
          x_1

Tactic:
rintro t _ rfl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
t : ↑I
⊢ { toFun := fun x_1 ↦ (fun p ↦ delayReflLeft p.1 p.2) (t, x_1), continuous_toFun := ⋯ } (refl x) =
    ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
        ((const (Path x x) (refl x)).prodMk (ContinuousMap.id (Path x x))))
      (refl x)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflRight p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (Path x x)).prodMk (const (Path x x) (refl x))))
          x_1

Tactic:
rintro t _ rfl

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
t : ↑I
⊢ { toFun := fun x_1 ↦ (fun p ↦ delayReflRight p.1 p.2) (t, x_1), continuous_toFun := ⋯ } (refl x) =
    ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (Path x x)).prodMk (const (Path x x) (refl x))))
      (refl x)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero
⊢ 1 / 4 ∈ preCantorSet 0 ∧ 3 / 4 ∈ preCantorSet 0

Tactic:
simp only [preCantorSet_zero]

Goal state after:
case zero
⊢ 1 / 4 ∈ Set.Icc 0 1 ∧ 3 / 4 ∈ Set.Icc 0 1
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
j : ↑S
hj : ↑j ∈ S
⊢ reorderRestrictProd S s p ↑j = p.2 j

Tactic:
simp [reorderRestrictProd, hj]

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
j : ↑Sᶜ
hj : ↑j ∉ S
⊢ reorderRestrictProd S s p ↑j = ↑p.1 j

Tactic:
simp [reorderRestrictProd, hj]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_1.nil
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ pure [] ≤ traverse 𝓝 []

Tactic:
exact le_rfl

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b ↦ (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
exact le_rfl

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

Goal state before:
pp: case h
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := ⋯
l : ℕ := ⋯
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
hsB : s ∈ (logSizeBallSeq J hJ a c l).ball c
htB : t ∈ (logSizeBallSeq J hJ a c l).ball c
hsP : ((logSizeBallSeq J hJ a c l).point, s) ∈ pairSetSeq J a c l
htP : ((logSizeBallSeq J hJ a c l).point, t) ∈ pairSetSeq J a c l
x y : T
hxy : (x, y) ∈ pairSetSeq J a c l
⊢ edist (f x) (f y) ≤ edist (f (x, y).1) (f (x, y).2)

Tactic:
exact le_rfl

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

Goal state before:
pp: case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
⊢ ∃ f, Isometry f

Tactic:
rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩

Goal state after:
case inr
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε) C
h : packingNumber ε A ≠ ⊤
⊢ C.encard ≤ (maximalSeparatedSet ε A).encard

Tactic:
by
  rw [encard_maximalSeparatedSet h]
  exact le_iSup_of_le C <| le_iSup_of_le h_subset <| le_iSup_of_le h_sep (by simp)

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case neg.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ IsOpen[inst✝²] (V ∩ ⋂ U ∈ S, interior Uᶜ)

pp: case neg.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x

pp: case neg.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
U : Set X
hU : U ∈ S
⊢ Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
· exact hVo.inter (isOpen_biInter_finset fun _ _ ↦ isOpen_interior)

Goal state after:
case neg.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
⊢ (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x

case neg.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
U : Set X
hU : U ∈ S
⊢ Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ 𝓝 a = 𝓟 (Ici a)

Tactic:
rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ 𝓝 a = 𝓟 (Iic a)

Tactic:
rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

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
x : X
this : f (inl x) ∈ ↑p
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
⊢ ⨅ y, Fb (inl x, inr y) ≤ r

Tactic:
have : z ∈ range Ψ := by rwa [← Ψrange] at zq

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
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
x : X
this✝ : f (inl x) ∈ ↑p
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑q
hz : dist (f (inl x)) z < r
this : z ∈ range Ψ
⊢ ⨅ y, Fb (inl x, inr y) ≤ r
Module: Mathlib.Topology.Sion

Goal state before:
pp: case insert
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
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

Tactic:
let X' := X ∩ (fun x ↦ f x b) ⁻¹' Iic t

Goal state after:
case insert
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
hrec :
  ∀ {X : Set E},
    X.Nonempty →
      IsCompact X →
        (∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X) →
          (∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y) →
            (∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y) →
              (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y) →
                Convex ℝ X → s ⊆ Y → (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
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
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsSymm (⋂ i_1, id (i.snd i_1))

Tactic:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]

Goal state after:
case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    i.fst.Finite →
      (∀ (a : ι) (b : a ∈ i.fst), i.snd ⟨a, b⟩ ∈ uniformity X) →
        (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsSymm) →
          (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsTrans) →
            SetRel.IsSymm (⋂ i_1, ⋂ (h : i_1 ∈ i.fst), i.snd ⟨i_1, h⟩)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsTrans (⋂ i_1, id (i.snd i_1))

Tactic:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]

Goal state after:
case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    i.fst.Finite →
      (∀ (a : ι) (b : a ∈ i.fst), i.snd ⟨a, b⟩ ∈ uniformity X) →
        (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsSymm) →
          (∀ (a : ι) (b : a ∈ i.fst), (i.snd ⟨a, b⟩).IsTrans) →
            SetRel.IsTrans (⋂ i_1, ⋂ (h : i_1 ∈ i.fst), i.snd ⟨i_1, h⟩)
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝¹⁸ : NontriviallyNormedField 𝕜
B₁ : Type u_3
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 B₁
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹¹ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹⁰ : FiberBundle F₁ E₁
inst✝⁹ : VectorBundle 𝕜 F₁ E₁
B₂ : Type u_6
F₂ : Type u_7
inst✝⁸ : NormedAddCommGroup F₂
inst✝⁷ : NormedSpace 𝕜 F₂
E₂ : B₂ → Type u_8
inst✝⁶ : (x : B₂) → AddCommGroup (E₂ x)
inst✝⁵ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝⁴ : TopologicalSpace B₂
inst✝³ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝² : (x : B₂) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
x₀ x : B₁
y₀ y : B₂
ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y
hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet
x✝ : ι → F₁
⊢ (inCoordinates F₁ F₂ x₀ x y₀ y ϕ) x✝ =
    (((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
            ϕ).compContinuousLinearMap
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm)
      x✝

Tactic:
simp [inCoordinates, *, Function.comp_def]

Goal state after: