mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
⊢ f x 0 = 0 → ContinuousMap.mkD (f x) ↑g = ↑(mkD (f x) g)

Tactic:
zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompactSpace Y
inst✝³ : Zero Y
s : Set X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(Y, E)
hs : MeasurableSet s
f : X → Y → E
g : C(Y, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0
x : X
zero_x : f x 0 = 0
⊢ ContinuousMap.mkD (f x) ↑g = ↑(mkD (f x) g)
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
x : X
⊢ f x ↑0 = 0 → ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)

Tactic:
zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)
Module: Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
s : Set X
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
hs : MeasurableSet s
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0
x : X
⊢ f x ↑0 = 0 → ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)

Tactic:
zero_x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : TopologicalSpace Y
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
s : Set X
t : Set Y
inst✝⁴ : CompactSpace ↑t
inst✝³ : Zero ↑t
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : SecondCountableTopologyEither X C(↑t, E)
hs : MeasurableSet s
f : X → Y → E
g : C(↑t, E)₀
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
f_zero : ∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0
x : X
zero_x : f x ↑0 = 0
⊢ ContinuousMap.mkD (t.domRestrict (f x)) ↑g = ↑(mkD (t.domRestrict (f x)) g)
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
⊢ Function.Injective ⇑toCLM

Tactic:
injective_iff_map_eq_zero

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
⊢ ∀ (a : CStarMatrix m n A), toCLM a = 0 → a = 0
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ f x 0 = 0 → f x ↑z = (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) z

Tactic:
zero_x

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
z : ↑(quasispectrum 𝕜 a)
x : X
cont_x : ContinuousOn (f x) (quasispectrum 𝕜 a)
zero_x : f x 0 = 0
⊢ f x ↑z = (mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) z
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
L : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : IsOrderedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : EquivLike L E F
inst✝ : LinearEquivClass L 𝕜 E F
f : L
s : Set E
⊢ ⇑f '' extremePoints 𝕜 s = extremePoints 𝕜 (⇑f '' s)

Tactic:
by
  ext b
  obtain ⟨a, rfl⟩ := EquivLike.surjective f b
  have : ∀ x y, f '' openSegment 𝕜 x y = openSegment 𝕜 (f x) (f y) :=
    image_openSegment _ (LinearMapClass.linearMap f).toAffineMap
  simp only [mem_extremePoints, (EquivLike.surjective f).forall,
    (EquivLike.injective f).mem_set_image, (EquivLike.injective f).eq_iff, ← this]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝² x✝¹ x✝ : f.PreGNS
⊢ f (star (f.ofPreGNS (x✝² + x✝¹)) * f.ofPreGNS x✝) =
    f (star (f.ofPreGNS x✝²) * f.ofPreGNS x✝) + f (star (f.ofPreGNS x✝¹) * f.ofPreGNS x✝)

Tactic:
by rw [map_add, star_add, add_mul, map_add]

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

Goal state before:
pp: case refine_1
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
⊢ a = e

Tactic:
suffices t • (e * (1 - a : A⁺¹) * e) = 0 by
      rw [← h0t.ne'.isUnit.smul_left_cancel, ← he.conjugate_of_nonneg_of_le
          (smul_nonneg h0t.le ha) ?hae]
      case hae => simpa [hlin] using le_add_of_nonneg_right (a := t • a) (by positivity : 0 ≤ s • b)
      apply inr_injective (R := ℂ) <| Eq.symm ?_
      simpa only [mul_one_sub_mul, he.inr.isIdempotentElem.eq, smul_sub, sub_eq_zero,
        smul_mul_assoc, mul_smul_comm, smul_sub, inr_mul, inr_smul]

Goal state after:
case refine_1
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 * (1 - ↑a) * ↑e) = 0
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 ∈ Multiset.map (fun x ↦ ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

Tactic:
intro x h_x
      rw [Multiset.mem_map] at h_x
      obtain ⟨a, h_a⟩ := h_x
      rw [← h_a.2]
      apply sq_nonneg

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

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
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV) (↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y)) =
    ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

Tactic:
· rw [(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV]
    change _ = U.openPartialHomeomorphSubtypeCoe hU _
    rw [(U.openPartialHomeomorphSubtypeCoe hU).right_inv hy.2]

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
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
z : Z
hz : z ∈ e.target
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) ((f ∘ e.invFun) z) = z

Tactic:
by simpa only [comp_apply, hf.injective.extend_apply e] using! e.right_inv' hz

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
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
⊢ ∀ (p : Z), proj p = a → ↑e p = ↑(e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) p

Tactic:
by
    rintro p rfl
    ext1
    · simp [*]
    · simp [*]

Goal state after:
Module: Mathlib.Topology.Covering.AddCircle

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
⊢ IsAddQuotientCoveringMap (fun x ↦ n • x) ↥(nsmulAddMonoidHom n).ker

Tactic:
convert! isAddQuotientCoveringMap_zsmul p (n := n) (mod_cast hn)

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝ : AddCircle p
⊢ HSMul.hSMul n = HSMul.hSMul ↑n

case e'_6
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
x✝ : AddCircle p
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n

case e'_7
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n

