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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ spectrum ℝ (a ^ 2), 0 ≤ x

Tactic:
← cfc_id (R := ℝ) a,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ ∀ x ∈ spectrum ℝ (cfc id a ^ 2), 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ ∃ x, (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i, I ^ ↑i • x i

Tactic:
by
  use ![(realPart a)⁺, (imaginaryPart a)⁺, (realPart a)⁻, (imaginaryPart a)⁻]
  rw [← and_assoc, ← forall_and]
  constructor
  · intro i
    fin_cases i
    all_goals
      constructor
      · simp
        cfc_tac
    · exact CStarAlgebra.norm_posPart_le _ |>.trans <| realPart.norm_le a
    · exact CStarAlgebra.norm_posPart_le _ |>.trans <| imaginaryPart.norm_le a
    · exact CStarAlgebra.norm_negPart_le _ |>.trans <| realPart.norm_le a
    · exact CStarAlgebra.norm_negPart_le _ |>.trans <| imaginaryPart.norm_le a
  · nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]
    simp only [Fin.sum_univ_four, Fin.coe_ofNat_eq_mod, Matrix.cons_val, Nat.reduceMod, I_sq,
      I_pow_three]
    module

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
a : A
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
have ha₁' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha.isUnit

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
a : A
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
ha₁' : 0 ∉ spectrum ℝ≥0 a
⊢ (a ^ x) ^ y = a ^ (x * y)
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul A E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
by
  simp only [norm_eq_sqrt_norm_inner_self (A := A), Real.sqrt_pos, norm_pos_iff]
  intro H
  rw [inner_self] at H
  exact hx H

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ star a * b * a ≤ ‖b‖ • (star a * a)

Tactic:
← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hb : IsSelfAdjoint b
this : ∀ (a b : Unitization ℂ A), IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a)
⊢ ↑(star a * b * a) ≤ ↑(‖b‖ • (star a * a))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
hf₀ : ¬f 0 = 0
⊢ ConvexOn ℝ s (cfcₙ f)

Tactic:
have : (cfcₙ f : A → A) = fun _ => 0 := by
      ext x
      simp [cfcₙ_apply_of_not_map_zero _ hf₀]
    rw [this]
    refine convexOn_const _ ?_
    have : Convex ℝ (inrl ⁻¹' inrl '' s) := Convex.linear_preimage hf.1 _
    rwa [Set.preimage_image_eq _ inrHom_injective] at this

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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, spectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : spectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
⊢ Tendsto (fun x ↦ cfc f (a x)) l (𝓝 (cfc f a₀))

Tactic:
by
  apply continuousOn_cfc_nnreal A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp
  rw [tendsto_nhdsWithin_iff]
  exact ⟨ha_tendsto, ha'.and ha⟩

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
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
⊢ ∀ x ∈ t, ContinuousWithinAt (fun x ↦ cfc f (a x)) t x

Tactic:
refine fun x hx ↦ (ha_cont x hx).cfc_nnreal (hs x hx) f hx ?_ ?_ (hf x hx)

Goal state after:
case refine_1
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
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[t] x, spectrum ℝ≥0 (a x_1) ⊆ s x

case refine_2
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
t : Set X
hs : ∀ x ∈ t, IsCompact (s x)
ha_cont : ∀ x ∈ t, ContinuousWithinAt a t x
ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in 𝓝[t] x₀, spectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
x : X
hx : x ∈ t
⊢ ∀ᶠ (x : X) in 𝓝[t] x, 0 ≤ a x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalCStarAlgebra A
inst✝ : PartialOrder A
l : Filter A
hl : l.IsIncreasingApproximateUnit
⊢ closedBall 0 1 ∈ l

Tactic:
by
  simpa [Metric.closedBall] using! hl.eventually_norm

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
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ‖↑z - ↑y * ↑z‖ ≤ c

Tactic:
refine norm_sub_mul_self_le _ ?_ ?_ hc h

Goal state after:
case refine_1
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ 0 ≤ ↑x

case refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ↑y ∈ Set.Icc (↑x) 1
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖0‖₊ = 0

Tactic:
nnnorm_zero

Goal state after:
case e_f.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ 0 = 0
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Tactic:
simp_rw [linfty_opNNNorm_def, Matrix.mul_apply]

Goal state after:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖∑ j_1, A i j_1 * B j_1 j‖₊) ≤
    (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst✝¹³ : NonUnitalCStarAlgebra A₁
inst✝¹² : NonUnitalCStarAlgebra A₂
inst✝¹¹ : PartialOrder A₁
inst✝¹⁰ : StarOrderedRing A₁
inst✝⁹ : PartialOrder A₂
inst✝⁸ : StarOrderedRing A₂
inst✝⁷ : CStarAlgebra B₁
inst✝⁶ : CStarAlgebra B₂
inst✝⁵ : PartialOrder B₁
inst✝⁴ : PartialOrder B₂
inst✝³ : StarOrderedRing B₁
F : Type u_5
inst✝² : FunLike F A₁ A₂
inst✝¹ : LinearMapClass F ℂ A₁ A₂
inst✝ : OrderHomClass F A₁ A₂
f : F
⊢ Continuous ⇑f

Tactic:
have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
      obtain ⟨C, h⟩ := exists_norm_apply_le (.ofClass f)
      exact ⟨C, h⟩

Goal state after:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst✝¹³ : NonUnitalCStarAlgebra A₁
inst✝¹² : NonUnitalCStarAlgebra A₂
inst✝¹¹ : PartialOrder A₁
inst✝¹⁰ : StarOrderedRing A₁
inst✝⁹ : PartialOrder A₂
inst✝⁸ : StarOrderedRing A₂
inst✝⁷ : CStarAlgebra B₁
inst✝⁶ : CStarAlgebra B₂
inst✝⁵ : PartialOrder B₁
inst✝⁴ : PartialOrder B₂
inst✝³ : StarOrderedRing B₁
F : Type u_5
inst✝² : FunLike F A₁ A₂
inst✝¹ : LinearMapClass F ℂ A₁ A₂
inst✝ : OrderHomClass F A₁ A₂
f : F
hbound : ∃ C, ∀ (a : A₁), ‖f a‖ ≤ C * ‖a‖
⊢ Continuous ⇑f
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖T (toLp 2 (Pi.single i 1))‖

Tactic:
toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ = ‖toLp 2 (diagonal v *ᵥ Pi.single i 1)‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • (toEuclideanLin ≪≫ₗ toContinuousLinearMap) x‖ ≤ ‖r‖ * ‖x‖

Tactic:
exact norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ EqOn (↑e' ∘ ↑(e.restr s).symm) (↑((e.symm.trans e').restr (↑e '' s))) ((e.restr s).symm.trans e').source

Tactic:
restr_symm_apply,

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ EqOn (↑e' ∘ ↑e.symm) (↑((e.symm.trans e').restr (↑e '' s))) ((e.restr s).symm.trans e').source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case h
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
F : X' → Z := extend f ↑e fun x ↦ Classical.arbitrary Z
F_eq : F = extend f ↑e fun x ↦ Classical.arbitrary Z
heq : EqOn F (↑e ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph f hf).symm) (f '' e.source)
x' : X'
x : X
hx : x ∈ e.source
hx'x : f x = x'
⊢ x ∈ e.source

Tactic:
exact hx

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
e f : Pretrivialization F proj
⊢ f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Tactic:
rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]

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

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
a : F
⊢ { proj := b, snd := a } ∈ (Z.localTrivAt b).source

Tactic:
by
  simp only [mfld_simps]

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
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ ↑e.toPartialEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ e.source ∩ e.source

Tactic:
rw [inter_assoc, inter_self]; rfl

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

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd.2 ^ k) x * y = x * (a.toProd.1 ^ k) y
x y : A
⊢ (a.toProd.2 ^ (k + 1)) x * y = x * (a.toProd.1 ^ (k + 1)) y

Tactic:
rw [pow_succ' a.snd, mul_apply_eq_comp, a.central, hk, pow_succ a.fst, mul_apply_eq_comp]

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
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint (proj ⁻¹' e.baseSet) (proj ⁻¹' e'.baseSet)

Tactic:
exact H.preimage _

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝¹ : x ∈ s
e : OpenPartialHomeomorph X Y
hx✝ : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_x : X
hx : _x ∈ e.source
⊢ f _x ∈ e.target

Tactic:
he hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝¹ : x ∈ s
e : OpenPartialHomeomorph X Y
hx✝ : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_x : X
hx : _x ∈ e.source
⊢ ↑e _x ∈ e.target
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝¹ : x ∈ s
e : OpenPartialHomeomorph X Y
hx✝ : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_x : X
hx : _x ∈ e.source
⊢ e.invFun (f _x) = _x

Tactic:
he hx

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝¹ : x ∈ s
e : OpenPartialHomeomorph X Y
hx✝ : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_x : X
hx : _x ∈ e.source
⊢ e.invFun (↑e _x) = _x
Module: Mathlib.Topology.IsLocalHomeomorph

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

Tactic:
imp_iff_right (Set.mem_univ _)

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
hf : IsCoveringMap f
t : Set X
⊢ IsCoveringMap (t.restrictPreimage f)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢
  exact hf.restrictPreimage t

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
inst✝² : Group E
inst✝¹ : IsTopologicalGroup E
inst✝ : Group X
f : E →* X
hf : IsQuotientMap ⇑f
disc : IsDiscrete ↑f.ker
x✝¹ x✝ : E
⊢ f x✝¹ = f x✝ ↔ x✝ * x✝¹⁻¹ ∈ f.ker

Tactic:
rw [eq_comm, ← mul_inv_eq_one, ← map_inv, ← map_mul]; rfl

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
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
have : ⋃ e, V' e ∈ nhdsSet (f ⁻¹' {x}) :=
    (isOpen_iUnion hV').mem_nhdsSet.2 fun e he ↦ mem_iUnion_of_mem ⟨e, he⟩ ⟨(hV e).1, (hφ _).1⟩

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
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
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
⊢ IsLocalHomeomorph f ↔ IsCoveringMap f

Tactic:
by
  refine ⟨fun h ↦ ?_, IsCoveringMap.isLocalHomeomorph⟩
  have hf : Continuous f := by
    rw [continuous_iff_continuousAt]
    intro e
    obtain ⟨φ, hφ, rfl⟩ := h e
    exact φ.continuousAt hφ
  rw [isCoveringMap_iff_isCoveringMapOn_univ]
  apply IsCoveringMapOn.of_isLocalHomeomorphOn hf
  simpa [← isLocalHomeomorph_iff_isLocalHomeomorphOn_univ]

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 : ℕ
s : Simplex k P n
⊢ s.centroid = (affineCombination k univ s.points) (centroidWeights k univ)

Tactic:
by rfl

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.faceOppositeCentroid i -ᵥ s.centroid = (↑n)⁻¹ • (s.centroid -ᵥ s.points i)

Tactic:
rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint {i} {j}
⊢ Disjoint (Submodule.span k (u '' {i})) (Submodule.span k (u '' {j}))

Tactic:
hi.disjoint_span_image h_ij

Goal state after:
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
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ (affineSpan k (insert p₁ ↑(affineSpan k s))).direction = (affineSpan k (insert p₁ ↑line[k, p₂, p₃])).direction

Tactic:
h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃

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
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ (affineSpan k (insert p₁ ↑(affineSpan k s))).direction = (affineSpan k (insert p₁ ↑(affineSpan k s))).direction
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
by
  have : IsAddTorsionFree E := .of_isTorsionFree ℝ E
  simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_right_eq_self]

Goal state after: