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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x

Tactic:
obtain ⟨r, hr, hr_min⟩ := h_cpct.exists_isMinOn
      (ContinuousFunctionalCalculus.spectrum_nonempty a ha) continuousOn_id

Goal state after:
case refine_2
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
h : ∀ x ∈ spectrum ℝ a, 0 < x
r : ℝ
hr : r ∈ spectrum ℝ a
hr_min : IsMinOn id (spectrum ℝ a) r
⊢ ∃ r > 0, ∀ x ∈ spectrum ℝ a, r ≤ x
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A = 0 ↔ x = 0

Tactic:
by
    refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
    apply equiv A (E × F) |>.injective
    ext
    · refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
      exact le_add_of_nonneg_right CStarModule.inner_self_nonneg |>.trans_eq h
    · refine inner_self.mp <| le_antisymm ?_ (inner_self_nonneg (A := A))
      exact le_add_of_nonneg_left CStarModule.inner_self_nonneg |>.trans_eq h

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖A i j‖₊)

Tactic:
by
  simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_def]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m : A
⊢ Tendsto (fun x ↦ x * m) (approximateUnit A) (𝓝 m)

Tactic:
by
  refine tendsto_mul_right_of_forall_nonneg_tendsto (fun m hm₁ hm₂ ↦ ?_) m
  rw [(hasBasis_approximateUnit A).tendsto_iff nhds_basis_closedBall]
  intro ε hε
  lift ε to ℝ≥0 using hε.le
  rw [coe_pos] at hε
  refine ⟨cfcₙ (fun y : ℝ≥0 ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • m),
    ⟨cfcₙ_nonneg_of_predicate, norm_cfcₙ_one_sub_one_add_inv_lt_one (ε⁻¹ ^ 2 • m)⟩, ?_⟩
  rintro x ⟨(hx₁ : _ ≤ x), hx₂⟩
  simp only [mem_closedBall, dist_eq_norm', zero_sub, norm_neg] at hx₂ ⊢
  rw [← coe_nnnorm, coe_le_coe]
  have hx₀ : 0 ≤ x := cfcₙ_nonneg_of_predicate.trans hx₁
  rw [← inr_le_iff _ _ (.of_nonneg cfcₙ_nonneg_of_predicate) (.of_nonneg hx₀),
    nnreal_cfcₙ_eq_cfc_inr _ _ (by simp [tsub_self]), inr_smul] at hx₁
  rw [← norm_inr (𝕜 := ℂ)] at hm₂ hx₂
  rw [← inr_nonneg_iff] at hx₀ hm₁
  rw [← nnnorm_inr (𝕜 := ℂ), inr_sub, inr_mul]
  generalize (x : A⁺¹) = x, (m : A⁺¹) = m at *
  set g : ℝ≥0 → ℝ≥0 := fun y ↦ 1 - (1 + y)⁻¹
  have hg : Continuous g := by
    rw [← continuousOn_univ]
    fun_prop (disch := intro _ _; positivity)
  have hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (spectrum ℝ≥0 m) :=
    ContinuousOn.inv₀ (by fun_prop) fun _ _ ↦ by positivity
  have hx : x ∈ Set.Icc 0 1 := mem_Icc_iff_norm_le_one.mpr ⟨hx₀, hx₂⟩
  have hx' : x ∈ Set.Icc _ 1 := ⟨hx₁, hx.2⟩
  refine nnnorm_sub_mul_self_le m cfc_nonneg_of_predicate hx' ?_
  suffices star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m =
      cfc (fun y : ℝ≥0 ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m by
    rw [this]
    refine nnnorm_cfc_nnreal_le fun y hy ↦ ?_
    calc
      y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y = y * ε ^ 2 * (y / (ε ^ 2 + y)) := by simp [field]
      _ ≤ ε ^ 2 * 1 := by
        gcongr
        · apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy
        · exact div_le_one (by positivity) |>.mpr le_add_self
      _ = ε ^ 2 := mul_one _
  rw [cfc_mul _ _ m (continuousOn_id' _ |>.fun_mul hg') (continuousOn_id' _),
    cfc_mul _ _ m (continuousOn_id' _) hg', cfc_id' .., hm₁.star_eq]
  congr
  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)]
  refine cfc_congr (fun y _ ↦ ?_)
  simp [g, tsub_tsub_cancel_of_le]

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
⊢ 𝓤 (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

Goal state after:
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
this : (fun x ↦ (ofMatrix.symm x.1, ofMatrix.symm x.2)) = id
⊢ 𝓤 (CStarMatrix m n A) = 𝓤 (CStarMatrix m n 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✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ (NonUnitalStarSubalgebra.map (cfcₙHom ha) (adjoin 𝕜 {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure =
    elemental 𝕜 a

Tactic:
NonUnitalStarAlgHom.map_adjoin

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
⊢ (adjoin 𝕜 (⇑(cfcₙHom ha) '' {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure = 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
⊢ (NonUnitalStarSubalgebra.map (cfcₙHom ha) (adjoin 𝕜 {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure ≤
    elemental 𝕜 a

Tactic:
NonUnitalStarAlgHom.map_adjoin

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
⊢ (adjoin 𝕜 (⇑(cfcₙHom ha) '' {ContinuousMapZero.id (quasispectrum 𝕜 a)})).topologicalClosure ≤ elemental 𝕜 a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: case mpr
A : Type u_1
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : T2Space A
inst✝³ : PartialOrder A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : StarOrderedRing A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
x✝ : A
⊢ x✝ ∈ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} → x✝ ∈ Set.range fun x ↦ cfcₙ x a

Tactic:
· rintro ⟨f, hf, rfl⟩
    simp only [cfcₙ_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

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

Goal state before:
pp: case hf
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
z : ↑(quasispectrum 𝕜 a)
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑(∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)

Tactic:
exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x

Tactic:
rintro H (rfl | rfl | hx)

Goal state after:
case mp.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₂ : E
h₂ : x₂ ∈ A
h₁ : x ∈ A
H : x ∈ openSegment 𝕜 x x₂ → x = x ∧ x₂ = x
⊢ x = x ∨ x₂ = x

case mp.inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
h₂ : x ∈ A
H : x ∈ openSegment 𝕜 x₁ x → x₁ = x ∧ x = x
⊢ x₁ = x ∨ x = x

case mp.inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∨ x₂ = x
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: case hp
α : 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₂
f : α →SL[σ] β
r : R₁
⊢ IsClosed
    {a | (↑((↑f).toAddMonoidHom.completion ⋯)).toFun (r • a) = σ r • (↑((↑f).toAddMonoidHom.completion ⋯)).toFun a}

Tactic:
exact isClosed_eq (continuous_map.comp <| continuous_const_smul r)
        (continuous_map.fun_const_smul _)

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
x✝¹ x✝ : A
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion = (f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion

Tactic:
ext c
    induction c using induction_on with
      | hp => apply isClosed_eq <;> fun_prop
      | ih c => simp

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

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ (∀ (x : X × Y), (↑eX x.1, ↑eY x.2) = (↑eX' x.1, ↑eY' x.2)) ∧
      (∀ (x : X' × Y'), (↑eX.symm x.1, ↑eY.symm x.2) = (↑eX'.symm x.1, ↑eY'.symm x.2)) ∧
        (eX.prod eY).source = (eX'.prod eY').source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source

Tactic:
prod_source,

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ (∀ (x : X × Y), (↑eX x.1, ↑eY x.2) = (↑eX' x.1, ↑eY' x.2)) ∧
      (∀ (x : X' × Y'), (↑eX.symm x.1, ↑eY.symm x.2) = (↑eX'.symm x.1, ↑eY'.symm x.2)) ∧
        eX.source ×ˢ eY.source = eX'.source ×ˢ eY'.source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
⊢ (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source

Tactic:
by
  simp only [subtypeRestr_def, mfld_simps]

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

Goal state before:
pp: case inl
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
heq : a = c
⊢ c ∈ s

Tactic:
rwa [← heq]

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
z : TotalSpace F E
hz : z.proj ∈ e.baseSet
⊢ (↑e.symm (↑e z)).snd ≍ z.snd

Tactic:
e.symm_apply_apply (e.mem_source.mpr hz)

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
z : TotalSpace F E
hz : z.proj ∈ e.baseSet
⊢ z.snd ≍ z.snd
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.1‖ = ‖a‖

Tactic:
by
  simp only [norm_def, toProdHom_apply, Prod.norm_def, norm_fst_eq_snd, max_eq_right le_rfl]

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

Goal state before:
pp: case refine_2
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ⊆ range ⇑(x.path y) ∪ range ⇑(y.path x)

pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(y.path x)

Tactic:
· rw [range_path_union_range_path hxy]
    exact subset_univ _

Goal state after:
case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y}ᶜ ⊆ range ⇑(y.path x)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
⊢ -1 ∈ spectrum ℂ u

Tactic:
have hz_norm : ‖z‖ = 1 := spectrum.norm_eq_one_of_unitary hu hz

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ IsLeast (re '' (fun x ↦ NormedSpace.exp (I • x)) '' ⇑(algebraMap ℝ ℂ) '' spectrum ℝ ↑x) (Real.cos ‖x‖)

Tactic:
simp only [Set.image_image, coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ,
    exp_ofReal_mul_I_re]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
⊢ IsLeast ((fun a ↦ Real.cos a) '' spectrum ℝ ↑x) (Real.cos ‖x‖)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂

Tactic:
have ha :=
    (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _
      (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁)
      (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h

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
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha : (↑univ).indicator (centroidWeightsIndicator k fs₁) = (↑univ).indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i✝ i : Fin (n + 1)
⊢ ∑ j ∈ {i}ᶜ, (↑n)⁻¹ • (s.points j -ᵥ s.points i) = ∑ j, (↑n)⁻¹ • (s.points j -ᵥ s.points i)

Tactic:
← Finset.sum_compl_add_sum {i}

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i✝ i : Fin (n + 1)
⊢ ∑ j ∈ {i}ᶜ, (↑n)⁻¹ • (s.points j -ᵥ s.points i) =
    ∑ i_1 ∈ {i}ᶜ, (↑n)⁻¹ • (s.points i_1 -ᵥ s.points i) + ∑ i_1 ∈ {i}, (↑n)⁻¹ • (s.points i_1 -ᵥ s.points i)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ line[k, s.points i, s.faceOppositeCentroid i] ≤ line[k, s.points i, s.centroid]

Tactic:
apply affineSpan_pair_le_of_right_mem

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i ∈ line[k, s.points i, s.centroid]
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h1 : s.median i ≤ line[k, s.points i, s.centroid]
⊢ line[k, s.points i, s.centroid] ≤ line[k, s.points i, s.faceOppositeCentroid i]

Tactic:
apply affineSpan_pair_le_of_right_mem

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h1 : s.median i ≤ line[k, s.points i, s.centroid]
⊢ s.centroid ∈ line[k, s.points i, s.faceOppositeCentroid i]
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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ vectorSpan k s ≤ k ∙ v

Tactic:
vectorSpan_eq_span_vsub_set_right k h,

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
⊢ Submodule.span k ((fun x ↦ x -ᵥ p₀) '' s) ≤ k ∙ v
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
s : Finset α
⊢ (fun s ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal) s ≤ C

Tactic:
exact hf s

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
⊢ ContDiff 𝕜 ↑m fun x ↦ ∑' (i : α), f i x

Tactic:
let T : Finset α := ht.toFinset

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
⊢ ContDiff 𝕜 ↑m fun x ↦ ∑' (i : α), f i x