mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ * x⁻) a = 0

Tactic:
← cfcₙ_zero ℝ a

Goal state after:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ * x⁻) a = cfcₙ 0 a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁻ * x⁺) a = 0

Tactic:
← cfcₙ_zero ℝ a

Goal state after:
case pos
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁻ * x⁺) a = cfcₙ 0 a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
obtain (hf | ha) := not_and_or.mp h

Goal state after:
case neg.inl
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ ↑(cfcₙ f a) = cfc f ↑a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case const
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this✝ : CompactSpace ↑s
r : 𝕜
this : ContinuousMap.const (↑s) r = (algebraMap 𝕜 C(↑s, 𝕜)) r
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦
    (cfcHomSuperset ⋯ ⋯) (ContinuousMap.const (↑s) r)

Tactic:
simpa only [this, AlgHomClass.commutes] using! continuous_const

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
⊢ ‖a‖₊ ≤ 1 ↔ a ≤ 1

Tactic:
rw [← NNReal.coe_le_coe]
  exact norm_le_one_iff_of_nonneg a

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n

Tactic:
rw [CFC.le_one_iff (R := ℝ) a] at ha₁

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha₀ : 0 ≤ a
ha₁ : ∀ x ∈ spectrum ℝ a, x ≤ 1
n m : ℕ
hnm : n ≤ m
⊢ ∀ x ∈ spectrum ℝ a, x ^ m ≤ x ^ n
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:

Tactic:
‖x‖ ^ 2 ≤ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ := prod_norm_sq x ▸ norm_add_le _ _
    _ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2 := by simp [norm_sq_eq A]
    _ ≤ ‖x.1‖ ^ 2 + 2 * ‖x.1‖ * ‖x.2‖ + ‖x.2‖ ^ 2 := by gcongr; positivity
    _ = (‖x.1‖ + ‖x.2‖) ^ 2 := by ring

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

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹⁰ : NormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedAlgebra ℝ A
inst✝⁷ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : ContinuousStar A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn (fun x ↦ cfc f (a x)) Set.univ

Tactic:
exact ha_cont.cfc_nnreal f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using ha x) (fun x _ ↦ ha' x)

Goal state after:
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 (n → 𝕜)) = ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
Pi.uniformity,

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 𝕜)) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}

Tactic:
have h₂ := lipschitzWith_one_ofFun_toFun' (𝔖 := {quasispectrum R a}) (𝔗 := {s}) (β := R)
    (by simpa)

Goal state after:
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : quasispectrum R a ⊆ s
h₂ : LipschitzWith 1 (⇑(ofFun {quasispectrum R a}) ∘ ⇑(toFun {s}))
⊢ LipschitzOnWith 1 (fun f ↦ cfcₙ ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s ∧ f 0 = 0}
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖diagonal v‖₊ = ‖toLp 2 v‖₊

Tactic:
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ,
    PiLp.nnnorm_eq_of_L2]

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (∑ x, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ x, ‖v x‖₊ ^ 2)
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 n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
⊢ (mapₗ ↑f) 0 = 0

Tactic:
simp [map_zero]

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

Goal state before:
pp: A : Type u_1
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra ℝ A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : T2Space A
inst✝⁵ : PartialOrder A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : StarOrderedRing A
inst✝² : ContinuousStar A
inst✝¹ : StarModule ℝ A
inst✝ : ClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfc x a) = {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
by
  apply subset_antisymm (range_cfc_nnreal_subset a ha)
  rw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.ofPred_and, SetLike.setOfPred_mem_eq,
    ← range_cfc _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
  rintro _ ⟨f, hf, rfl⟩
  exact cfc_cases _ a f ⟨0, by simp, by simp⟩ fun hf' ha' ↦
    ⟨f, (cfc_nonneg_iff f a hf' ha').mp (by simpa), by simp [cfc_apply f a ha' hf']⟩

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:
rw [range_cfcₙ_eq_range_cfcₙHom 𝕜 ha, range_cfcₙHom 𝕜 ha]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ x * y ∈ {x | ‖x‖ = 0}

Tactic:
by
    apply le_antisymm _ (norm_nonneg' _)
    refine (norm_mul_le' x y).trans_eq ?_
    rw [hx, hy, add_zero]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
⊢ IsExtreme 𝕜 A (⋂ i, F i)

Tactic:
refine ⟨iInter_subset_of_subset default (hAF default).1, fun x₁ hx₁A x₂ hx₂A x hxF hx ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
A : Set E
ι : Sort u_6
inst✝ : Nonempty ι
F : ι → Set E
hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)
inhabited_h : Inhabited ι
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxF : x ∈ ⋂ i, F i
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ ⋂ i, F i
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_1
𝕜 : 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)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x i

Tactic:
← update_self i x₁ x,

Goal state after:
case refine_1
𝕜 : 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)
x : (i : ι) → M i
hx : ∀ (i : ι), x i ∈ s i
h :
  ∀ (x₁ : (i : ι) → M i),
    (∀ (i : ι), x₁ i ∈ s i) → ∀ (x₂ : (i : ι) → M i), (∀ (i : ι), x₂ i ∈ s i) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
i : ι
x₁ : M i
hx₁ : x₁ ∈ s i
x₂ : M i
hx₂ : x₂ ∈ s i
hi : x i ∈ openSegment 𝕜 x₁ x₂
⊢ update x i x₁ i = x i
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
⊢ ‖(↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x‖ ≤ ‖a‖ * ‖x‖

Tactic:
rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, ← RCLike.ofReal_le_ofReal (K := ℂ),
      RCLike.ofReal_pow, RCLike.ofReal_eq_complex_ofReal, preGNS_norm_sq]
    have : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤
        ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x := by
      rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]
      exact CStarAlgebra.star_left_conjugate_le_norm_smul
    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: case ih
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
m : ℂ
x : A
a : f.PreGNS
⊢ (f.leftMulMapPreGNS (m • x)).completion ↑a = (m • (f.leftMulMapPreGNS x).completion) ↑a

Tactic:
| ih a =>

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
⊢ e.symm b = fun x ↦ Classical.arbitrary (E b)

Tactic:
by
  ext; 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
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
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)

Tactic:
rw [ts]

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
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
        ((Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))
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)
⊢ Prod.map Subtype.val id '' e.baseSet ×ˢ univ = (Subtype.val '' e.baseSet) ×ˢ univ

Tactic:
prodMap_image_prod,

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)
⊢ (Subtype.val '' e.baseSet) ×ˢ (id '' univ) = (Subtype.val '' e.baseSet) ×ˢ 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
b : B
h :
  IsInducing
    ((a.pretrivializationAt b).source.domRestrict ↑(a.pretrivializationAt b) ∘
      codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
this : TopologicalSpace (TotalSpace F E) := ⋯
⊢ IsInducing (codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)

Tactic:
refine h.of_comp ?_ (continuousOn_iff_continuous_domRestrict.mp
    (a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)).continuousOn)

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
b : B
h :
  IsInducing
    ((a.pretrivializationAt b).source.domRestrict ↑(a.pretrivializationAt b) ∘
      codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous[inst✝ b, instTopologicalSpaceSubtype] (codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ DiscreteTopology X ↔ IsLocallyInjective fun x ↦ y

Tactic:
by
  rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]
  refine forall_congr' fun x ↦ ⟨fun h ↦ ⟨{x}, h, Set.injOn_singleton _ _⟩, fun ⟨U, hU, inj⟩ ↦ ?_⟩
  convert! hU; ext x'; refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩
  rintro rfl; exact mem_of_mem_nhds hU

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit (Multiplicative G) e₂

Tactic:
by simp [hf.apply_eq_iff_mem_orbit]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit (Additive G) e₂

Tactic:
by simp [hf.apply_eq_iff_mem_orbit]

Goal state after:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
⊢ e ∈ ⋃ g, (fun x ↦ g • x) ⁻¹' U → e ∈ f ⁻¹' f '' U

Tactic:
intro ⟨_, ⟨g, rfl⟩, hg⟩

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
e : E
g : G
hg : e ∈ (fun g ↦ (fun x ↦ g • x) ⁻¹' U) g
⊢ e ∈ f ⁻¹' f '' U
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun m ↦ m • e) g' ∈ U
hfe : f ((fun m ↦ m • e) g') = f e
⊢ g • g⁻¹ • g' • e = g' • e

Tactic:
smul_inv_smul

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
⊢ (if hx : (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1 ∈ V then
      inv (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).2 hx
    else Classical.arbitrary (X → E) (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι).1) =
    e

Tactic:
simp_rw [dif_pos (id he : f e ∈ V)]

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
⊢ inv (idx e ⋯) ⋯ = e
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
hr : r ≤ π
t : ℝ
ht : t ∈ {x | |x| < r}
⊢ |(↑(exp t)).arg| < r

Tactic:
have htπ : |t| < π := ht.trans_le hr

Goal state after:
r : ℝ
hr : r ≤ π
t : ℝ
ht : t ∈ {x | |x| < r}
htπ : |t| < π
⊢ |(↑(exp t)).arg| < r
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
refine (disjoint_path_image_Ioc h).mono ?_ ?_ <;> exact image_mono Ioo_subset_Ioc_self

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this✝ : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
this : I * ↑y.arg = log y
⊢ NormedSpace.exp (I • ↑y.arg) = y

Tactic:
simpa [← exp_eq_exp_ℂ, this] using exp_log (by aesop)

Goal state after: