mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : f.closure.toFun ⟨x, hx⟩ = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
simp only [Submodule.mk_eq_zero]

Goal state after:
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
f' : F →ₗ.[R] E
h : f.inverse.graph.topologicalClosure = f'.graph
x : E
hx : x ∈ f.closure.domain
hx' : f.closure.toFun ⟨x, hx⟩ = 0
⊢ x = 0
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ ↑T† y = 0

Tactic:
by
  classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
⊢ ∀ (i j : ι₁ × ι₂), inner 𝕜 (b₁ i.1 ⊗ₜ[𝕜] b₂ i.2) (b₁ j.1 ⊗ₜ[𝕜] b₂ j.2) = if i = j then 1 else 0

Tactic:
rintro ⟨i₁, i₂⟩ ⟨j₁, j₂⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : ι₁ → E
b₂ : ι₂ → F
hb₁ : Orthonormal 𝕜 b₁
hb₂ : Orthonormal 𝕜 b₂
i₁ : ι₁
i₂ : ι₂
j₁ : ι₁
j₂ : ι₂
⊢ inner 𝕜 (b₁ (i₁, i₂).1 ⊗ₜ[𝕜] b₂ (i₁, i₂).2) (b₁ (j₁, j₂).1 ⊗ₜ[𝕜] b₂ (j₁, j₂).2) = if (i₁, i₂) = (j₁, j₂) then 1 else 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1

Tactic:
refine CStarRing.norm_of_mem_unitary <| Matrix.det_of_mem_unitary ?_

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis ∈ Matrix.unitaryGroup ι 𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
⊢ mkMetric m₁ ≤ c • mkMetric m₂

Tactic:
refine fun s =>
    le_of_tendsto_of_tendsto (mkMetric'.tendsto_pre _ s)
      (ENNReal.Tendsto.const_mul (mkMetric'.tendsto_pre _ s) (Or.inr hc))
      (mem_of_superset (Ioo_mem_nhdsGT hr0) fun r' hr' => ?_)

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ r' ∈
    {x |
      (fun x ↦
          (fun r ↦ (mkMetric'.pre (fun s ↦ m₁ (ediam s)) r) s) x ≤
            (fun b ↦ c * (mkMetric'.pre (fun s ↦ m₂ (ediam s)) b) s) x)
        x}
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
rw [f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv']

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) f.rangeRestrict).det‖ = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
⊢ (mkMetric fun x ↦ ∞) = ⊤

Tactic:
simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]
  rw [le_iSup_iff]
  intro b hb
  simpa using hb ⊤

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
⊢ map (⇑(IsometryEquiv.vaddConst p')) volume = ‖v‖ₑ • map (⇑(IsometryEquiv.vaddConst p')) (map (⇑f) volume)

Tactic:
← Measure.map_smul

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
⊢ map (⇑(IsometryEquiv.vaddConst p')) volume = map (⇑(IsometryEquiv.vaddConst p')) (‖v‖ₑ • map (⇑f) volume)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ (if (t n).Nonempty then ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) else ⊥) = ∞

Tactic:
if_pos,

Goal state after:
case neg
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) = ∞

case neg.hc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
⊢ (t n).Nonempty
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg.hc
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
n : ℕ
hn : r < ediam (t n)
x : X
hx : x ∈ t n
⊢ (t n).Nonempty

Tactic:
exact ⟨x, hx⟩

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

Goal state before:
pp: case mpr.mem
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f✝ p f : H →L[𝕜] H
⊢ ((fun s ↦ star s * s) f).IsPositive

Tactic:
simpa using! ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
⊢ kernel (OfKernel K) = K

Tactic:
ext x y v

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
x y : X
v : V
⊢ (kernel (OfKernel K) x y) v = (K x y) v
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
⊢ x⁻¹ • ⇑f ⁻¹' (σ x • U) = ⇑f ⁻¹' U

Tactic:
rw [x_ne.isUnit.preimage_smul_setₛₗ _, inv_smul_smul₀ x_ne _]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ A = B

Tactic:
ContinuousLinearMapWOT.ext_iff,

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ ∀ (x : E), A x = B x
Module: Mathlib.Analysis.Matrix.LDL

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ Invertible ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ

Tactic:
haveI :=
    Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (Sᵀ.toNormedAddCommGroup hS.transpose)
        (Sᵀ.toInnerProductSpace hS.transpose.posSemidef) n _ _ _ (Pi.basisFun 𝕜 n))

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
this : Invertible ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))
⊢ Invertible ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
⊢ ⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

Tactic:
by
  by_cases ha : a = 0
  · simp [ha]
  apply (o.basisRightAngleRotation a ha).ext
  intro i
  fin_cases i
  · simp [mul_comm, o.areaForm_swap a x]
  · simp [mul_comm, real_inner_comm]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
| ↑f (e.symm x)

Tactic:
ContinuousLinearMap.coe_coe,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
| f (e.symm x)
Module: Mathlib.Analysis.Normed.Affine.Ceva

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
hp : ∀ (i : Fin 3), ∃ r, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) r = p i
⊢ ∏ i, dist (t.points (i + 1)) (p i) = ∏ i, dist (p i) (t.points (i + 2))

Tactic:
choose r hr using hp

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
r : Fin 3 → 𝕜
hr : ∀ (i : Fin 3), (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i) = p i
⊢ ∏ i, dist (t.points (i + 1)) (p i) = ∏ i, dist (p i) (t.points (i + 2))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
c : k
v : V
hc : 0 < c
⊢ c • v ∈ asymptoticCone k s ↔ v ∈ asymptoticCone k s

Tactic:
by
  simp_rw [mem_asymptoticCone_iff, asymptoticNhds_smul v hc]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s

Tactic:
rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedRing F
inst✝ : NormedAlgebra ℝ F
x : F
u : ℝ × ℝ
⊢ (aeval x) (X ^ 2 - C u.1 * X + C u.2) = φ x u

Tactic:
by
  simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ p 1 ≠ 0

Tactic:
rw [h]

Goal state after:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ 1 ≠ 0
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← hf1]; exact f.smul' _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
⊢ f (x * y * z) ≤ f (x * z) * seminormFromBounded' f y

Tactic:
mul_comm (f (x * z))

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
⊢ ∃ c, ∃ (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y

Tactic:
obtain ⟨c, _, hc⟩ := exists_mem_eq_sup' univ_nonempty (fun i : ι × ι ↦ B.norm (B i.1 * B i.2))

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ (x y : L), B.norm (x * y) ≤ c * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case e_f
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
k : K
y : L
j : ι
⊢ ‖(B.repr ((algebraMap K L) k * y)) j‖ = ‖k‖ * ‖(B.repr y) j‖

Tactic:
repr_smul',

Goal state after:
case e_f
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
i : ι
hBi : B i = 1
k : K
y : L
j : ι
⊢ ‖k * (B.repr y) j‖ = ‖k‖ * ‖(B.repr y) j‖
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nβ (f x) ^ n ≤ (C ^ (1 / ↑n) * nα x) ^ n

Tactic:
rw [mul_pow, h, ← hβ _ hn, ← map_pow]

Goal state after:
case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nβ (f (x ^ n)) ≤ C * nα x ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f x = 0

Tactic:
rw [h]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f 0 = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ spectralNorm K L 1 = 1

Tactic:
by
  have h1 : (1 : L) = algebraMap K L 1 := by rw [map_one]
  rw [h1, spectralNorm_extends, norm_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ normedMk x = 0

Tactic:
rw [h]

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
⊢ 0 x = 0
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: case h₁
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := ⋯
x : ι
a✝ : x ∈ s
⊢ edist (f.ofLp x) (h.ofLp x) ≤ edist (f.ofLp x) (g.ofLp x) + edist (g.ofLp x) (h.ofLp x)

Tactic:
exact edist_triangle ..

Goal state after:
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
x : X
⊢ ‖x‖ = ‖(P * Q) • x + (x - (P * Q) • x)‖

Tactic:
by rw [add_sub_cancel ((P * Q) • x) x]

Goal state after: