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

Goal state before:
pp: 𝕜 : 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✝³ : StarModule 𝕜 A
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : ContinuousStar A
a : A
ha : p a
⊢ (cfcHom ha).range = elemental 𝕜 a

Tactic:
rw [StarAlgHom.range_eq_map_top, ← ContinuousMap.elemental_id_eq_top, StarAlgebra.elemental,
    ← StarSubalgebra.topologicalClosure_map _ _ (cfcHom_isClosedEmbedding ha (R := 𝕜)).isClosedMap
      (cfcHom_continuous ha), StarAlgHom.map_adjoin]
  congr
  simpa using cfcHom_id ha

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

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (fun x ↦ star (f x) * f x) a = cfc 1 a ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

Tactic:
cfc_eq_cfc_iff_eqOn

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ Set.EqOn (fun x ↦ star (f x) * f x) 1 (spectrum R a) ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ x * y ∈ {x | ‖x‖ = 0}

Tactic:
apply le_antisymm _ (norm_nonneg' _)

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ ‖x * y‖ ≤ 0
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ (toDualMap 𝕜 E) 0 = ℓ

Tactic:
by simp [hℓ]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
this : cfc (⇑f) a = cfc 0 a
⊢ False

Tactic:
cfc_eq_cfc_iff_eqOn

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
hx' : x ∉ spectrum ℝ (φ a)
f : C(ℝ, ℝ)
h_eqOn : Set.EqOn (⇑f) 0 (spectrum ℝ (φ a))
h_eqOn_x : Set.EqOn (⇑f) 1 {x}
this : Set.EqOn (⇑f) 0 (spectrum ℝ a)
⊢ False
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: ⊢ ↑(exp 0) = ↑1

Tactic:
rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
e' : Y ≃ₜ Z
f'' : OpenPartialHomeomorph Z Z'
⊢ (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

Tactic:
simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc,
    trans_toOpenPartialHomeomorph]

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

Goal state before:
pp: 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 e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ ↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) z = ↑(e.symm.trans e') z

Tactic:
simp [hf.injective.extend_apply e']

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 : ι
⊢ ∀ ⦃x : Z.TotalSpace⦄,
    x ∈ Z.proj ⁻¹' Z.baseSet i →
      { proj := (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1,
          snd :=
            Z.coordChange i (Z.indexAt (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1)
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).2 } =
        x

Tactic:
rintro ⟨x, v⟩ hx
    replace hx : x ∈ Z.baseSet i := hx
    dsimp only
    rw [Z.coordChange_comp, Z.coordChange_self] <;> apply_rules [mem_baseSet_at, mem_inter]

Goal state after:
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 ∈ e.source
hl : ¬∀ᶠ (x : α) in l, f x ∈ 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)

Tactic:
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.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₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2

Tactic:
by
  rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
obtain ⟨U, hn, hi⟩ := h x
    exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩

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
s : Set B
hps : IsOpen[inst✝²] (proj ⁻¹' s)
e : Trivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ ContinuousOn e.toPretrivialization.invFun e.toPretrivialization.domExtend.target

Tactic:
by
    convert! e.continuousOn_invFun

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
e e' : ↑(f ⁻¹' {x})
this✝ : MulAction G ↑(f ⁻¹' {x}) := hf.mulActionFiber x
this : MulAction.IsPretransitive G ↑(f ⁻¹' {x})
⊢ ∃ g, ((hf.toPermFiber x) g) e = e'

Tactic:
obtain ⟨g, rfl⟩ := MulAction.IsPretransitive.exists_smul_eq e e' (M := G)

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
hf : IsQuotientCoveringMap f G
x : X
e : ↑(f ⁻¹' {x})
this✝ : MulAction G ↑(f ⁻¹' {x}) := hf.mulActionFiber x
this : MulAction.IsPretransitive G ↑(f ⁻¹' {x})
g : G
⊢ ∃ g_1, ((hf.toPermFiber x) g_1) e = g • e
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
⊢ IsCoveringMap (f ∘ ⇑g)

Tactic:
by
  rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢
  exact hf.comp_homeomorph g

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' Icc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * π) = univ

Tactic:
periodic_exp.image_Icc two_pi_pos

Goal state after:
x y : Circle
h : x ≠ y
⊢ range ⇑exp = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ insert ((y.path x) 1) (⇑(y.path x) '' Ioo 0 1) ∩ {exp (↑x).arg}ᶜ = ⇑(y.path x) '' Ioo 0 1

Tactic:
(y.path x).target,

Goal state after:
x y : Circle
h : x ≠ y
⊢ insert x (⇑(y.path x) '' Ioo 0 1) ∩ {exp (↑x).arg}ᶜ = ⇑(y.path x) '' Ioo 0 1
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
y : ℝ
hy : y ∈ spectrum ℝ ↑x
⊢ Real.cos ‖x‖ ≤ (fun a ↦ Real.cos a) y

Tactic:
exact Real.cos_abs y ▸ Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) hx <|
      spectrum.norm_le_norm_of_mem hy

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

Goal state before:
pp: T : ℝ
hT : T ≠ 0
a : AddCircle T
⊢ ∀ ⦃a₂ : AddCircle T⦄, a.toCircle = a₂.toCircle → a = a₂

Tactic:
b

Goal state after:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
⊢ a.toCircle = b.toCircle → a = b
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
⊢ a = b

Tactic:
induction a using QuotientAddGroup.induction_on

Goal state after:
case H
T : ℝ
hT : T ≠ 0
b : AddCircle T
z✝ : ℝ
h : toCircle ↑z✝ = b.toCircle
⊢ ↑z✝ = b
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize (normalize x) = normalize x

Tactic:
· simp [normalize_eq_self_of_norm_eq_one, hx]

Goal state after:
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
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ↑(normSq (↑x.re + I * ↑√(1 - x.re ^ 2))) = 1

Tactic:
Complex.normSq_ofReal_add_I_mul_sqrt_one_sub,

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
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ↑1 = 1

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
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ∀ (x : ↥(unitary A)) (i : ℝ), 0 < i ∧ i < 2 → IsPathConnected {y | (y, x) ∈ {p | dist p.1 p.2 < i}}

Tactic:
by
    simpa using! isPathConnected_ball

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✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : F
f : E →L[𝕜] F
⊢ (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) ((adjoint f) x)

Tactic:
by
  ext; simp [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
⊢ IsStarNormal T ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
rw [isStarNormal_iff, Commute, SemiconjBy, ← sub_eq_zero]

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
⊢ star T * T - T * star T = 0 ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
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✝ : CharZero k
s : Simplex k P n
p : P
h : ∑ i, (s.points i -ᵥ p) = 0
x : Fin (n + 1)
hx : x ∈ univ
⊢ s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)

Tactic:
vsub_sub_vsub_cancel_right _ _ s.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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : ∑ i, (s.points i -ᵥ p) = 0
x : Fin (n + 1)
hx : x ∈ univ
⊢ s.points x -ᵥ p = s.points x -ᵥ p
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ (LinearIndependent k fun i ↦ p ↑i -ᵥ p i₁) ↔ finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
linearIndependent_iff_card_eq_finrank_span,

Goal state after:
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
i₁ : ι
⊢ Fintype.card { x // x ≠ i₁ } = Set.finrank k (Set.range fun i ↦ p ↑i -ᵥ p i₁) ↔
    finrank k ↥(vectorSpan k (Set.range p)) = n
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = #{x | x ≠ i₁} ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n

Tactic:
simp [Finset.filter_ne', Finset.card_erase_of_mem, 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
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
⊢ Fintype.card ι ≤ finrank k ↥(vectorSpan k (Set.range p)) + 1

Tactic:
cases isEmpty_or_nonempty ι
  · simp [Fintype.card_eq_zero]
  rw [← tsub_le_iff_right]
  exact (affineIndependent_iff_le_finrank_vectorSpan _ _
    (tsub_add_cancel_of_le <| Nat.one_le_iff_ne_zero.2 Fintype.card_ne_zero).symm).1 hp

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

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ BddAbove (Set.range fun i ↦ ‖(f + g) i‖)

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ∞
hg : Memℓp g ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
⊢ BddAbove (Set.range fun i ↦ ‖(f + g) i‖)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
⊢ {i | (c • f) i ≠ 0}.Finite

Tactic:
refine hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ∞
⊢ Memℓp (c • f) ∞

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove

Goal state after:
case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
⊢ Memℓp (c • f) ∞
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

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

Tactic:
by
  by_cases hr : 0 < r
  · rw [univBall_target c hr]
  · rw [univBall, dif_neg hr]
    exact subset_univ _

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
t : Set H
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (f x).ofLp i) t

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]
  rfl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inr
x y : ℝ
hxy : x ≤ y
hx : 0 < x
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
simp [expNegInvGlue, not_le.2 hx, not_le.2 (hx.trans_le hxy),
    inv_le_inv₀ (hx.trans_le hxy) hx, hxy]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ ↑(m + 1) fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]

Goal state after:
case succ
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (↑m + 1) fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 1 < R
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)

Tactic:
rw [← sub_pos] at hR

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
x : E
hR : 0 < R - 1
⊢ ContDiffAt ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (R, x)
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x ↦ ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x

Tactic:
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x ↦ re ⟪x, x⟫) (2 • (innerSL ℝ) x) x
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : ‖y‖ < |1|
⊢ 0 < 1 - ‖y‖ ^ 2

Tactic:
← abs_norm,

Goal state after:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : |‖y‖| < |1|
⊢ 0 < 1 - ‖y‖ ^ 2
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: case e_a.e_μ.e_s
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
y : E
⊢ y ∈ ⇑e.symm ⁻¹' s ↔ y ∈ R • s

Tactic:
mem_smul_set_iff_inv_smul_mem₀ hR

Goal state after:
case e_a.e_μ.e_s
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
y : E
⊢ y ∈ ⇑e.symm ⁻¹' s ↔ R⁻¹ • y ∈ s
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case hfs
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ x ∈ k'

Tactic:
refine ⟨p, hp, p⁻¹ * x, ?_, by simp⟩

Goal state after:
case hfs
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ p⁻¹ * x ∈ k⁻¹