mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)).source

pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ EqOn (↑(e'.symm.trans (e.restr s))) (↑((e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)))
    (e'.symm.trans (e.restr s)).source

Tactic:
· simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_toPartialEquiv_symm,
      PartialEquiv.restr_source, preimage_inter]
    -- Shuffle the intersections, pull e'.target into the interior and use interior_inter.
    rw [interior_eq_iff_isOpen.mpr hs,
      ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]
    congr 1
    nth_rw 2 [← interior_eq_iff_isOpen.mpr e'.open_target]
    rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ EqOn (↑(e'.symm.trans (e.restr s))) (↑((e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)))
    (e'.symm.trans (e.restr s)).source
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)

Tactic:
by
  have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
  refine ⟨?_, ?_⟩
  · simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_toPartialEquiv_symm,
      PartialEquiv.restr_source, preimage_inter]
    -- Shuffle the intersections, pull e'.target into the interior and use interior_inter.
    rw [interior_eq_iff_isOpen.mpr hs,
      ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]
    congr 1
    nth_rw 2 [← interior_eq_iff_isOpen.mpr e'.open_target]
    rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
  · simp [Set.eqOn_refl]

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

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ ∀ ⦃x : X'⦄, x ∈ f '' e.source → extend f (↑e) (fun x ↦ Classical.arbitrary Z) x ∈ e.target

Tactic:
rintro x ⟨x₀, hx₀, hxx₀⟩

Goal state after:
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ extend f (↑e) (fun x ↦ Classical.arbitrary Z) x ∈ e.target
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ (f ∘ e.invFun) (↑e x₀) = f x₀

Tactic:
comp_apply

Goal state after:
X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
x : X'
x₀ : X
hx₀ : x₀ ∈ e.source
hxx₀ : f x₀ = x
⊢ f (e.invFun (↑e x₀)) = f x₀
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hs
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
x✝ : z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = (f ∘ ↑e.symm) z
⊢ ↑e.symm z ∈ e'.source

Tactic:
comp_apply

Goal state after:
case hs
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
x✝ : z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = f (↑e.symm z)
⊢ ↑e.symm z ∈ e'.source
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:
convert! e.continuousOn_invFun

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
hs : IsOpen[inst✝⁴] s
proj : Z → ↑s
e : Trivialization F proj
inst✝ : Nonempty (B → F → Z)
⊢ ContinuousOn ((Pretrivialization.codExtend' hs e.toPretrivialization).invFun ∘ Prod.map Subtype.val id)
    e.toPretrivialization.target

Tactic:
convert! e.continuousOn_invFun

Goal state after:
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)
⊢ (Pretrivialization.codExtend' hs e.toPretrivialization).invFun ∘ Prod.map Subtype.val id = e.invFun
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:
rintro rfl

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
U : Set X
inj : Set.InjOn (fun x ↦ y) U
x' : X
x✝ : ∃ U ∈ 𝓝 x', Set.InjOn (fun x ↦ y) U
hU : U ∈ 𝓝 x'
⊢ x' ∈ U
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✝
T✝ : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst✝² : TopologicalSpace ι
inst✝¹ : LocallyCompactPair ι ↑T✝.baseSet
γ : C(ι, ↑T✝.baseSet)
i : ι
e : ↑T✝.source
T : Trivialization F proj
inst✝ : LocallyCompactPair ι ↑T.baseSet
⊢ C(↑T.source × C(ι, ↑T.baseSet), C(ι, ↑T.source))

Tactic:
let Ψ : C((T.source × C(ι, T.baseSet)) × ι, C(ι, T.baseSet) × ι) :=
    ⟨fun eγt => (eγt.1.2, eγt.2), by fun_prop⟩

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
inst✝⁴ : TopologicalSpace Z
inst✝³ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b✝ : B
y : E b✝
T✝ : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst✝² : TopologicalSpace ι
inst✝¹ : LocallyCompactPair ι ↑T✝.baseSet
γ : C(ι, ↑T✝.baseSet)
i : ι
e : ↑T✝.source
T : Trivialization F proj
inst✝ : LocallyCompactPair ι ↑T.baseSet
Ψ : C((↑T.source × C(ι, ↑T.baseSet)) × ι, C(ι, ↑T.baseSet) × ι) :=
  { toFun := fun eγt ↦ (eγt.1.2, eγt.2), continuous_toFun := ⋯ }
⊢ C(↑T.source × C(ι, ↑T.baseSet), C(ι, ↑T.source))
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
⊢ ↑f x ∈ ↑f.symm.symm.symm ⁻¹' gf.source

pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑(f.symm.trans gf) y

Tactic:
· apply (f.left_inv hxf).symm ▸ hgf

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = ↑(f.symm.trans gf) y
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
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
⊢ ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)

Tactic:
fun_prop (disch := aesop)

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
⊢ z ∈ centeredArc (s / ↑n)

Tactic:
by
  have hs0 : 0 < s := by
    contrapose! h2
    simp [centeredArc_eq_empty h2]
  have hn0 : n ≠ 0 := by
    contrapose! h1
    simp [h1]
  have hn : 1 ≤ (n : ℝ) := by simpa [Nat.one_le_iff_ne_zero]
  rw [mem_centeredArc ((div_le_self hs0.le hn).trans hs),
    lt_div_iff₀' (one_pos.trans_le hn)]
  rw [mem_centeredArc (div_le_self pi_nonneg hn)] at h1
  rwa [mem_centeredArc hs, coe_pow, ← arg_coe_angle_toReal_eq_arg, arg_pow_coe_angle,
    (Angle.nsmul_toReal_eq_mul hn0).mpr (mem_Ioc_of_Ioo ?_), abs_mul, Nat.abs_cast,
    arg_coe_angle_toReal_eq_arg] at h2
  rwa [neg_div, mem_Ioo, ← abs_lt, arg_coe_angle_toReal_eq_arg]

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

Goal state before:
pp: x y : Circle
t : ↑unitInterval
⊢ ↑(exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) t)) =
    ↑((⇑exp ∘ ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg))) t)

Tactic:
comp_apply

Goal state after:
x y : Circle
t : ↑unitInterval
⊢ ↑(exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) t)) =
    ↑(exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) t))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ -x ≠ y

Tactic:
rintro rfl

Goal state after:
x : Circle
hyx : -x ≠ x
hxP : x ∈ range ⇑((-x).path (-x))
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r : ℝ
hset : {x | |x| < r} = Ioo (-r) r
⊢ IsOpen (centeredArc r)

Tactic:
simpa [centeredArc, hset] using
    isLocalHomeomorph_circleExp.isOpenMap (Ioo (-r) r) isOpen_Ioo

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
⊢ ContinuousAt (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) u

Tactic:
obtain ⟨ε, huε, hε2⟩ := exists_between (sq_lt_sq₀ (by positivity) (by positivity) |>.mpr hu)

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
⊢ ContinuousAt (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) u
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
x : E
hx : x ∈ (↑T).ker
⊢ x ∈ (↑(adjoint T)).rangeᗮ

Tactic:
· rintro _ ⟨y, rfl⟩
    simp_all [T.adjoint_inner_left]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
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
y : F
x : E
hb : BddBelow (Set.range fun w ↦ ‖y - ↑w‖)
⊢ (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ (adjoint A) (y - A x) = 0

Tactic:
rw [← A.norm_eq_iInf_range_iff_adjoint_apply_eq_zero y x, le_antisymm_iff,
    and_iff_left (ciInf_le hb ⟨A x, x, rfl⟩), le_ciInf_iff hb]

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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
y : F
x : E
hb : BddBelow (Set.range fun w ↦ ‖y - ↑w‖)
⊢ (∀ (z : E), ‖y - A x‖ ≤ ‖y - A z‖) ↔ ∀ (i : ↥(↑A).range), ‖y - A x‖ ≤ ‖y - ↑i‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : CompleteSpace F
E : Type u_5
G : Type u_6
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup G
inst✝¹ : InnerProductSpace 𝕜 G
inst✝ : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
⊢ (toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) y) ∘SL f = toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) ((adjoint f) y)

Tactic:
comp_assoc,

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : CompleteSpace F
E : Type u_5
G : Type u_6
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup G
inst✝¹ : InnerProductSpace 𝕜 G
inst✝ : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
⊢ toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) y ∘SL f = toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) ((adjoint f) y)
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
i : Fin (n + 1)
⊢ (↑n + 1) • (s.centroid -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)

Tactic:
by
  rw [centroid_eq_smul_sum_vsub_vadd s i, vadd_vsub, smul_smul, mul_inv_cancel₀, one_smul]
  norm_cast

Goal state after:
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
⊢ (∀ (a : H →L[𝕜] H), (a ∘SL ↑(↑g).symm) ∘SL ↑↑f = (↑(↑g).symm ∘SL ↑↑f) ∘SL a) ↔ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
comp_assoc,

Goal state after:
𝕜 : 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
⊢ (∀ (a : H →L[𝕜] H), a ∘SL ↑(↑g).symm ∘SL ↑↑f = ↑(↑g).symm ∘SL ↑↑f ∘SL a) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
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
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n → n ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
rintro rfl

Goal state after:
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))
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ m = n

Tactic:
by simpa using Fintype.card_eq.2 ⟨e⟩

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
e : H ≃ₗᵢ[𝕜] H
e' : (H →L[𝕜] H)ˣ := { val := ↑↑e, inv := ↑↑e.symm, val_inv := ⋯, inv_val := ⋯ }
⊢ ↑↑e ∈ unitary (H →L[𝕜] H)

Tactic:
exact IsUnit.mem_unitary_of_star_mul_self ⟨e', rfl⟩ <|
          (e : H →L[𝕜] H).norm_map_iff_adjoint_comp_self.mp e.norm_map

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

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
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀) → ∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v

Tactic:
· rintro ⟨v, hp₀v⟩
    use v
    intro w hw
    have hs : vectorSpan k s ≤ k ∙ v := by
      rw [vectorSpan_eq_span_vsub_set_right k h, Submodule.span_le, Set.subset_def]
      intro x hx
      rw [SetLike.mem_coe, Submodule.mem_span_singleton]
      rw [Set.mem_image] at hx
      rcases hx with ⟨p, hp, rfl⟩
      rcases hp₀v p hp with ⟨r, rfl⟩
      use r
      simp
    have hw' := SetLike.le_def.1 hs hw
    rwa [Submodule.mem_span_singleton] at hw'

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
⊢ Collinear k {p₁, p₂}

Tactic:
rw [collinear_iff_exists_forall_eq_smul_vadd]

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₁ p₂ : P
⊢ ∃ p₀ v, ∀ p ∈ {p₁, p₂}, ∃ r, p = r • v +ᵥ 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
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₂

Tactic:
rintro rfl

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₁ p₃ : P
h : ¬Collinear k {p₁, p₁, p₃}
⊢ False
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
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₃

Tactic:
rintro rfl

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₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₁}
⊢ False
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
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₂ ≠ p₃

Tactic:
rintro rfl

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₁ p₂ : P
h : ¬Collinear k {p₁, p₂, p₂}
⊢ False
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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₂ ≠ 0

Tactic:
rintro rfl

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
hp₁ : p₁ ∈ s
v : V
h : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
hp₂ : 0 • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ 0 • v +ᵥ p₁
⊢ False
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
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' * x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
integral_mul_left_eq_self f x'

Goal state after: