mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : Pretrivialization F proj
s : Set B
⊢ ↑e.symm ⁻¹' proj ⁻¹' s ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ

Tactic:
by
  ext ⟨x, y⟩
  suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
    simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]
  intro h
  rw [e.proj_symm_apply' h]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
let := a.totalSpaceTopology

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ ↑e'.symm ⁻¹' e.source)
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
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ ↑e.toPartialEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ (e.source ∩ e.source)

Tactic:
inter_self

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ ↑e.toPartialEquiv ⁻¹' s ∩ e.source = ↑e ⁻¹' s ∩ e.source
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
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : ↑e ∘ ↑e'.symm ⁻¹' s ∩ (e'.target ∩ ↑e'.symm ⁻¹' e.source) = u ∩ (e'.target ∩ ↑e'.symm ⁻¹' e.source)
hu3 :
  (fun x ↦ ↑x) ⁻¹' ↑e ∘ ↑e'.symm ⁻¹' s ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source =
    (fun x ↦ ↑x) ⁻¹' u ∩ (fun x ↦ ↑x) ⁻¹' ↑e'.symm ⁻¹' e.source
⊢ Subtype.val ⁻¹' (u ∩ e'.target ∩ ↑e'.symm ⁻¹' e.source) = e'.setSymm ⁻¹' (↑e ⁻¹' s ∩ e.source)

Tactic:
by
        simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]; rfl

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
⊢ Continuous[inst✝ b, a.totalSpaceTopology] (TotalSpace.mk b)

Tactic:
let := a.totalSpaceTopology

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous[inst✝ b, a.totalSpaceTopology] (TotalSpace.mk b)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
h : IsInducing (↑(a.pretrivializationAt b) ∘ TotalSpace.mk b)
⊢ IsInducing (TotalSpace.mk b)

Tactic:
let := a.totalSpaceTopology

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
b : B
h : IsInducing (↑(a.pretrivializationAt b) ∘ TotalSpace.mk b)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ IsInducing (TotalSpace.mk b)
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
⊢ Continuous[a.totalSpaceTopology, inst✝²] TotalSpace.proj

Tactic:
let := a.totalSpaceTopology

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous[a.totalSpaceTopology, inst✝²] TotalSpace.proj
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)

Tactic:
let := a.totalSpaceTopology

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ ContinuousOn f (TotalSpace.proj ⁻¹' s)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.1 ∈ e.baseSet
right✝ : x.2 ∈ univ
⊢ { proj := x.1, snd := e.symm x.1 x.2 } = ↑e.symm x

Tactic:
e.mk_symm hx

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : ∀ (x : B), Nonempty (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.1 ∈ e.baseSet
right✝ : x.2 ∈ univ
⊢ ↑e.symm (x.1, x.2) = ↑e.symm x
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
⊢ MulAction.IsPretransitive G ↑(f ⁻¹' {x})

Tactic:
let := hf.mulActionFiber x
  constructor
  intro e e'
  obtain ⟨g, hg⟩ := hf.apply_eq_iff_mem_orbit.mp (e'.2.trans e.2.symm)
  exact ⟨g, Subtype.ext hg⟩

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ range ⇑(x.path y) ∪ range ⇑(y.path x) = univ

Tactic:
range_path,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ range ⇑(y.path x) = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ range ⇑(y.path x) = univ

Tactic:
range_path,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ ⇑exp '' Icc (↑y).arg (y.angleDiff x + (↑y).arg) = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Ioo 0 1

Tactic:
range_path,

Goal state after:
x y : Circle
h : x ≠ y
⊢ (⇑exp '' Icc (↑x).arg (x.angleDiff y + (↑x).arg))ᶜ = ⇑(y.path x) '' Ioo 0 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H
T : ℝ
hT : T ≠ 0
z✝ : ℝ
⊢ ((homeomorphAddCircle T (2 * π) hT homeomorphCircle._proof_1).trans homeomorphCircle') ↑z✝ = toCircle ↑z✝

Tactic:
Homeomorph.trans_apply,

Goal state after:
case H
T : ℝ
hT : T ≠ 0
z✝ : ℝ
⊢ homeomorphCircle' ((homeomorphAddCircle T (2 * π) hT homeomorphCircle._proof_1) ↑z✝) = toCircle ↑z✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
hz1 : z ∈ centeredArc (π / 2)
n : ℕ
ih : z ∈ centeredArc (π / 2 ^ (n + 1))
⊢ z ∈ centeredArc (π / ↑(2 ^ (n + 1)))

Tactic:
simpa

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

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

Tactic:
conv_rhs => rw [← expUnitary_argSelfAdjoint hu]
  exact Eq.symm <| norm_sq_expUnitary_sub_one <| norm_argSelfAdjoint_le_pi u

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ 1 ∈ ball 1 δ

Tactic:
simpa

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
h : p = s.centroid
⊢ ∑ i, (s.points i -ᵥ p) = 0

Tactic:
rw [h, centroid_weighted_vsub_eq_zero]

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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ (s.map f hf).centroid = f s.centroid

Tactic:
rw [centroid, map_points, centroid_eq_affineCombination, Finset.map_affineCombination]

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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ Finset.centroid k univ (⇑f ∘ s.points) = (affineCombination k univ (⇑f ∘ s.points)) (centroidWeights k univ)

case hw
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
inst✝³ : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective ⇑f
⊢ univ.sum (centroidWeights k univ) = 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
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ (↑n)⁻¹ • n • (s.points j -ᵥ s.points i) + (↑n)⁻¹ • (s.points j -ᵥ s.points i) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)

Tactic:
add_comm

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✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 : ∀ (i : Fin (n + 1)), ∑ x, (s.points x -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ (↑n)⁻¹ • (s.points j -ᵥ s.points i) + (↑n)⁻¹ • n • (s.points j -ᵥ s.points i) =
    (↑n)⁻¹ • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
x : H
this : f ((adjoint ↑↑f) (g x)) = (starRingEnd 𝕜) y • f x
⊢ ↑↑g x = (star y • ↑↑f) x

Tactic:
simpa

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
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ p ∈ ∅, ∃ r, p = r • v +ᵥ p₀

pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
· simp [collinear_empty]

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut

Tactic:
exact f.rIn_lt_rOut

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}

Tactic:
Collinear,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Collinear k {p₁, p₂, p₃}
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Collinear k {p₁, p₂, p₃}

Tactic:
Collinear,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Module.rank k ↥(vectorSpan k (insert p₁ s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k {p₁, p₂, p₃}) ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Collinear k (insert p s) ↔ Collinear k s

Tactic:
Collinear,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Collinear k s
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Collinear k s

Tactic:
Collinear,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 1 ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.inr
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
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ finrank k ↥s.direction + 1

Tactic:
add_comm

Goal state after:
case pos.inr
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
p₀ : P
hp₀ : p₀ ∈ ↑s
⊢ finrank k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank k ↥s.direction
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ ∀ i ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0

Tactic:
intro i hi

Goal state after:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset
⊢ ‖f i‖ ^ p.toReal = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr.refine_2
α : 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
⊢ ∀ (i : α), ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖

Tactic:
intro i hi

Goal state after:
case inr.inr.inr.inr.inr.refine_2
α : 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
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖f i‖
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 ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i ↦ ‖g i‖)
⊢ BddAbove (Set.range fun i ↦ ‖(f + g) i‖)

Tactic:
refine ⟨A + B, ?_⟩

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‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i ↦ ‖g i‖)
⊢ A + B ∈ upperBounds (Set.range fun i ↦ ‖(f + g) i‖)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
rw [norm_eq_tsum_rpow hp, ← Real.rpow_mul]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal

case hx
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ 0 ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x ↦ g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)‖ ≤ u n

Tactic:
simpa

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)
f : ↥(lp E p)
⊢ f = 0 → ‖f‖ = 0

Tactic:
rintro rfl; exact norm_zero

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun n ↦ g n y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)‖ ≤ u n

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ ∀ (n : α) (x : 𝕜), ‖ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)‖ ≤ u n

Tactic:
simpa

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)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
rw [lp.norm_rpow_eq_tsum hp f]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ∑' (i : α), ‖↑f i‖ ^ p.toReal