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
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
have hs' := hs

Goal state after:
X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁵ : Unique n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Star A
inst✝ : Module R A
x✝ : CStarMatrix n n A
i j : n
⊢ (fun a x y ↦ a) ((fun M ↦ M default default) x✝) i j = x✝ i j

Tactic:
simp [Subsingleton.elim i default, Subsingleton.elim j default]

Goal state after:
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 : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x

Tactic:
obtain ⟨a, h_a⟩ := h_x

Goal state after:
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 ≤ x
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case pos
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet

Tactic:
obtain ⟨ed, hed⟩ : ∃ ed : Trivialization F (π F E), d ∈ ed.baseSet :=
      ⟨trivializationAt F E d, mem_baseSet_trivializationAt F E d⟩

Goal state after:
case pos
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
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
e✝ : Pretrivialization F proj
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ Prod.map Subtype.val id
      (⟨proj
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
          ⋯⟩,
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x

Tactic:
Prod.map_apply

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
e✝ : Pretrivialization F proj
x✝ : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
x : ↑s × F
hx : (↑x.1, x.2) ∈ e.target
⊢ (proj
        ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
          else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2),
      id
        (↑e
            ↑(if h : (↑x.1, x.2) ∈ e.target then ⟨e.invFun (↑x.1, x.2), ⋯⟩
              else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) x.1 x.2)).2) =
    Prod.map Subtype.val id x
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen[inst✝] U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
exact ⟨U, ho.mem_nhds hm, hi⟩

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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
⊢ g = 1

Tactic:
have := h.2.2.2.1

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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ g = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (⇑exp '' {x | -r < x ∧ x < r})

Tactic:
Set.Ioo_def

Goal state after:
r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (⇑exp '' Ioo (-r) r)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ 2⁻¹ ∈ unitInterval

Tactic:
simp only [mem_Icc, inv_nonneg, Nat.ofNat_nonneg, true_and]; linarith

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
⊢ Subtype.val '' closedBall 1 √ε ⊆ {a | IsStarNormal a ∧ spectrum ℂ a ⊆ sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}}

Tactic:
rintro - ⟨v, hv, rfl⟩

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : v ∈ closedBall 1 √ε
⊢ ↑v ∈ {a | IsStarNormal a ∧ spectrum ℂ a ⊆ sphere 0 1 ∩ {z | 2 * (1 - z.re) ≤ ε}}
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ u ∈ pathComponent 1 ↔ ∃ l, (List.map expUnitary l).prod = u

Tactic:
by
  constructor
  · revert u
    simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]
    refine IsClopen.connectedComponent_subset ?_ ⟨[], by simp⟩
    refine .of_thickening_subset_self zero_lt_two ?_
    intro u hu
    rw [mem_thickening_iff] at hu
    obtain ⟨v, ⟨⟨l, (hlv : (l.map expUnitary).prod = v)⟩, huv⟩⟩ := hu
    refine ⟨argSelfAdjoint (u * star v) :: l, ?_⟩
    simp [hlv, mul_assoc,
      expUnitary_eq_mul_inv u v (by simpa [Subtype.dist_eq, dist_eq_norm] using! huv)]
  · rintro ⟨l, rfl⟩
    induction l with
    | nil => simp
    | cons x xs ih => simpa using! (joined_one_expUnitary x).mul ih

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
A : E →L[𝕜] F
⊢ adjoint A ∘SL A = 0 ↔ A = 0

Tactic:
by rw [← norm_eq_zero]; simp [norm_adjoint_comp_self]

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

Goal state before:
pp: case mpr
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
⊢ ∑ i, (s.points i -ᵥ p) = 0 → p = s.centroid

Tactic:
· intro h
    rw [← vsub_eq_zero_iff_eq]
    have : ∑ i, (s.points i -ᵥ p) = ∑ i, ((s.points i -ᵥ s.centroid) - (p -ᵥ s.centroid)) := by
      apply sum_congr rfl
      intro x hx
      rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
    rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h
    simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h
    have h' : ((n : k) + 1) • (p -ᵥ s.centroid) = 0 := by norm_cast
    rw [smul_eq_zero_iff_right (by norm_cast)] at h'
    exact h'

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace 𝕜 E
inst✝⁶ : InnerProductSpace 𝕜 F
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
⊢ ⟪((toLin v₂.toBasis v₁.toBasis) Aᴴ) (v₂.toBasis i), v₁.toBasis j⟫_𝕜 =
    ⟪v₂.toBasis i, ((toLin v₁.toBasis v₂.toBasis) A) (v₁.toBasis j)⟫_𝕜

Tactic:
simp_rw [toLin_self]

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
m : Type u_5
n : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
v₁ : OrthonormalBasis n 𝕜 E
v₂ : OrthonormalBasis m 𝕜 F
A : Matrix m n 𝕜
i : m
j : n
⊢ ⟪∑ j, Aᴴ j i • v₁.toBasis j, v₁.toBasis j⟫_𝕜 = ⟪v₂.toBasis i, ∑ j_1, A j_1 j • v₂.toBasis j_1⟫_𝕜
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points)
hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points)
this : Set.range s.medial.points -ᵥ Set.range s.medial.points = (-↑n)⁻¹ • (Set.range s.points -ᵥ Set.range s.points)
⊢ Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points) =
    Submodule.span k (Set.range s.points -ᵥ Set.range s.points)

Tactic:
rw [this, Submodule.span_smul_eq_of_isUnit]
    simpa using NeZero.ne n

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
p : Fin 3 → P
⊢ AffineIndependent k p ↔ ¬finrank k ↥(vectorSpan k (Set.range p)) ≤ 1

Tactic:
affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)

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
p : Fin 3 → P
⊢ ¬finrank k ↥(vectorSpan k (Set.range p)) ≤ 1 ↔ ¬finrank k ↥(vectorSpan k (Set.range p)) ≤ 1
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

Tactic:
exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem

Goal state after:
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 + Module.finrank S (V →ₗ[R] W) = (Module.finrank R V + 1) * Module.finrank S W

Tactic:
Module.finrank_linearMap

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 R V * Module.finrank S W = (Module.finrank R V + 1) * Module.finrank S W
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'
          have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
          have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _
          have hf₂ := lp.hasSum_norm hp'' f
          have hg₂ := lp.hasSum_norm hp'' g
          -- apply Minkowski's inequality
          obtain ⟨C, hC₁, hC₂, hCfg⟩ :=
            Real.Lp_add_le_hasSum_of_nonneg hp' hf₁ hg₁ (norm_nonneg' _) (norm_nonneg' _) hf₂ hg₂
          refine le_trans ?_ hC₂
          rw [← Real.rpow_le_rpow_iff (norm_nonneg' (f + g)) hC₁ hp'']
          refine hasSum_le ?_ (lp.hasSum_norm hp'' (f + g)) hCfg
          intro i
          gcongr
          apply norm_add_le

Goal state after:
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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Tactic:
have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _

Goal state after:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0

Tactic:
· intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

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 α
hp : 0 < p
i : α
x : E i
this : Nonempty α
⊢ ‖lp.single p i x‖ = ‖x‖

Tactic:
induction p with
  | top =>
    simp only [norm_eq_ciSup, lp.coeFn_single]
    refine
      ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
    · obtain rfl | hij := Decidable.eq_or_ne i j
      · rw [Pi.single_eq_same]
      · rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
        exact norm_nonneg _
    · rw [Pi.single_eq_same]
  | coe p =>
    have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
    rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div,
      Real.rpow_rpow_inv _ this.ne', Pi.single_eq_same]
    · exact norm_nonneg _
    · intro j hji
      rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']

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

Goal state before:
pp: case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ (↑n) (↑(univUnitBall.trans' (unitBallBall c r h) ⋯).symm) (ball c r)

pp: case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n) (↑(IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph.symm) (ball c r)

Tactic:
· refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
    rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
    apply OpenPartialHomeomorph.mapsTo_symm

Goal state after:
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiffOn ℝ (↑n) (↑(IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph.symm) (ball c r)
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
H₁ :
  Integrable F' (μ.restrict (Set.Ioc a b)) ∧
    HasFDerivAt (fun x ↦ ∫ (a : ℝ) in Set.Ioc a b, F x a ∂μ) (∫ (a : ℝ) in Set.Ioc a b, F' a ∂μ) x₀
H₂ :
  Integrable F' (μ.restrict (Set.Ioc b a)) ∧
    HasFDerivAt (fun x ↦ ∫ (a : ℝ) in Set.Ioc b a, F x a ∂μ) (∫ (a : ℝ) in Set.Ioc b a, F' a ∂μ) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
exact ⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀

Tactic:
have diff_x₀ : ∀ᵐ a ∂μ, HasDerivAt (F · a) (F' x₀ a) x₀ :=
    h_diff.mono fun a ha ↦ ha x₀ (hε x₀_in)

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
⊢ Integrable (F' x₀) μ ∧ HasDerivAt (fun n ↦ ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
⊢ x ∈ μ.everywherePosSubset s ↔ x ∈ s \ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
simp [everywherePosSubset, pos_iff_ne_zero]

Goal state after: