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

Goal state before:
pp: A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute ((cfcHom ha) { toFun := (spectrum ℝ a).domRestrict f, continuous_toFun := ⋯ }) b

Tactic:
← cfc_apply ..

Goal state after:
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute (cfc f a) b
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: n : Type u_2
A : Type u_5
inst✝ : Star A
f : CStarMatrix n n A
i j : n
⊢ star f i j = star (f j i)

Tactic:
star_eq_conjTranspose,

Goal state after:
n : Type u_2
A : Type u_5
inst✝ : Star A
f : CStarMatrix n n A
i j : n
⊢ f.conjTranspose i j = star (f j i)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
| 2⁻¹ • (cfcₙ (fun x ↦ x) a + cfcₙ (fun x ↦ star x) a)

Tactic:
← cfcₙ_add ..,

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
| 2⁻¹ • cfcₙ (fun x ↦ x + star x) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
suffices cfcₙ (fun z : ℂ ↦ re z + I * im z) a = ℜ a + I • ℑ a by
    rw [cfcₙ_add .., cfcₙ_const_mul .., cfcₙ_re_id a] at this
    simpa

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ cfcₙ (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
⊢ ‖M‖ ≤ ↑C

Tactic:
refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_
  obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt
  · rw [← h₀]
    positivity
  · refine le_of_mul_le_mul_right ?_ h₀
    simpa [← sq, norm_sq_eq A] using h ..

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖M‖ ≤ ↑(↑(Fintype.card n) * ↑(Fintype.card m)) * ‖ofMatrixₗ.symm M‖

Tactic:
calc
    ‖M‖ ≤ ∑ j, ∑ i, ‖M i j‖ := by
      rw [norm_def]
      refine (toCLM M).opNorm_le_bound (by positivity) fun v => ?_
      simp only [toCLM_apply_eq_sum, Finset.sum_mul]
      apply pi_norm_le_sum_norm _ |>.trans
      gcongr with i _
      apply norm_sum_le _ _ |>.trans
      gcongr with j _
      apply norm_mul_le _ _ |>.trans
      rw [mul_comm]
      gcongr
      exact norm_apply_le_norm v j
    _ ≤ ∑ _ : n, ∑ _ : m, ‖ofMatrixₗ.symm (R := ℂ) M‖ := by
      gcongr with j _ i _
      exact ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm
    _ = _ := by simp [mul_assoc]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (Set.range fun x ↦ cfcₙ x a) = ↑(elemental 𝕜 a)

Tactic:
range_cfcₙ_eq_range_cfcₙHom 𝕜 ha,

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ ↑(NonUnitalStarAlgHom.range (cfcₙHom ha)) = ↑(elemental 𝕜 a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (Set.range fun x ↦ cfcₙ x a) ⊆ ↑(elemental 𝕜 a)

Tactic:
range_cfcₙ_eq_range_cfcₙHom 𝕜 ha,

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : Module 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousConstSMul 𝕜 A
inst✝³ : StarModule 𝕜 A
inst✝² : IsTopologicalRing A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ ↑(NonUnitalStarAlgHom.range (cfcₙHom ha)) ⊆ ↑(elemental 𝕜 a)
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
⊢ ‖(InnerProductSpace.toDual ℝ E).symm L‖ ^ 2 = ∑ i, L (b i) ^ 2

Tactic:
← b.sum_sq_inner_left,

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
⊢ ∑ i, inner ℝ ((InnerProductSpace.toDual ℝ E).symm L) (b i) ^ 2 = ∑ i, L (b i) ^ 2
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 α
⊢ ∀ (a : α), (↑((↑f).toAddMonoidHom.extension ⋯)).toFun (c • ↑a) = σ c • (↑((↑f).toAddMonoidHom.extension ⋯)).toFun ↑a

Tactic:
by
    simp [← Completion.coe_smul, AddMonoidHom.extension_coe f.toAddMonoidHom f.continuous]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ = ‖a‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity)]

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ ^ 2 = ‖a‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
m : ℂ
x : A
a : Completion f.PreGNS
⊢ (f.leftMulMapPreGNS (m • x)).completion a = (m • (f.leftMulMapPreGNS x).completion) a

Tactic:
induction a using induction_on with

Goal state after:
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
x✝ : F
⊢ e.symm b x✝ = Classical.arbitrary (E b)

Tactic:
exact symm_apply_of_notMem e hb _

Goal state after:
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 : ι
p : B × F
⊢ p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j

Tactic:
trivChange,

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p ∈
      { toFun := fun p ↦ (p.1, Z.coordChange i j p.1 p.2), invFun := fun p ↦ (p.1, Z.coordChange j i p.1 p.2),
          source := (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ, target := (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ,
          map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, continuousOn_toFun := ⋯,
          continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯ }.source ↔
    p.1 ∈ Z.baseSet i ∩ Z.baseSet j
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : x ∈ Prod.map Subtype.val id ⁻¹' e.target
⊢ (if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2) ∈
    Subtype.val ⁻¹' e.source

Tactic:
simp only [mem_preimage, (Prod.map_apply), id_eq] at hx

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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2) ∈
    Subtype.val ⁻¹' e.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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (if h : (proj ↑z, (↑e ↑z).2) ∈ e.target then ⟨e.invFun (proj ↑z, (↑e ↑z).2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) ⟨proj ↑z, ⋯⟩ (↑e ↑z).2) =
    z

Tactic:
rw [dif_pos] <;> all_goals simp_rw [← e.proj_toFun _ hz]

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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ ⟨e.invFun ((↑e.toPartialEquiv ↑z).1, (↑e ↑z).2), ⋯⟩ = z

case hc
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ ((↑e.toPartialEquiv ↑z).1, (↑e ↑z).2) ∈ e.target
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : x ∈ Prod.map Subtype.val id ⁻¹' e.target
⊢ Prod.map Subtype.val id
      (⟨proj
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
          ⋯⟩,
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x

Tactic:
simp only [mem_preimage, (Prod.map_apply), id_eq] at hx

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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ Prod.map Subtype.val id
      (⟨proj
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
          ⋯⟩,
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))

Tactic:
have : IsOpen (f.source ∩ f ⁻¹' s) := by
      rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
      exact (continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ ↑f ⁻¹' s)
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x ⊓ 𝓟 (TotalSpace.mk b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ

pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ

Tactic:
· congr
      exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _)

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source

Tactic:
refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = e'.setSymm ⁻¹' e.source
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case refine_3
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ (↑e z).1 ∈ s ∩ (a.pretrivializationAt z.proj).baseSet

Tactic:
rw [e.coe_fst]

Goal state after:
case refine_3
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z.proj ∈ s ∩ (a.pretrivializationAt z.proj).baseSet

case refine_3
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z ∈ e.source
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
⊢ ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source

Tactic:
refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
    fun y hy ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑((gf.restr (f ⁻¹' g.source)).trans g.symm) y
Module: Mathlib.Topology.IsLocalHomeomorph

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

Tactic:
isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorphOn f Set.univ ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ t₁ = t₂

Tactic:
rw [← sub_eq_zero, ← cos_eq_one_iff_of_lt_of_lt h1 h2, ← exp_ofReal_mul_I_re]

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
heq : exp t₁ = exp t₂
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp (↑t₁ * I) = cexp (↑t₂ * I)
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
rw [exp_eq_exp_iff_exp_sub_eq_one, ← sub_mul, ← ofReal_sub, Complex.ext_iff] at heq

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : (cexp (↑(t₁ - t₂) * I)).re = re 1 ∧ (cexp (↑(t₁ - t₂) * I)).im = im 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (↑x).arg < x.angleDiff y + (↑x).arg

Tactic:
simp [angleDiff_pos h]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) ≤ ‖↑u - 1‖ ^ 2

Tactic:
exact (two_mul_one_sub_cos_norm_argSelfAdjoint hu).le

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ContinuousOn (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) (ball 1 2)

Tactic:
rw [isOpen_ball.continuousOn_iff]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ∀ ⦃a : ↥(unitary A)⦄, a ∈ ball 1 2 → ContinuousAt (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) a