mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) := ⋯
⊢ instUniformSpace m n 𝕜 = PseudoEMetricSpace.toUniformSpace

Tactic:
rw [← @IsUniformAddGroup.rightUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]

Goal state after:
case e_2
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ IsTopologicalAddGroup.rightUniformSpace (Matrix m n 𝕜) = PseudoEMetricSpace.toUniformSpace
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
  let __src := l2OpNormedAddCommGroupAux.replaceTopology ⋯;
  { toNorm := l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := addCommGroup, toMetricSpace := __src, dist_eq := ⋯ }
⊢ MetricSpace (Matrix m n 𝕜)

Tactic:
exact normed_add_comm_group.replaceUniformity <| by
    congr
    rw [← @IsUniformAddGroup.rightUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]
    rw [@IsUniformAddGroup.rightUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯

Tactic:
ext

Goal state after:
case h
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
x✝ : X
⊢ ↑((ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s')) x✝ = ↑(ofSet (s ∩ s') ⋯) x✝

case hinv
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
x✝ : X
⊢ ↑((ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s')).symm x✝ = ↑(ofSet (s ∩ s') ⋯).symm x✝

case hs
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
x✝ : X
⊢ x✝ ∈ ((ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s')).source ↔ x✝ ∈ (ofSet (s ∩ s') ⋯).source
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' interior s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e.symm ⁻¹' e'.source ∩ interior (↑e '' s)

Tactic:
interior_eq_iff_isOpen.mpr hs',

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' interior s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e '' s
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y

pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
· change domRestrict _ e _ = _
    rw [← e.subtypeRestr_coe hU, (e.subtypeRestr hU).right_inv hy]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∉ e.baseSet
⊢ e.symm b = fun x ↦ Classical.arbitrary (E b)

Tactic:
ext

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∉ e.baseSet
x✝ : F
⊢ e.symm b x✝ = Classical.arbitrary (E b)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source

case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j))) (↑(Z.trivChange i j).toPartialEquiv)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ e.target = e.baseSet ×ˢ univ

Tactic:
ext

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
x✝ : B × F
⊢ x✝ ∈ e.target ↔ x✝ ∈ e.baseSet ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
      (↑e
          (if h : (Prod.map Subtype.val id x).1 ∈ s then
            e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
          else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2) =
    Prod.map Subtype.val id x

Tactic:
ext

Goal state after:
case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).1 =
    (Prod.map Subtype.val id x).1

case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x : { x // x ∈ s } × F
hx : x ∈ e.target
⊢ (↑(↑e
              (if h : (Prod.map Subtype.val id x).1 ∈ s then
                e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
              else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).1,
        (↑e
            (if h : (Prod.map Subtype.val id x).1 ∈ s then
              e.invFun (⟨(Prod.map Subtype.val id x).1, h⟩, (Prod.map Subtype.val id x).2)
            else Classical.arbitrary (B → F → Z) (Prod.map Subtype.val id x).1 (Prod.map Subtype.val id x).2)).2).2 =
    (Prod.map Subtype.val id x).2
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
⊢ e.source = Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet

Tactic:
ext

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : Z
⊢ x✝ ∈ e.source ↔ x✝ ∈ Subtype.val ∘ proj ⁻¹' Subtype.val '' e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source = ⇑h ∘ proj ⁻¹' ⇑h.symm ⁻¹' e.baseSet

Tactic:
ext

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
x✝ : Z
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).source ↔ x✝ ∈ ⇑h ∘ proj ⁻¹' ⇑h.symm ⁻¹' e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
⊢ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target = (⇑h.symm ⁻¹' e.baseSet) ×ˢ univ

Tactic:
ext

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
B' : Type u_5
inst✝ : TopologicalSpace B'
h : B ≃ₜ B'
x✝ : B' × F
⊢ x✝ ∈ (e.transHomeomorph (h.prodCongr (Homeomorph.refl F))).target ↔ x✝ ∈ (⇑h.symm ⁻¹' e.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) (e.baseSet ×ˢ univ)

Tactic:
← e.target_eq

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) e.target
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))

Tactic:
refine Prod.ext ?_ rfl

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (↑e₂ (↑e₁.symm (b, x))).1
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst✝¹, inst✝¹] (e₁.coordChange e₂ b)

Tactic:
refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)

Goal state after:
case refine_1
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst✝¹, instTopologicalSpaceProd] (Prod.mk b)

case refine_2
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑e₁.symm (b, x) ∈ e₂.source
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ (∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U) → IsLocallyInjective f
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ (Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z =
    (↑e.toPartialEquiv ∘ Subtype.val) z

Tactic:
ext

Goal state after:
case fst
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).1 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).1

case snd
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
e : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).2 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).2
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case e'_5
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj✝ : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj✝
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝⁴] s
proj : Z → ↑s
e : Trivialization F proj
inst✝ : Nonempty (B → F → Z)
⊢ (Pretrivialization.codExtend' hs e.toPretrivialization).invFun ∘ Prod.map Subtype.val id = e.invFun

Tactic:
ext

Goal state after:
case e'_5
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj✝ : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj✝
x : Z
e' : Trivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝⁴] s
proj : Z → ↑s
e : Trivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : { x // x ∈ s } × F
⊢ ((Pretrivialization.codExtend' hs e.toPretrivialization).invFun ∘ Prod.map Subtype.val id) x✝ = e.invFun x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
x y : A
⊢ (a.toProd.2 - b.toProd.2) x * y = x * (a.toProd.1 - b.toProd.1) y

Tactic:
simp only [sub_apply, _root_.sub_mul, _root_.mul_sub, central]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝ : 𝓜(𝕜, A)
⊢ star (star x✝) = x✝

Tactic:
ext

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.1 x✝ = x✝¹.toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (star x✝¹)).toProd.2 x✝ = x✝¹.toProd.2 x✝
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
⊢ IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ x✝ : 𝓜(𝕜, A)
⊢ star (x✝¹ + x✝) = star x✝¹ + star x✝

Tactic:
ext

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.1 x✝ = (star x✝² + star x✝¹).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² + x✝¹)).toProd.2 x✝ = (star x✝² + star x✝¹).toProd.2 x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ x✝ : 𝓜(𝕜, A)
⊢ star (x✝¹ * x✝) = star x✝ * star x✝¹

Tactic:
ext

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.1 x✝ = (star x✝¹ * star x✝²).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² * x✝¹)).toProd.2 x✝ = (star x✝¹ * star x✝²).toProd.2 x✝
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝¹ : 𝕜
x✝ : 𝓜(𝕜, A)
⊢ star (x✝¹ • x✝) = star x✝¹ • star x✝

Tactic:
ext

Goal state after:
case fst
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.1 x✝ = (star x✝² • star x✝¹).toProd.1 x✝

case snd
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : StarRing 𝕜
inst✝² : StarRing A
inst✝¹ : StarModule 𝕜 A
inst✝ : NormedStarGroup A
x✝² : 𝕜
x✝¹ : 𝓜(𝕜, A)
x✝ : A
⊢ (star (x✝² • x✝¹)).toProd.2 x✝ = (star x✝² • star x✝¹).toProd.2 x✝