mathlib-initiative/mathlib-tactics huggingface dataset:
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
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, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto (fun x ↦ cfcₙ f (a x)) l (𝓝 (cfcₙ f a₀))

Tactic:
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.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
⊢ reindexₐ R A e.symm = (reindexₐ R A e).symm

Tactic:
simp [reindexₐ, reindexₗ]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
i : m
j : n
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
suffices ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖ by
    obtain (h | h) := eq_zero_or_norm_pos (M i j)
    · simp [h, norm_def]
    · exact le_of_mul_le_mul_right this h
  rw [← CStarRing.norm_star_mul_self, ← toCLM_apply_single_apply]
  apply norm_apply_le_norm _ _ |>.trans
  apply (toCLM M).le_opNorm _ |>.trans
  simp [norm_def]

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✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : ContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ cfc (fun r ↦ ∫ (x : X) in s, f x r ∂μ) a = ∫ (x : X) in s, cfc (f x) a ∂μ

Tactic:
refine cfc_setIntegral' _ _ this ⟨?_, ?_⟩ ha

Goal state after:
case refine_1
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
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ AEStronglyMeasurable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)

case refine_2
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
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
s : Set X
hs : MeasurableSet s
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf : ContinuousOn (Function.uncurry f) (s ×ˢ spectrum 𝕜 a)
bound_ge : ∀ᵐ (x : X) ∂μ.restrict s, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound (μ.restrict s)
ha : p a
this : ∀ᵐ (x : X) ∂μ.restrict s, ContinuousOn (f x) (spectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) (μ.restrict s)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfcₙ x a) ⊆ {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha,

Goal state after:
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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} ⊆ {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfcₙ x a) = {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha,

Goal state after:
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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (fun x ↦ cfcₙ x a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} = {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: 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✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h : ¬f 0 = 0
⊢ cfcₙ 0 a = cfcₙ f a

Tactic:
simp [cfcₙ_apply_of_not_map_zero a h]

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(((rankOne 𝕜) x) y)).rank = 1

Tactic:
by
  rw [LinearMap.rank, rankOne_def, range_smulRight_apply, Module.rank_eq_one_iff_finrank_eq_one]
  · exact finrank_span_singleton hx
  · exact map_eq_zero_iff _ (toDualMap 𝕜 F).injective |>.not.mpr hy

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

Goal state before:
pp: case refine_3
𝕜 : 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₁ : F⦄, x₁ ∈ t → ∀ ⦃x₂ : F⦄, x₂ ∈ t → (x, y).2 ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y).2

Tactic:
rintro x₁ hx₁ x₂ hx₂ hx_snd

Goal state after:
case refine_3
𝕜 : 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₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = (x, y).2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ ‖U i a‖ ^ 2

Tactic:
apply sq_nonneg

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ exp (↑n * x) = exp x ^ n

Tactic:
rw [← nsmul_eq_mul, exp_nsmul]

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)

Tactic:
rintro ⟨_, x⟩ rfl
    exact ⟨x, rfl⟩

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 = ↑eX' x.1 ∧ ↑eY x.2 = ↑eY' x.2) ∧
      (∀ (x : X' × Y'), ↑eX.symm x.1 = ↑eX'.symm x.1 ∧ ↑eY.symm x.2 = ↑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

Tactic:
Set.prod_eq_prod_iff_of_nonempty h,

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 = ↑eX' x.1 ∧ ↑eY x.2 = ↑eY' x.2) ∧
      (∀ (x : X' × Y'), ↑eX.symm x.1 = ↑eX'.symm x.1 ∧ ↑eY.symm x.2 = ↑eY'.symm x.2) ∧
        eX.source = eX'.source ∧ eY.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
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
⊢ ∀ ⦃x : X'⦄, x ∈ f '' e.source → (f ∘ e.invFun) (extend f (↑e) (fun x ↦ Classical.arbitrary Z) x) = x

Tactic:
by
    intro x ⟨x₀, hx₀, hxx₀⟩
    rw [← hxx₀, hf.injective.extend_apply e, comp_apply]
    congr
    exact e.left_inv' hx₀

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
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (have this := fun x ↦ { proj := x, snd := v };
    this)
    x

Tactic:
refine ((Z.localTrivAt x).toOpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_

Goal state after:
case refine_1
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ (have this := fun x ↦ { proj := x, snd := v };
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(Z.localTrivAt x).toOpenPartialHomeomorph ∘
      have this := fun x ↦ { proj := x, snd := v };
      this)
    x
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 (↑e.toOpenPartialHomeomorph ∘ f) l (𝓝 (↑e.toOpenPartialHomeomorph z)) ∧ Tendsto f l (𝓟 e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
Prod.tendsto_iff,

Goal state after:
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 (fun n ↦ ((↑e.toOpenPartialHomeomorph ∘ f) n).1) l (𝓝 (↑e.toOpenPartialHomeomorph z).1) ∧
        Tendsto (fun n ↦ ((↑e.toOpenPartialHomeomorph ∘ f) n).2) l (𝓝 (↑e.toOpenPartialHomeomorph z).2)) ∧
      Tendsto f l (𝓟 e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)
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 (fun n ↦ ((↑e ∘ f) n).1) l (𝓝 (↑e z).1) ∧ Tendsto (fun n ↦ ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)

Tactic:
coe_fst _ hz

Goal state after:
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 (fun n ↦ ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n ↦ ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧
      ∀ᶠ (a : α) in l, f a ∈ e.source) ↔
    Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (↑e (f x)).2) l (𝓝 (↑e z).2)
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)

Tactic:
by
  let := a.totalSpaceTopology
  intro z hz
  let e : Trivialization F (π F E) :=
    a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas z.proj)
  refine (e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt
  · exact a.mem_base_pretrivializationAt z.proj
  · exact (hs.inter (a.pretrivializationAt z.proj).open_baseSet).prod isOpen_univ
  refine ⟨?_, mem_univ _⟩
  rw [e.coe_fst]
  · exact ⟨hz, a.mem_base_pretrivializationAt z.proj⟩
  · rw [e.mem_source]
    exact a.mem_base_pretrivializationAt z.proj

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
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
⊢ p ∈ (e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯).source →
    (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

Tactic:
rintro (⟨he, hs⟩ | ⟨he, hs⟩) <;> simp [*]

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
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑((gf.restr (f ⁻¹' g.source)).trans g.symm) y

Tactic:
change f y = g.symm (gf y)

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
⊢ f y = ↑g.symm (↑gf y)
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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ f e ∈ f '' {e | MulAction.stabilizer G e = ⊥}

Tactic:
replace hU := mem_of_mem_nhds hU

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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hGU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
hU : e ∈ U
⊢ f e ∈ f '' {e | MulAction.stabilizer G e = ⊥}
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mp
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
⊢ ‖u - 1‖ ^ 2 < 2 ^ 2 → -1 ∉ spectrum ℂ u

Tactic:
intro h h1

Goal state after:
case mp
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
h : ‖u - 1‖ ^ 2 < 2 ^ 2
h1 : -1 ∈ spectrum ℂ u
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ : Angle
⊢ ↑(↑θ.toCircle).arg = θ

Tactic:
induction θ using Angle.induction_on
  rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 2 * (1 - Real.cos ‖argSelfAdjoint u‖) = ‖↑(expUnitary (argSelfAdjoint u)) - 1‖ ^ 2

Tactic:
exact Eq.symm <| norm_sq_expUnitary_sub_one <| norm_argSelfAdjoint_le_pi u

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ 1 - ‖↑u - 1‖ ^ 2 / 2 ≤ 1

Tactic:
linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst✝¹ : FiniteDimensional k ↥s₁.direction
inst✝ : FiniteDimensional k ↥s₂.direction
⊢ FiniteDimensional k ↥(s₁ ⊔ s₂).direction

Tactic:
rcases eq_bot_or_nonempty s₁ with rfl | ⟨p₁, hp₁⟩

Goal state after:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
s₂ : AffineSubspace k P
inst✝¹ : FiniteDimensional k ↥s₂.direction
inst✝ : FiniteDimensional k ↥⊥.direction
⊢ FiniteDimensional k ↥(⊥ ⊔ s₂).direction

case inr
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst✝¹ : FiniteDimensional k ↥s₁.direction
inst✝ : FiniteDimensional k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ ↑s₁
⊢ FiniteDimensional k ↥(s₁ ⊔ s₂).direction
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
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Tactic:
rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
    Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]

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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v

Tactic:
have h₂ : r₂ ≠ 0 := by
    rintro rfl
    simp at 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
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
h₂ : r₂ ≠ 0
⊢ (r₃ / r₂) • ((r₂ • v +ᵥ p₁) -ᵥ p₁) = r₃ • v
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ p.toReal
⊢ Memℓp f p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
    exact (Set.Finite.of_summable_const (by simp) H).subset (Set.subset_univ _)
  · apply memℓp_infty
    have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
    simpa using ((Set.Finite.of_summable_const (by simp) H).image fun i => ‖f i‖).bddAbove
  exact (memℓp_gen_iff hp).2 hf

Goal state after: