mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
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
⊢ ∃ t, IsOpen[instTopologicalSpaceProd] t ∧ Subtype.val ⁻¹' t = e'.setSymm ⁻¹' (↑e ⁻¹' s ∩ e.source)

Tactic:
refine ⟨u ∩ e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source, ?_, by
        simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]; rfl⟩

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' : 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
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ e'.target ∩ ↑e'.symm ⁻¹' e.source)
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
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x

Tactic:
rw [e.source_eq, ← preimage_comp]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 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
⊢ IsLocallyInjective f → ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
intro h x

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U
Module: Mathlib.Topology.SeparatedMap

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

Tactic:
intro h x

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

Goal state before:
pp: case e'_5
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
hs : IsOpen[inst✝⁴] s
proj : Z → ↑s
e : Trivialization F proj
inst✝ : Nonempty (B → F → Z)
x✝ : { x // x ∈ s } × F
⊢ ↑e.toPretrivialization.symm x✝ = ↑e.symm x✝

Tactic:
rfl

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

Goal state before:
pp: case zero
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x y : A
⊢ (a.toProd ^ 0).2 x * y = x * (a.toProd ^ 0).1 y

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x ↦ y) U
x' : X
⊢ x' ∈ {x} ↔ x' ∈ U

Tactic:
refine ⟨?_, fun h ↦ inj h (mem_of_mem_nhds hU) rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
x : X
x✝ : ∃ U ∈ 𝓝 x, Set.InjOn (fun x ↦ y) U
U : Set X
hU : U ∈ 𝓝 x
inj : Set.InjOn (fun x ↦ y) U
x' : X
⊢ x' ∈ {x} → x' ∈ U
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case fst
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ (↑𝕜 x).toProd.1 = ((algebraMap 𝕜 𝓜(𝕜, 𝕜)) x).toProd.1

Tactic:
rfl

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

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

Tactic:
rfl

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
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ (Homeomorph.setCongr this).symm x = (⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)) ⟨⟨↑x, ⋯⟩, ⋯⟩

Tactic:
rfl

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
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : X
hx : x ∈ s
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
lift x to s using hx

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
t : (x : ↑s) → ↑x ∈ Set.range f → { t // ↑x ∈ t.baseSet }
h : ∀ (x : ↑s), ↑x ∉ Set.range f → ∃ U ∈ 𝓝 ↑x, f ⁻¹' U = ∅
x : { x // x ∈ s }
⊢ IsEvenlyCovered f ↑x ↑(f ⁻¹' {↑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 : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝¹ : TopologicalSpace G := ⊥
this✝ : DiscreteTopology G
this : ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t, x ∈ t.baseSet
⊢ IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})

Tactic:
choose t ht using this

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 : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
t : (x : X) → x ∈ f '' {e | MulAction.stabilizer G e = ⊥} → Trivialization G f
ht : ∀ (x : X) (a : x ∈ f '' {e | MulAction.stabilizer G e = ⊥}), x ∈ (t x a).baseSet
⊢ IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : Group E
inst✝¹ : IsTopologicalGroup E
inst✝ : Group X
f : E →* X
hf : IsQuotientMap ⇑f
disc : IsDiscrete ↑f.ker
x✝¹ x✝ : E
⊢ f (x✝ * x✝¹⁻¹) = 1 ↔ x✝ * x✝¹⁻¹ ∈ f.ker

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ ∀ x ∈ spectrum ℝ a, x ≠ 0

Tactic:
grind

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

Goal state before:
pp: r : ℝ
hr : r ≤ π
⊢ r - -r ≤ 2 * π

Tactic:
grind

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

Goal state before:
pp: x y : Circle
h✝ : x ≠ y
h : Disjoint (⇑(x.path y) '' Ioo 0 1) (⇑(y.path x) '' Ioo 0 1)
⊢ insert ((x.path y) 0) (insert ((x.path y) 1) (⇑(x.path y) '' Ioo 0 1)) ∩
      insert ((y.path x) 0) (insert ((y.path x) 1) (⇑(y.path x) '' Ioo 0 1)) =
    {x, y}

Tactic:
grind

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

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∉ range ⇑((-x).path y)
t : ↑unitInterval
⊢ ((-x).path y) t ∈ {x}ᶜ

Tactic:
grind

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

Goal state before:
pp: case inr
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
hne : -x ≠ y
hP₂ : x ∉ range ⇑(y.path (-x))
⊢ ∀ (t : ↑unitInterval), (y.path (-x)).symm t ∈ {x}ᶜ

Tactic:
grind

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

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker

Tactic:
let e := AddCircle.homeomorphCircle one_ne_zero

Goal state after:
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
e : AddCircle 1 ≃ₜ Circle := homeomorphCircle ⋯
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
u : ↥(unitary A)
x✝ : A
⊢ ((mulLeft R A) u).symm x✝ = ((mulLeft R A) (star u)) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u : ↥(unitary A)
x✝ : A
⊢ (mulRight R u).symm x✝ = (mulRight R (star u)) x✝

Tactic:
rfl

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
this : ContinuousOn arg (spectrum ℂ ↑u)
| ↑u

Tactic:
rw [← cfc_id' ℂ (u : A)]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
| cfc (fun x ↦ x) ↑u
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
x : E
⊢ ⟪(adjoint A ∘SL A) x, x⟫_𝕜 = ⟪(adjoint A) (A x), x⟫_𝕜

Tactic:
rfl

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
x : E
⊢ ⟪x, (adjoint A ∘SL A) x⟫_𝕜 = ⟪x, (adjoint A) (A x)⟫_𝕜

Tactic:
rfl

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
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪(adjoint B) x, y⟫_𝕜

Tactic:
by simp only [adjoint_inner_left, h x y]

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
⊢ Real.arccos (1 - ‖↑u - 1‖ ^ 2 / 2) < Real.arccos (1 - 2 ^ 2 / 2)

Tactic:
by
        apply Real.arccos_lt_arccos (by norm_num) (by gcongr)
        linarith [(by positivity : 0 ≤ ‖(u - 1 : A)‖ ^ 2 / 2)]

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
hT : IsStarNormal T
x : E
⊢ (adjoint T) x = 0 ↔ T x = 0

Tactic:
simp_rw [← norm_eq_zero (E := E), ← isStarNormal_iff_norm_eq_adjoint.mp hT]

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
n : ℕ
s : Simplex k P n
⊢ s.centroid = (affineCombination k univ s.points) (centroidWeights k univ)

Tactic:
rfl

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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : s.centroid ∈ affineSpan k (s.points '' t)
⊢ t ⊂ Set.univ

Tactic:
grind

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪(adjoint B) x, y⟫_𝕜

Tactic:
by simp only [adjoint_inner_left, h x y]

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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOpposite i = s.face ⋯

Tactic:
rfl

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
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face ⋯
⊢ (affineCombination k {i}ᶜ s.points) (Function.const (Fin (n + 1)) (↑n)⁻¹) =
    (affineCombination k {i}ᶜ s.points) fun x ↦ (↑n)⁻¹

Tactic:
rfl

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
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
⊢ ContinuousLinearMap.adjoint.toLinearEquiv (toContinuousLinearMap ↑T) = toContinuousLinearMap ↑T ↔
    ContinuousLinearMap.adjoint T = T

Tactic:
rfl

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

Goal state before:
pp: case e_a
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 : Fin (n + 1)
⊢ (↑n)⁻¹ = 1 + (↑n)⁻¹ - 1

Tactic:
grind

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

Goal state before:
pp: case mp
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
hc : Fintype.card ι = finrank k ↥(vectorSpan k (Set.range p)) + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
rfl

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
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
x✝ : H
⊢ (let __src := ↑(u * v);
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star (u * v)), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝ =
    ((let __src := ↑u;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) *
        let __src := ↑v;
        { toLinearMap := ↑__src, invFun := ⇑↑↑(star v), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ })
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

pp: case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
· -- The zero-dimensional case.
    have : range b = univ :=
      AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
    simp [this]

Goal state after:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Tactic:
rfl

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
this : AffineIndependent k fun a ↦ if h : a = i₀ then ⋯ ▸ s.centroid else s.points a
⊢ AffineIndependent k p

Tactic:
grind

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p✝ : P
h : ∀ (i : Fin (n + 1)), p✝ ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p✝ = (p✝ -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p✝ -ᵥ s.centroid ∈ k ∙ u i
p : Fin (n + 1) → P := fun x ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent k fun i ↦ (if ↑i = i₀ then s.centroid else s.points ↑i) -ᵥ if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x // x ≠ i₀ } :=
  have h := ⋯;
  fun x ↦ ⟨↑x, ⋯⟩
x y : ↥{i₀}ᶜ
hxy : f x = f y
⊢ x = y

Tactic:
grind

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
hcard : #s' = n
⊢ 1 < #s'

Tactic:
grind

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ ball c f.rOut
⊢ ↑f x ≠ 0

Tactic:
← support_eq,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ support ↑f
⊢ ↑f x ≠ 0
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 (g * a) ∂μ

Tactic:
integral_mul_left_eq_self

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₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
h1 : Collinear k {p₁, p₃, p₂, p}
⊢ {p₁, p₂, p₃} ⊆ {p₁, p₃, p₂, p}

Tactic:
grind

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

Goal state before:
pp: case neg
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
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1

Tactic:
have hf' : ¬FiniteDimensional k (vectorSpan k (insert p (s : Set P))) := by
      intro h
      have h' : s.direction ≤ vectorSpan k (insert p (s : Set P)) := by
        conv_lhs => rw [← affineSpan_coe s, direction_affineSpan]
        exact vectorSpan_mono k (Set.subset_insert _ _)
      exact hf (Submodule.finiteDimensional_of_le h')

Goal state after:
case neg
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
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1