case e'_8
𝕜 : Type u_1
inst✝³ : TopologicalSpace 𝕜
inst✝² : Ring 𝕜
inst✝¹ : IsTopologicalRing 𝕜
p : 𝕜
inst✝ : T0Space (AddCircle p)
n : ℕ
hn : IsUnit ↑n
e_6✝ : ↥(nsmulAddMonoidHom n).ker = ↥(zsmulAddGroupHom ↑n).ker
e_7✝ : (nsmulAddMonoidHom n).ker.toAddGroup ≍ (zsmulAddGroupHom ↑n).ker.toAddGroup
⊢ nsmulAddMonoidHom n = zsmulAddGroupHom ↑n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r s : ℝ
⊢ exp r = exp s ↔ r ≡ s [PMOD 2 * π]

Tactic:
simp [AddCommGroup.modEq_iff_zsmul', ← exp_eq_one, div_eq_one, eq_comm (a := exp r)]

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
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
have hV' e : IsOpen (V' e) := (hV e).2.inter (φ e).open_source

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)
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
⊢ ‖cfc (fun x ↦ x - 1 x) u‖ ^ 2 = 2 * (1 - x)

Tactic:
have h₃ : IsGreatest ((‖· - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (· - 1 : ℂ → ℂ) u‖ ^ 2) := by
    have := pow_left_monotoneOn (n := 2) |>.mono (s₂ := ((‖· - 1‖) '' spectrum ℂ u)) (by simp)
    simpa [Set.image_image] using this.map_isGreatest (IsGreatest.norm_cfc (fun z : ℂ ↦ z - 1) u)

Goal state after:
case inr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
h₂ : IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
h₃ : IsGreatest ((fun x ↦ ‖x - 1‖ ^ 2) '' spectrum ℂ u) (‖cfc (fun x ↦ x - 1) u‖ ^ 2)
⊢ ‖cfc (fun x ↦ x - 1 x) u‖ ^ 2 = 2 * (1 - 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
h : IsLocalHomeomorph f
e : E
⊢ ContinuousAt f e

Tactic:
obtain ⟨φ, hφ, rfl⟩ := h e

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
e : E
φ : OpenPartialHomeomorph E X
hφ : e ∈ φ.source
h : IsLocalHomeomorph ↑φ
⊢ ContinuousAt (↑φ) e
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
⊢ a + I • CFC.sqrt (1 - a ^ 2) ∈ unitary A

Tactic:
key,

Goal state after:
case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
⊢ cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a ∈ unitary 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
T : E →L[𝕜] F
⊢ (↑T).kerᗮ = (↑(adjoint T)).range.topologicalClosure

Tactic:
rw [← Submodule.orthogonal_orthogonal_eq_closure]
  apply le_antisymm
  all_goals refine Submodule.orthogonal_le fun x hx ↦ ?_
  · refine ext_inner_left 𝕜 fun y ↦ ?_
    simp [← T.adjoint_inner_left, hx _]
  · rintro _ ⟨y, rfl⟩
    simp_all [T.adjoint_inner_left]

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:
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
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
⊢ adjoint (A ∘ₗ B) = adjoint B ∘ₗ adjoint A

Tactic:
by
  ext v
  refine ext_inner_left 𝕜 fun w => ?_
  simp only [adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply]

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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Finset.centroid k univ (s.reindex e).points = s.centroid

Tactic:
centroid

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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Finset.centroid k univ (s.reindex e).points = Finset.centroid k univ s.points
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
⊢ #s ≤ #t

Tactic:
have := hs'.to_subtype

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty ↥s
⊢ #s ≤ #t
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ #s < #t

Tactic:
have := hs'.to_subtype

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this : Nonempty ↥s
⊢ #s < #t
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
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
⊢ affineSpan k ↑(Finset.image p s) = sp

Tactic:
by
  have hn : s.Nonempty := by
    rw [← Finset.card_pos, hc]
    apply Nat.succ_pos
  refine eq_of_direction_eq_of_nonempty_of_le ?_ ((hn.image p).to_set.affineSpan k) hle
  have hd := direction_le hle
  rw [direction_affineSpan] at hd ⊢
  exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ici c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Iic c) μ

Tactic:
simpa using hf.comp_inv

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iic c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Ici c) μ

Tactic:
simpa using hf.comp_inv

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ioi c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Iio c) μ

Tactic:
simpa using hf.comp_inv

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁶ : MeasurableSpace G
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
inst✝⁴ : PartialOrder G
inst✝³ : CommGroup G
inst✝² : IsOrderedMonoid G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iio c⁻¹) μ
⊢ IntegrableOn (fun x ↦ f x⁻¹) (Set.Ioi c) μ

Tactic:
simpa using hf.comp_inv

Goal state after:
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✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), -f a ∂μ

Tactic:
← hf',

Goal state after:
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✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), f (g * a) ∂μ
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
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), -f a ∂μ

Tactic:
← hf',

Goal state after:
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
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), f (a * g) ∂μ
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 : ↥(lp E p)
⊢ ‖-f‖ = ‖f‖

Tactic:
by
  rcases p.trichotomy with (rfl | rfl | hp)
  · simp only [norm_eq_card_dsupport, coeFn_neg, Pi.neg_apply, ne_eq, neg_eq_zero]
  · cases isEmpty_or_nonempty α
    · simp only [lp.eq_zero' f, neg_zero, norm_zero]
    apply (lp.isLUB_norm (-f)).unique
    simpa only [coeFn_neg, Pi.neg_apply, norm_neg] using lp.isLUB_norm f
  · suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
      exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this
    apply (lp.hasSum_norm hp (-f)).unique
    simpa only [coeFn_neg, Pi.neg_apply, _root_.norm_neg] using lp.hasSum_norm hp f

Goal state after: