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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : 0 ≤ ↑a
⊢ ↑a ^ (-x) = ↑a⁻¹ ^ x

Tactic:
suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by
    rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
    refine cfc_congr fun _ _ => ?_
    simp [NNReal.rpow_neg, NNReal.inv_rpow]
  refine NNReal.continuousOn_rpow_const (.inl ?_)
  rintro ⟨z, hz, hz'⟩
  exact spectrum.zero_notMem ℝ≥0 a.isUnit <| inv_eq_zero.mp hz' ▸ hz

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝²² : PartialOrder A
inst✝²¹ : Ring A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : StarOrderedRing A
inst✝¹⁷ : Algebra ℝ A
inst✝¹⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹⁵ : NonnegSpectrumClass ℝ A
inst✝¹⁴ : IsSemitopologicalRing A
inst✝¹³ : T2Space A
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ cfc (fun x_1 ↦ x_1 ^ x) (a, b) = (cfc (fun x_1 ↦ x_1 ^ x) a, cfc (fun x_1 ↦ x_1 ^ x) b)

Tactic:
refine cfc_map_prod (R := ℝ≥0) (S := ℝ) _ a b (by cfc_cont_tac) ?_

Goal state after:
A : Type u_1
inst✝²² : PartialOrder A
inst✝²¹ : Ring A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : StarOrderedRing A
inst✝¹⁷ : Algebra ℝ A
inst✝¹⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹⁵ : NonnegSpectrumClass ℝ A
inst✝¹⁴ : IsSemitopologicalRing A
inst✝¹³ : T2Space A
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0 ≤ (a, b)
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul A (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
⊢ ‖x‖ = √‖∑ i, ⟪x i, x i⟫_A‖

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ‖(equiv A ((i : ι) → E i)) x‖ ≤ ‖x‖

Tactic:
pi_norm_le_iff_of_nonneg (by positivity)

Goal state after:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul A (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
x✝ : NormedAddCommGroup C⋆ᵐᵒᵈ(A, (i : ι) → E i) := normedAddCommGroup A
⊢ ∀ (i : ι), ‖(equiv A ((i : ι) → E i)) x i‖ ≤ ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ m * x) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun x ↦ star m * x) x = x * m

Tactic:
simp [hx.star_eq]

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)
m x : A
hx : IsSelfAdjoint x
⊢ (star ∘ fun x ↦ x * star m) x = m * x

Tactic:
simp [hx.star_eq]

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

Goal state before:
pp: n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateRow ι v‖₊ = ∑ i, ‖v i‖₊

Tactic:
simp [linfty_opNNNorm_def]

Goal state after:
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:
by
  simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ,
    PiLp.nnnorm_eq_of_L2]
  let s := (Finset.univ : Finset n).map ⟨fun i : n => (i, i), fun i j h => congr_arg Prod.fst h⟩
  rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
  · rw [Finset.sum_map, NNReal.sqrt_eq_rpow]
    dsimp
    simp_rw [diagonal_apply_eq, NNReal.rpow_two]
  · suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
    intro h
    exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
x : X
⊢ (∀ (y : Y), ‖(f x) y‖ ≤ bound x) → 0 x ≤ bound x

Tactic:
bound_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : TopologicalSpace Y
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompactSpace Y
f : X → C(Y, E)
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
h : Nonempty Y
x : X
bound_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
⊢ 0 x ≤ bound x
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : TopologicalSpace Y
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : CompactSpace Y
inst✝ : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
x : X
⊢ (∀ (y : Y), ‖(f x) y‖ ≤ bound x) → 0 x ≤ bound x

Tactic:
bound_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : MeasurableSpace X
μ : Measure X
inst✝³ : TopologicalSpace Y
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : CompactSpace Y
inst✝ : Zero Y
f : X → C(Y, E)₀
bound : X → ℝ
bound_int : HasFiniteIntegral bound μ
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x
x : X
bound_x : ∀ (y : Y), ‖(f x) y‖ ≤ bound x
⊢ 0 x ≤ bound x
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
a : A
f : X → C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : Integrable f μ
ha : p a
⊢ ∫ (x : X), (cfcL ha) (f x) ∂μ = (cfcL ha) (∫ (x : X), f x ∂μ)

Tactic:
ContinuousLinearMap.integral_comp_comm _ hf₁

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
a : A
f : X → C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : Integrable f μ
ha : p a
⊢ (cfcL ha) (∫ (x : X), f x ∂μ) = (cfcL ha) (∫ (x : X), f x ∂μ)
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
inst✝ : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.im) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ f ↑(ℑ a) = cfcₙ (fun x ↦ f ↑x.im) a

Tactic:
rw [← cfcₙ_im_id a, ← cfcₙ_comp' ..]

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✝⁷ : 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
a : A
f : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : Integrable f μ
ha : p a
⊢ ∫ (x : X), (cfcₙL ha) (f x) ∂μ = (cfcₙL ha) (∫ (x : X), f x ∂μ)

Tactic:
ContinuousLinearMap.integral_comp_comm _ hf₁

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✝⁷ : 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
a : A
f : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : Integrable f μ
ha : p a
⊢ (cfcₙL ha) (∫ (x : X), f x ∂μ) = (cfcₙL ha) (∫ (x : X), f x ∂μ)
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖(toCLM M) v‖ ≤ √‖M * star M‖ * ‖v‖

Tactic:
norm_eq_sqrt_norm_inner_self (A := A),

Goal state after:
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ √‖⟪(toCLM M) v, (toCLM M) v⟫_A‖ ≤ √‖M * star M‖ * ‖v‖
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:
apply subset_antisymm (range_cfc_nnreal_subset a ha)

Goal state after:
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
⊢ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x} ⊆ Set.range fun x ↦ cfc x a
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case hbc
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖(toCLM Mᴴ) ((toCLM M) v)‖ ≤ ‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖

Tactic:
rw [← ContinuousLinearMap.comp_apply]

Goal state after:
case hbc
A : Type u_1
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
M : CStarMatrix n n A
v : C⋆ᵐᵒᵈ(A, n → A)
⊢ ‖(toCLM Mᴴ ∘SL toCLM M) v‖ ≤ ‖toCLM Mᴴ ∘SL toCLM M‖ * ‖v‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case e_f
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
⊢ (∑ x, (∑ c, y.ofLp c * A x c) * Pi.single x 1 i) * x.ofLp i = (∑ c, y.ofLp c * A i c) * x.ofLp i

Tactic:
simp [Pi.single_apply]

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

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

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

Tactic:
· intro x hx; simp_all

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

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

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
  · obtain ⟨e, hxe, rfl⟩ := h x hx
    exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩
  · obtain ⟨U, hU, emb⟩ := h x hx
    have : IsOpenEmbedding ((interior U).domRestrict f) := by
      refine emb.comp ⟨.inclusion interior_subset, ?_⟩
      rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
    obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_isOpenMap.mp this
    have : Nonempty X := ⟨x⟩
    exact ⟨OpenPartialHomeomorph.ofContinuousOpenRestrict
      (Set.injOn_iff_injective.mpr inj).toPartialEquiv
      (continuousOn_iff_continuous_domRestrict.mpr cont) openMap isOpen_interior,
      mem_interior_iff_mem_nhds.mpr hU, rfl⟩

Goal state after:
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
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
⊢ ∀ x ∈ f '' s, ∃ e, x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ e, f x ∈ e.source ∧ Set.EqOn g (↑e) e.source
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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ (fun x ↦ g • x) '' interior U ∩ interior U ⊆ (fun x ↦ g • x) '' U ∩ U

Tactic:
interior_subset

Goal state after:
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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ (fun x ↦ g • x) '' U ∩ U ⊆ (fun x ↦ g • x) '' U ∩ U
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r s : ℝ
h : r ≤ s
⊢ centeredArc r ⊆ centeredArc s

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
r s : ℝ
h : r ≤ s
x : ℝ
hx : x ∈ {x | |x| < r}
⊢ exp x ∈ centeredArc s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
by
  rw [range_path, ← Ioc_insert_left (by simp), image_insert_eq,
    ← path_image_Ioc_of_ne h, ← union_singleton, compl_union, compl_path_image_Ioc h,
    ← Ioo_insert_right (by simp), image_insert_eq, (y.path x).target, exp_arg,
    insert_inter_of_notMem (by simp), inter_eq_left]
  rintro z ⟨t, ht, rfl⟩
  exact (path_injective_of_ne h.symm).ne ht.2.ne |>.trans_eq (y.path x).target

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

Goal state before:
pp: x : Circle
⊢ -x ∈ (range ⇑(x.path x))ᶜ

Tactic:
simp [neg_ne_self]

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

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
⊢ x ∉ range ⇑(y.path (-x))

Tactic:
rintro hP₂

Goal state after:
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
hP₂ : x ∈ range ⇑(y.path (-x))
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑m * T = -z✝¹ + z✝

Tactic:
field_simp at hm

Goal state after:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : z✝ = z✝¹ + T * ↑m
⊢ ↑m * T = -z✝¹ + z✝
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✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑(T ∘SL adjoint T)).ker = (↑(adjoint T)).ker

Tactic:
by
  simpa using T†.ker_adjoint_comp_self

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 - ↑‖(adjoint T) x‖ ^ 2 = 0) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
sub_eq_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ (∀ (x : E), ↑‖T x‖ ^ 2 = ↑‖(adjoint T) x‖ ^ 2) ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ IsStarProjection T ↔ (↑T).IsSymmetricProjection

Tactic:
by
  simp [isStarProjection_iff, LinearMap.isSymmetricProjection_iff,
    isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← toLinearMap_comp, mul_def]

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
⊢ (A ∘ₗ adjoint A).range = A.range

Tactic:
by
  simpa using A.adjoint.range_adjoint_comp_self

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
A : E →ₗ[𝕜] E
⊢ A.IsSymmetric ↔ IsSelfAdjoint A

Tactic:
rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]
  exact eq_comm

Goal state after:
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)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • ∑ x, (s.points i -ᵥ s.points x)

Tactic:
rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, ← neg_smul,
    Lean.Grind.Ring.neg_eq_mul_neg_one, ← smul_smul, smul_sum]

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)
⊢ (↑n)⁻¹ • ∑ x, -1 • (s.points x -ᵥ s.points i) = (↑n)⁻¹ • ∑ x, (s.points i -ᵥ s.points x)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : 1 - (starRingEnd 𝕜) y * y = 0 ∨ ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
sub_eq_zero,

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : 1 = (starRingEnd 𝕜) y * y ∨ ↑↑g = 0
⊢ ∃ α, ∀ (x : H), f x = (α • g) x