mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ℓ z • x - ℓ x • z ∈ Y
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ℓ z • x - ℓ x • z ∈ Y
h₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_4
M : ι → Type u_5
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module 𝕜 (M i)
s : (i : ι) → Set (M i)
⊢ extremePoints 𝕜 (univ.pi s) = univ.pi fun i ↦ extremePoints 𝕜 (s i)

Tactic:
by
  classical
  ext x
  simp only [mem_extremePoints_iff_left, mem_univ_pi, @forall_and ι]
  refine and_congr_right fun hx ↦ ⟨fun h i ↦ ?_, fun h ↦ ?_⟩
  · rintro x₁ hx₁ x₂ hx₂ hi
    rw [← update_self i x₁ x, h (update x i x₁) _ (update x i x₂)]
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
    · rw [← Pi.image_update_openSegment]
      exact ⟨_, hi, update_eq_self _ _⟩
    · rintro j
      obtain rfl | hji := eq_or_ne j i <;> simp [*]
  · rintro x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, rfl⟩
    ext i
    exact h _ _ (hx₁ _) _ (hx₂ _) ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ((innerₛₗ 𝕜) 0).toAddMonoidHom x = 0 x

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ((innerₛₗ 𝕜) 0).toAddMonoidHom x = 0 x
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ((innerₛₗ 𝕜) (x + y)).toAddMonoidHom z = (((innerₛₗ 𝕜) x).toAddMonoidHom + ((innerₛₗ 𝕜) y).toAddMonoidHom) z

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ((innerₛₗ 𝕜) (x + y)).toAddMonoidHom z = (((innerₛₗ 𝕜) x).toAddMonoidHom + ((innerₛₗ 𝕜) y).toAddMonoidHom) z
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
c : R₁
a : Completion α
⊢ Continuous fun a ↦ σ c • ((↑f).toAddMonoidHom.extension ⋯) a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
c : R₁
a : Completion α
⊢ Continuous fun a ↦ σ c • ((↑f).toAddMonoidHom.extension ⋯) a
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
g : Completion α →SL[σ] β
h : ∀ (e : α), f e = g ↑e
x✝ : Completion α
⊢ f.fromCompletion x✝ = g x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : UniformSpace α
inst✝¹² : AddCommGroup α
inst✝¹¹ : IsUniformAddGroup α
inst✝¹⁰ : Semiring R₁
inst✝⁹ : Module R₁ α
inst✝⁸ : UniformContinuousConstSMul R₁ α
inst✝⁷ : Semiring R₂
inst✝⁶ : UniformSpace β
inst✝⁵ : AddCommGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : Module R₂ β
inst✝² : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
g : Completion α →SL[σ] β
h : ∀ (e : α), f e = g ↑e
x✝ : Completion α
⊢ f.fromCompletion x✝ = g x✝
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
this : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤ ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x
⊢ f
      (star (f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) *
        f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) ≤
    ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)

Tactic:
calc
      _ ≤ f (‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x) := by
        simpa using OrderHomClass.mono f this
      _ = _ := by simp [← Complex.coe_smul, preGNS_norm_sq, smul_mul_assoc]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a b : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (a * b)) c = (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b) c

Tactic:
;

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a b : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (a * b)) c = (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b) c
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
;

Goal state after:
x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
by
  classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast ⋯ b) = { proj := x, snd := b }

Tactic:
;

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast ⋯ b) = { proj := x, snd := b }
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖

Tactic:
;

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖T‖ * ‖toLp 2 (Pi.single i 1)‖ ≤ ‖T‖
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_2
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
⊢ EqOn (↑e' ∘ ↑e.symm) (↑((e.symm.trans e').restr (↑e '' s))) ((e.restr s).symm.trans e').source

Tactic:
restr_apply,

Goal state after:
case refine_2
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
⊢ EqOn (↑e' ∘ ↑e.symm) (↑(e.symm.trans e')) ((e.restr s).symm.trans e').source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case pos
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)

pp: case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)

Tactic:
;

Goal state after:
case pos
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)

case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
x : X'
hx : x ∈ f '' e.source
⊢ ContinuousWithinAt (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source) x

Tactic:
;

Goal state after:
case neg
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : ¬Nonempty X
x : X'
hx : x ∈ f '' e.source
⊢ ContinuousWithinAt (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source) x
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hf
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := ⋯
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

pp: case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := ⋯
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source) e.source

Tactic:
;

Goal state after:
case hf
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := ⋯
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)

case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := ⋯
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
⊢ MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source) e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source

Tactic:
;

Goal state after:
case h
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
h✝ : Nonempty X
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hs
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
x✝ : z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = (f ∘ ↑e.symm) z
⊢ ↑e.symm z ∈ e'.source

Tactic:
;

Goal state after:
case hs
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
x✝ : z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = (f ∘ ↑e.symm) z
⊢ ↑e.symm z ∈ e'.source
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
a✝ : ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀
⊢ ContinuousWithinAt (fun x ↦ x) a x₀

Tactic:
;

Goal state after:
B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
a : Set B
x₀ : B
a✝ : ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) (TotalSpace.mk' F x (s x))).2) a x₀
⊢ ContinuousWithinAt (fun x ↦ x) a x₀
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContinuousWithinAt (fun x ↦ TotalSpace.mk' F x (s x)) univ x₀ ↔
    ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) univ x₀

Tactic:
;

Goal state after:
B : Type u_2
F : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
s : (x : B) → E x
x₀ : B
⊢ ContinuousWithinAt (fun x ↦ TotalSpace.mk' F x (s x)) univ x₀ ↔
    ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) univ x₀
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen[instTopologicalSpaceProd] toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝¹] baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ p).1 = proj p
h₁ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toPartialEquiv =
    e'.toPartialEquiv
h₂ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'

Tactic:
;

Goal state after:
case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen[instTopologicalSpaceProd] toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝¹] baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ p).1 = proj p
h₁ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toPartialEquiv =
    e'.toPartialEquiv
h₂ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'
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
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
← PartialEquiv.symm_source,

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).symm.source = (e.baseSet ∩ e'.baseSet) ×ˢ univ
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case neg
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
d' : B
hdd' : d' < d
hd'c : d' ∈ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet

Tactic:
exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩

Goal state after: