mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ContinuousOn (Z.localTrivAsPartialEquiv i).invFun (Z.localTrivAsPartialEquiv i).target

Tactic:
refine continuousOn_isOpen_of_generateFrom fun t ht ↦ ?_
    simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
    obtain ⟨j, s, s_open, ts⟩ : ∃ j s, IsOpen s ∧
      t = (localTrivAsPartialEquiv Z j).source ∩ localTrivAsPartialEquiv Z j ⁻¹' s := ht
    rw [ts]
    simp only [preimage_inter]
    let e := Z.localTrivAsPartialEquiv i
    let e' := Z.localTrivAsPartialEquiv j
    let f := e.symm.trans e'
    have : IsOpen (f.source ∩ f ⁻¹' s) := by
      rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
      exact (continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open
    convert! this using 1
    dsimp [f, PartialEquiv.trans_source]
    rw [← preimage_comp, inter_assoc]

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
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : Z.TotalSpace
x✝ : p ∈ (Z.localTrivAsPartialEquiv i).source
⊢ (↑{ toPartialEquiv := Z.localTrivAsPartialEquiv i, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯,
            open_source := ⋯, open_target := ⋯ }
        p).1 =
    Z.proj p

Tactic:
simp only [mfld_simps]
    rfl

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 (e.baseSet ×ˢ univ) e'.target

Tactic:
e'.target_eq,

Goal state after:
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 (e.baseSet ×ˢ univ) (e'.baseSet ×ˢ univ)
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 _x ∈ e.target

Tactic:
exact e.map_source' hx

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
⊢ ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊

Tactic:
intro b

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
b : A
⊢ ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
⊢ ∀ (b : A), ‖a.toProd.2 b‖₊ ^ 2 ≤ ‖a.toProd.1‖₊ * ‖a.toProd.2 b‖₊ * ‖b‖₊

Tactic:
intro b

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
b : A
⊢ ‖a.toProd.2 b‖₊ ^ 2 ≤ ‖a.toProd.1‖₊ * ‖a.toProd.2 b‖₊ * ‖b‖₊
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C
h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊
b : A
⊢ ‖a.toProd.2 b‖₊ ^ 2 ≤ ‖a.toProd.1‖₊ * ‖a.toProd.2 b‖₊ * ‖b‖₊

Tactic:
calc
      ‖a.snd b‖₊ ^ 2 = ‖a.snd b * star (a.snd b)‖₊ := by
        simpa only [← sq] using CStarRing.nnnorm_self_mul_star.symm
      _ ≤ ‖b‖₊ * ‖a.fst (star (a.snd b))‖₊ :=
        ((a.central b (star (a.snd b))).symm ▸ nnnorm_mul_le _ _)
      _ = ‖a.fst (star (a.snd b))‖₊ * ‖b‖₊ := mul_comm _ _
      _ ≤ ‖a.fst‖₊ * ‖a.snd b‖₊ * ‖b‖₊ :=
        nnnorm_star (a.snd b) ▸ mul_le_mul_left (a.fst.le_opNNNorm _) _

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
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Tactic:
by
  refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_
  · rintro _ ⟨U, hU, s, hs, rfl⟩
    refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩)
      s.continuous).isOpen_range
    rwa [Subtype.range_val]
  · obtain ⟨f, hxf, rfl⟩ := hf x
    refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU,
      ⟨_, continuousOn_iff_continuous_domRestrict.mp (f.continuousOn_invFun.mono fun _ h ↦ h.1)⟩,
      ?_, (Set.range_domRestrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩
    · ext y; exact f.right_inv y.2.1
    · apply (f.symm_image_target_inter_eq _).trans
      rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
        f.source_preimage_target, f.source_inter_preimage_inv_preimage]

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
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
have := hf.discreteTopology_fiber

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : x ∈ V ×ˢ Set.univ
⊢ (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ f ⁻¹' V

Tactic:
dif_pos hx.1

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : x ∈ V ×ˢ Set.univ
⊢ inv x.2 ⋯ ∈ f ⁻¹' V
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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : x ∈ V ×ˢ Set.univ
⊢ (f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1),
      if he : f (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) ∈ V then
        idx (if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1) he
      else Classical.arbitrary ι) =
    x

Tactic:
dif_pos hx.1

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : x ∈ V ×ˢ Set.univ
⊢ (f (inv x.2 ⋯), if he : f (inv x.2 ⋯) ∈ V then idx (inv x.2 ⋯) he else Classical.arbitrary ι) = 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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
x : X × ι
hx : x ∈ V ×ˢ Set.univ
h : ¬(f (inv x.2 ⋯), idx (inv x.2 ⋯) ⋯).2 = x.2
⊢ False

Tactic:
exact (disjoint h).le_bot ⟨idx_U .., inv_U _ _⟩

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
| ↑x

Tactic:
← cfc_id' ℂ (x : A)

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
| cfc (fun x ↦ x) ↑x
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
y : F
x : E
⊢ y - A x ∈ (↑A).rangeᗮ ↔ (adjoint A) (y - A x) = 0

Tactic:
A.orthogonal_range,

Goal state after:
𝕜 : 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
y : F
x : E
⊢ y - A x ∈ (↑(adjoint A)).ker ↔ (adjoint A) (y - A x) = 0
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:
rw [isStarProjection_iff, and_congr_right_iff]

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
⊢ IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)
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
this✝ : CompleteSpace E
this : CompleteSpace F
⊢ A.kerᗮ = (adjoint A).range

Tactic:
simpa using! A.toContinuousLinearMap.orthogonal_ker

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mp
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✝ : CharZero k
s : Simplex k P n
p : P
⊢ p = s.centroid → ∑ i, (s.points i -ᵥ p) = 0

Tactic:
intro h
    rw [h, centroid_weighted_vsub_eq_zero]

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

Goal state before:
pp: 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
p : P
hs : ↑s = ∅
⊢ FiniteDimensional k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction

Tactic:
rw [coe_eq_bot_iff] at hs

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
p : P
hs : s = ⊥
⊢ FiniteDimensional k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inl
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 : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : ↑s = ∅
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1

Tactic:
rw [coe_eq_bot_iff] at hs

Goal state after:
case pos.inl
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 : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst✝¹⁴ : Ring R
inst✝¹³ : Ring S
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : Module.Finite R V
inst✝⁹ : Module.Free R V
inst✝⁸ : AffineSpace V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : Module S W
inst✝⁴ : Module.Finite S W
inst✝³ : SMulCommClass R S W
inst✝² : Module.Free S W
inst✝¹ : StrongRankCondition R
inst✝ : StrongRankCondition S
⊢ Module.finrank S (W × (V →ₗ[R] W)) = (Module.finrank R V + 1) * Module.finrank S W

Tactic:
Module.finrank_prod,

Goal state after:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst✝¹⁴ : Ring R
inst✝¹³ : Ring S
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : Module.Finite R V
inst✝⁹ : Module.Free R V
inst✝⁸ : AffineSpace V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : Module S W
inst✝⁴ : Module.Finite S W
inst✝³ : SMulCommClass R S W
inst✝² : Module.Free S W
inst✝¹ : StrongRankCondition R
inst✝ : StrongRankCondition S
⊢ Module.finrank S W + Module.finrank S (V →ₗ[R] W) = (Module.finrank R V + 1) * Module.finrank S W
Module: Mathlib.Analysis.Normed.Lp.lpSpace

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

Tactic:
intro b

Goal state after:
case h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
b : α
⊢ 0 ≤ ‖f b‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite

Tactic:
simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)

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 : ‖f‖ = 0
_i : Nonempty α
⊢ f = 0

Tactic:
have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using! lp.isLUB_norm f

Goal state after:
case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i ↦ ‖↑f i‖) 0
⊢ f = 0
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case left
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
⊢ ↑m ≤ N →
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
      iteratedFDeriv 𝕜 m (fun x ↦ ∑' (i : α), f i x) x

Tactic:
hm

Goal state after:
case left
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
    iteratedFDeriv 𝕜 m (fun x ↦ ∑' (i : α), f i x) x
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
⊢ ↑m < N → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m (fun x ↦ ∑' (i : α), f i x) x

Tactic:
hm

Goal state after:
case right
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
⊢ Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m (fun x ↦ ∑' (i : α), f i x) x
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn (fun x ↦ (√(1 + ‖x‖ ^ 2))⁻¹ • x) univ

Tactic:
by
    suffices Continuous fun (x : E) => (√(1 + ‖x‖ ^ 2))⁻¹ by fun_prop
    exact Continuous.inv₀ (by fun_prop) fun x => Real.sqrt_ne_zero'.mpr (by positivity)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x ↦ (f x).ofLp i

Tactic:
by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]
  rfl

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this✝ :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal
H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
this : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| = ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal

Tactic:
exact this ▸ hs

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
F : ι → ↥(lp E p)
hF : Bornology.IsBounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 f)
⊢ Memℓp f p

Tactic:
obtain ⟨C, hCF⟩ : ∃ C, ∀ k, ‖F k‖ ≤ C := hF.exists_norm_le.imp fun _ ↦ Set.forall_mem_range.1
  rcases eq_top_or_lt_top p with (rfl | hp)
  · apply memℓp_infty
    use C
    rintro _ ⟨a, rfl⟩
    exact norm_apply_le_of_tendsto (Eventually.of_forall hCF) hf a
  · apply memℓp_gen'
    exact sum_rpow_le_of_tendsto hp.ne (Eventually.of_forall hCF) hf

Goal state after: