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

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : CompleteSpace A
s : Set 𝕜
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)})

Tactic:
refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_

Goal state after:
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : CompleteSpace A
s : Set 𝕜
x✝¹ : (𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜) × A
f : 𝕜 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] 𝕜
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : p (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum 𝕜 (f, a).2)
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
              {a | p a ∧ s ∈ 𝓝ˢ (quasispectrum 𝕜 a)} ∩
            t)
Module: Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A₁
inst✝⁵ : NonUnitalCStarAlgebra A₂
inst✝⁴ : PartialOrder A₁
inst✝³ : PartialOrder A₂
inst✝² : StarOrderedRing A₁
inst✝¹ : StarOrderedRing A₂
n : Type u_3
inst✝ : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
hmain : 0 ≤ (mapₗ ↑φ) ((reindexₐ ℂ A₁ e) M)
⊢ 0 ≤ M.map ⇑φ

Tactic:
rw [← mapₗ_reindexₐ] at hmain

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A₁
inst✝⁵ : NonUnitalCStarAlgebra A₂
inst✝⁴ : PartialOrder A₁
inst✝³ : PartialOrder A₂
inst✝² : StarOrderedRing A₁
inst✝¹ : StarOrderedRing A₂
n : Type u_3
inst✝ : Fintype n
φ : A₁ →CP A₂
M : CStarMatrix n n A₁
hM : 0 ≤ M
k : ℕ := Fintype.card n
e : n ≃ Fin (Fintype.card n) := Fintype.equivFinOfCardEq ⋯
hmain : 0 ≤ (reindexₐ ℂ A₂ e) ((mapₗ ↑φ) M)
⊢ 0 ≤ M.map ⇑φ
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case e_a.e_a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ 1 - cfc g (ε⁻¹ ^ 2 • m) = cfc (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) m

Tactic:
rw [← cfc_one (R := ℝ≥0) m, ← cfc_comp_smul _ _ _ hg.continuousOn hm₁,
    ← cfc_tsub _ _ m (by simp [g]) hm₁ (by fun_prop) (Continuous.continuousOn <| by fun_prop)]

Goal state after:
case e_a.e_a
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
⊢ cfc (fun x ↦ 1 x - g (ε⁻¹ ^ 2 • x)) m = cfc (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) m
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) (f * g)) b

Tactic:
rw [map_mul]

Goal state after:
case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) f * (cfcHom ha) g) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : 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✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) (f * g)) b

Tactic:
rw [map_mul]

Goal state after:
case mul
𝕜 : 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✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) f * (cfcₙHom ha) g) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)})

Tactic:
refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_

Goal state after:
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
x✝¹ : (ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0) × A
f : ℝ≥0 →ᵤ[{t | IsCompact t ∧ t ⊆ s}] ℝ≥0
a : A
x✝ :
  (f, a) ∈
    {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)}
hf : (f, a).1 ∈ {f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0}
ha : 0 ≤ (f, a).2
has : s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (f, a).2)
⊢ ∃ t,
    IsOpen[instTopologicalSpaceProd] t ∧
      (f, a) ∈ t ∧
        ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
          ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ
              {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)} ∩
            t)
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ ((WithCStarModule.equiv A (m → A)) x ᵥ* (c • M)) i = c • ((WithCStarModule.equiv A (m → A)) x ᵥ* M) i

Tactic:
rw [Matrix.vecMul_smul, Pi.smul_apply]

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
cfc_eq_cfcL_mkD _ a,

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
⊢ (cfcL ha) (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) =
    ∫ (x : X), (cfcL ha) (mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) ∂μ
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
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n A)

Tactic:
have :
    (fun x : CStarMatrix m n A × CStarMatrix m n A => ⟨ofMatrix.symm x.1, ofMatrix.symm x.2⟩)
      = id := by
    ext i <;> rfl
  rw [← uniformInducing_toMatrixAux.comap_uniformity, this, Filter.comap_id]
  rfl

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : 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✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
⊢ cfc (fun z ↦ ↑z.re + I * ↑z.im) a = ↑(ℜ a) + I • ↑(ℑ a)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(Y.mem_orthogonal' z).mp hz

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
⊢ 0 = 0

case a
𝕜 : 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
⊢ ℓ z • x - ℓ x • z ∈ Y
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ (s.openPartialHomeomorphSubtypeCoe hs).symm.trans (s.openPartialHomeomorphSubtypeCoe hs) ≈ ofSet (↑s) openness₂

Tactic:
refine Setoid.trans (symm_trans_self (s.openPartialHomeomorphSubtypeCoe hs)) ?_

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : OpenPartialHomeomorph X Y
openness₁ : IsOpen[inst✝] (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen[inst✝¹] ↑s
⊢ ofSet (s.openPartialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s) openness₂
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
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
hb : b ∈ e'.baseSet
⊢ (↑e' { proj := b, snd := y }).1 = b

Tactic:
by
  simp [hb]

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
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)
z : Z
hzp : proj z ∈ s
hze : ⟨z, hzp⟩ ∈ e.source
⊢ (if h : proj ↑⟨z, hzp⟩ ∈ s then ↑e ⟨↑⟨z, hzp⟩, h⟩ else (proj ↑⟨z, hzp⟩, Classical.arbitrary (Z → F) ↑⟨z, hzp⟩)).1 =
    proj ↑⟨z, hzp⟩

Tactic:
simp [hzp, e.coe_fst hze]

Goal state after:
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).1 = (↑e₂ (↑e₁.symm (b, x))).1

Tactic:
e₂.coe_fst',

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 = proj (↑e₁.symm (b, x))

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
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_1
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝¹ : f x₁ = f x₂
x✝ : x₁ ≠ x₂
h : ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
⊢ (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)

pp: case refine_2
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝² : f x₁ = f x₂
x✝¹ : x₁ ≠ x₂
x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
t : Set (X × X)
ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
· simp_rw [← Filter.disjoint_iff, ← compl_diagonal_mem_prod] at h
    exact ⟨_, h, subset_rfl⟩

Goal state after:
case refine_2
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝² : f x₁ = f x₂
x✝¹ : x₁ ≠ x₂
x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
t : Set (X × X)
ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂
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
n : ℕ
x y : A
⊢ ↑n x * y = x * ↑n y

Tactic:
simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
        smul_mul_assoc]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
⊢ ∀ u ∈ {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, IsOpen[inst✝¹] u

Tactic:
rintro _ ⟨U, hU, s, hs, rfl⟩

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
U : Set Y
hU : IsOpen[inst✝] U
s : C(↑U, X)
hs : f ∘ ⇑s = Subtype.val
⊢ IsOpen[inst✝¹] (Set.range ⇑s)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r x : ℝ
hx : x ∈ {x | |x| < r}
⊢ 0 < r

Tactic:
exact (abs_nonneg x).trans_lt hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ {x}ᶜ

Tactic:
rintro z ⟨t, ht, rfl⟩

Goal state after:
x y : Circle
h : x ≠ y
t : ↑unitInterval
ht : t ∈ Ioo 0 1
⊢ (y.path x) t ∈ {x}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ range ⇑(x.path y) ⊂ univ

Tactic:
rw [ssubset_univ_iff_nonempty_compl]
  obtain rfl | hne := eq_or_ne x y
  · use -x, by simp [neg_ne_self]
  rw [compl_range_path hne]
  use y.path x ⟨2⁻¹, by simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]; linarith⟩
  refine mem_image_of_mem _ ⟨by simp [← unitInterval.coe_pos], unitInterval.coe_lt_one.mp ?_⟩
  linarith

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 F - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range

Tactic:
rw [← A.adjoint.ker.finrank_add_finrank_orthogonal,
    orthogonal_ker, adjoint_adjoint]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 ↥(adjoint A).ker + finrank 𝕜 ↥A.range - finrank 𝕜 ↥(adjoint A).ker = finrank 𝕜 ↥A.range
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
y : P
⊢ ε / ‖y -ᵥ q‖ * ‖y -ᵥ q‖ ≤ ε

Tactic:
div_mul_comm

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
y : P
⊢ ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Collinear k {p}

Tactic:
rw [collinear_iff_rank_le_one, vectorSpan_singleton]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Module.rank k ↥⊥ ≤ 1
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) (range Subtype.val))).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
Subtype.range_coe_subtype,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) {x | x ∈ t})).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
⊢ ‖lp.single (↑p) i x‖ = ‖x‖

Tactic:
have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp' hp

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
hp : p ≠ ∞
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : (a : α) → E a
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 f)
s : Finset α
hp' : p ≠ 0
hp'' : 0 < p.toReal
⊢ ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal