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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
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₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x✝
⊢ x ∈ t → quasispectrum 𝕜 (a x) ⊆ s x✝

Tactic:
hxt

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
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₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ quasispectrum 𝕜 (a x) ⊆ s x✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
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₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x✝
⊢ x ∈ t → p (a x)

Tactic:
hxt

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : X → Set 𝕜
f : 𝕜 → 𝕜
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₀, quasispectrum 𝕜 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, p (a x)
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum 𝕜 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ p (a x)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case star_id
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute (star ((cfcHom ha) (ContinuousMap.restrict (spectrum 𝕜 a) (ContinuousMap.id 𝕜)))) b

Tactic:
cfcHom_id

Goal state after:
case star_id
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
⊢ Commute (star a) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x✝
⊢ x ∈ t → quasispectrum ℝ≥0 (a x) ⊆ s x✝

Tactic:
hxt

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ quasispectrum ℝ≥0 (a x) ⊆ s x✝
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x✝
⊢ x ∈ t → 0 ≤ a x

Tactic:
hxt

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : 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₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ∀ x ∈ t, ContinuousOn f (s x)
hf0 : f 0 = 0
x✝ : X
hx✝ : x✝ ∈ t
x : X
hx : quasispectrum ℝ≥0 (a x) ⊆ s x✝
hxt : x ∈ t
⊢ 0 ≤ a 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
s : Set X
f : X → 𝕜 → 𝕜
a : A
hf : IntegrableOn (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) s μ
ha : p a
⊢ IntegrableOn (fun x ↦ cfc (f x) a) s μ

Tactic:
by
  exact integrable_cfc' _ _ hf ha

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

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 B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
⊢ IsExtreme 𝕜 A C

Tactic:
refine ⟨hBC.subset.trans hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxC hx ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ s → ∀ ⦃x₂ : E⦄, x₂ ∈ s → (x, y).1 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).1

Tactic:
rintro x₁ hx₁ x₂ hx₂ hx_fst

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : E
hx₁ : x₁ ∈ s
x₂ : E
hx₂ : x₂ ∈ s
hx_fst : (x, y).1 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = (x, y).1
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
⊢ t • ↑e - t • (↑e * ↑a * ↑e) + (s • ↑e - s • (↑e * ↑b * ↑e)) = ↑e - (t • (↑e * ↑a * ↑e) + s • (↑e * ↑b * ↑e))

Tactic:
match_scalars <;> grind

Goal state after:
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) '' Subtype.val ⁻¹' e.source ⊆ ↑e '' e.source

Tactic:
rintro z ⟨z₀, hz₀, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
z₀ : ↥s
hz₀ : z₀ ∈ Subtype.val ⁻¹' e.source
⊢ ↑(e.subtypeRestr hs) z₀ ∈ ↑e '' e.source
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case neg
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ proj ⁻¹' e.baseSet
hl : ¬∀ᶠ (x : α) in l, f x ∈ proj ⁻¹' e.baseSet
⊢ Tendsto (proj ∘ f) l (𝓝 (proj z)) → ¬Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz

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

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
α : Type u_5
l : Filter α
f : α → Z
z : Z
hz : z ∈ e.source
⊢ Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
by
  rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,
    tendsto_principal, coe_fst _ hz]
  by_cases hl : ∀ᶠ x in l, f x ∈ e.source
  · simp only [hl, and_true]
    refine (tendsto_congr' ?_).and Iff.rfl
    exact hl.mono fun x ↦ e.coe_fst
  · simp only [hl, and_false, false_iff, not_and]
    rw [e.source_eq] at hl hz
    exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz

Goal state after:
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) := a.totalSpaceTopology
⊢ IsInducing (TotalSpace.mk b)

Tactic:
apply IsInducing.of_codRestrict (a.mem_pretrivializationAt_source b)

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) := ⋯
⊢ IsInducing (codRestrict (TotalSpace.mk b) (a.pretrivializationAt b).source ⋯)
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 : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ (Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z =
    (↑e.toPartialEquiv ∘ Subtype.val) z

Tactic:
by ext; exacts [(e.proj_toFun _ hz).symm, rfl]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst✝¹] U
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hf : IsLocalHomeomorph ↑f
⊢ ↑f ∘ ⇑{ toFun := (f.target ∩ ↑f.symm ⁻¹' U).domRestrict f.invFun, continuous_toFun := ⋯ } = Subtype.val

Tactic:
ext y; exact f.right_inv y.2.1

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

Goal state before:
pp: r : ℝ
hr : r ≤ 0
⊢ centeredArc r = ∅

Tactic:
by
  contrapose! hr
  obtain ⟨-, x, hx, rfl⟩ := hr
  exact (abs_nonneg x).trans_lt hx

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ ⇑(y.path x) '' Ioc 0 1 = univ

Tactic:
path_image_Ioc_of_ne h.symm,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ ⇑exp '' Ioc (↑y).arg (y.angleDiff x + (↑y).arg) = univ
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)
this✝ : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this : Finite ↑(f ⁻¹' {x})
e : ↑(f ⁻¹' {x})
⊢ IsOpen[inst✝¹] (f '' V' e)

Tactic:
by
    convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ e).2

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a ^ 2 ≤ 1

Tactic:
← CStarAlgebra.norm_le_one_iff_of_nonneg (a ^ 2),

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ ‖a ^ 2‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re) a + I • cfc (fun x ↦ ↑√(1 - x.re ^ 2)) a

Tactic:
← cfc_real_eq_complex (fun x ↦ x) ha,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = cfc (fun x ↦ x) a + I • cfc (fun x ↦ ↑√(1 - x.re ^ 2)) a
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
A : E →L[𝕜] F
B : F →L[𝕜] E
⊢ A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
by
  refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
  ext x
  exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : A
⊢ ∃ u c, x = ∑ i, c i • ↑(u i) ∧ ∀ (i : Fin 4), ‖c i‖ ≤ ‖x‖ / 2

Tactic:
by
  let _ := CStarAlgebra.spectralOrder
  let _ := CStarAlgebra.spectralOrderedRing
  obtain (rfl | hx) := eq_or_ne x 0
  · exact ⟨![1, -1, 1, -1], 0, by simp⟩
  · have := norm_smul_two_inv_smul_add_four_unitary x hx
    extract_lets u₁ u₂ at this
    use ![u₁, star u₁, u₂, star u₂], ![‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹, ‖x‖ * 2⁻¹ * I, ‖x‖ * 2⁻¹ * I]
    constructor
    · conv_lhs => rw [this]
      simp [Fin.sum_univ_four, ← Complex.coe_smul]
      module
    · intro i
      fin_cases i
      all_goals simp [div_eq_mul_inv]

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
⊢ IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T

Tactic:
by
  rw [isStarProjection_iff, and_congr_right_iff]
  exact fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h

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
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
by
  refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
  ext x
  exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ ↑((s.restrict S hS).faceOppositeCentroid i) = s.faceOppositeCentroid i

Tactic:
rw [eq_comm]
  have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  have hf : Function.Injective (S.subtype) := by
    simp only [coe_subtype, Subtype.val_injective]
  exact (s.restrict S hS).faceOppositeCentroid_map S.subtype hf (i := i)

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ↑(f x) (g x)) s x

Tactic:
by
  change ContDiffWithinAt ℝ n (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X =>
    ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
  refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le
    (mod_cast le_top)).comp_contDiffWithinAt x ?_
  · exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem
  · exact (hR.div hr (f x).rIn_pos.ne').prodMk ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))

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
p : P
⊢ finrank k ↥(vectorSpan k (insert p ↑(affineSpan k s))) ≤ finrank k ↥(affineSpan k s).direction + 1

Tactic:
exact finrank_vectorSpan_insert_le ..

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
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n ↦ f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto (fun t ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt (fun x ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y

Tactic:
exact HasFDerivAt.fun_sum fun n _ => hf n y hy

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

Goal state before:
pp: case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h✝ : Nonempty α
⊢ ‖-f‖ = ‖f‖

Tactic:
apply (lp.isLUB_norm (-f)).unique

Goal state after:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h✝ : Nonempty α
⊢ IsLUB (Set.range fun i ↦ ‖↑(-f) i‖) ‖f‖
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : ¬0 < r
⊢ ball c r ⊆ (univBall c r).target

Tactic:
· rw [univBall, dif_neg hr]
    exact subset_univ _

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

Goal state before:
pp: case mp
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
⊢ (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) →
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y

Tactic:
intro hfl

Goal state after:
case mp
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
⊢ ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y