mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hxy.e'_6.a
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p = (∫⋯∫⁻_{j}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p

Tactic:
congr! 1
                rw [← lmarginal_union μ f hf]
                · congr
                  rw [Finset.union_comm]
                  rfl
                · rw [Finset.disjoint_singleton]
                  exact fun h ↦ hi (h ▸ hj)

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ Antitone fun s ↦ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s

Tactic:
rw [Finset.antitone_iff_forall_insert_le]
  intro s i hi
  -- apply the lemma designed to encapsulate the inductive step
  convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
  · rw [← lmarginal_union μ f hf]
    · rw [← insert_compl_insert hi]
      rfl
    rw [Finset.disjoint_singleton_left, notMem_compl]
    exact mem_insert_self i s
  · -- the main nontrivial point is to check that an exponent `p` satisfying `0 ≤ p` and
    -- `(#ι - 1) * p ≤ 1` is in the valid range for the inductive-step lemma
    refine le_trans ?_ hp
    gcongr
    suffices (s.card : ℝ) + 1 ≤ #ι by linarith
    rw [← card_add_card_compl s]
    norm_cast
    gcongr
    have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
    rwa [← card_pos] at hi'

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x y : Fin n → E
⊢ (innerProductForm ((ιMulti ℝ n) x)) ((ιMulti ℝ n) y) = (of fun i j ↦ ⟪x j, y i⟫).det

Tactic:
simp [innerProductForm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
⊢ IsUnit f

Tactic:
by
  rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]
  have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
  refine ⟨?_, ⟨_, h_anti⟩⟩
  rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]
  intro x hx
  have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
    (by positivity)
  aesop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
⊢ M.PosSemidef ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
classical
  have := Fintype.ofFinite n
  rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]
  simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
    ContinuousLinearMap.toLinearMap_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
  exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ birkhoffAverage R f g n x = g x

Tactic:
birkhoffAverage,

Goal state after:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ (↑n)⁻¹ • birkhoffSum f g n x = g x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case neg.inl
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p' : ℝ≥0
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
n' : ℝ≥0 := (↑n).conjExponent
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hp : 1 ≤ 1
hp' : (↑p')⁻¹ = ↑1⁻¹ - (↑n)⁻¹
h2p : ↑1 < ↑n
hnp : 0 < ↑n - ↑1
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑1) * eLpNorm (fderiv ℝ u) (↑1) μ

Tactic:
convert! eLpNorm_le_eLpNorm_fderiv_one μ hu h2u hn using 2
    · suffices (p' : ℝ) = n' by simpa using this
      rw [← inv_inj, hp']
      simp [field, n', NNReal.conjExponent, *]
    · norm_cast
      simp_rw [n', n, eLpNormLESNormFDerivOfEqInnerConst]
      simp only [n, NNReal.coe_one] at hnp
      field_simp
      simp

Goal state after:
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 = (adjointAux hT) y

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

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:

Tactic:
eLpNorm u p' μ
      = eLpNorm (e.symm ∘ v) p' μ := by simp_rw [v, Function.comp_def, e.symm_apply_apply]
    _ ≤ C₁ • eLpNorm v p' μ := by
      apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
      exact Eventually.of_forall (fun x ↦ (e.symm : F' →L[ℝ] F).le_opNNNorm _)
    _ = C₁ * eLpNorm v p' μ := rfl
    _ ≤ C₁ * C * eLpNorm (fderiv ℝ v) p μ := by rw [mul_assoc]; gcongr
    _ ≤ C₁ * C * (C₂ * eLpNorm (fderiv ℝ u) p μ) := by
      gcongr; exact eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul (Eventually.of_forall h4v) p
    _ = SNormLESNormFDerivOfEqConst F μ p * eLpNorm (fderiv ℝ u) p μ := by
      simp_rw [C₂, C₁, C, e, SNormLESNormFDerivOfEqConst]
      push_cast
      simp_rw [mul_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
this : μ (⋃ n, S n) ≤ ⨆ n, μ (S n)
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
by calc
    μ (s ∩ t) + μ (s \ t) = μ (s ∩ t) + μ (⋃ n, S n) := by rw [iUnion_S]
    _ ≤ μ (s ∩ t) + ⨆ n, μ (S n) := by gcongr
    _ = ⨆ n, μ (s ∩ t) + μ (S n) := ENNReal.add_iSup ..
    _ ≤ μ s := iSup_le hSs

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝¹⁴ : RCLike 𝕜
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : InnerProductSpace 𝕜 G
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : InnerProductSpace 𝕜 H
inst✝⁵ : CompleteSpace E
inst✝⁴ : CompleteSpace G
inst✝³ : CompleteSpace (E ⊗[𝕜] G)
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace (F ⊗[𝕜] H)
f : E →L[𝕜] F
g : G →L[𝕜] H
⊢ ContinuousLinearMap.adjoint (mapL f g) = mapL (ContinuousLinearMap.adjoint f) (ContinuousLinearMap.adjoint g)

Tactic:
apply ContinuousLinearMap.coe_inj.mp <| ext' ?_
  simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (f '' ⋃ i ∈ u, s ∩ t i) ≤ dimH (⋃ i ∈ u, s ∩ t i) / ↑r

Tactic:
image_iUnion₂,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (⋃ i ∈ u, f '' (s ∩ t i)) ≤ dimH (⋃ i ∈ u, s ∩ t i) / ↑r
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
⊢ finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1

Tactic:
rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]

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

Goal state before:
pp: case neg
𝕜 : 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
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : ¬f.ker = ⊥
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
· have h' : (c • f).ker ≠ ⊥ := by simpa [f.ker_smul _ hc] using h
    simp [normDet_eq_zero_iff_ker_ne_bot.mpr h, normDet_eq_zero_iff_ker_ne_bot.mpr h']

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
⊢ dimH (range f) = dimH (f '' univ)

Tactic:
by rw [image_univ]

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
s : X →₀ V →L[𝕜] V
⊢ IsSelfAdjoint ((s.sum fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) - 0)

pp: case refine_2
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
s : X →₀ V →L[𝕜] V
v : V
⊢ 0 ≤ ⟪((s.sum fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) - 0) v, v⟫_𝕜

Tactic:
· rw [IsSelfAdjoint, sub_zero, star_finsuppSum, Finsupp.sum_comm]
    simp [← mul_assoc, (isHermitian_kernel H).apply]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
s : X →₀ V →L[𝕜] V
v : V
⊢ 0 ≤ ⟪((s.sum fun i xi ↦ s.sum fun j xj ↦ star xi * kernel H i j * xj) - 0) v, v⟫_𝕜
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)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.symm y)

Tactic:
by
  have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
    ext i
    fin_cases i <;> rfl
  simp [areaForm_to_volumeForm, volumeForm_map, this]

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

Goal state before:
pp: case e'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ o = (map (Fin 2) φ.toLinearEquiv) o

pp: case e'_3.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ x = φ.symm (φ x)

pp: case e'_3.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ y = φ.symm (φ y)

Tactic:
· symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

Goal state after:
case e'_3.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ x = φ.symm (φ x)

case e'_3.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ y = φ.symm (φ y)
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)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) y = -⟪o.rightAngleRotation x, o.rightAngleRotation y⟫

Tactic:
o.inner_rightAngleRotation_right,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) y = - -(o.areaForm (o.rightAngleRotation x)) y
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ o = (map (Fin 2) φ.toLinearEquiv) o

Tactic:
· symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

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

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)

Tactic:
let invPair_symm := invPair.symm

Goal state after:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
invPair_symm : RingHomInvPair (↑σ_equiv.symm) σ₂₃ := RingHomInvPair.symm σ₂₃ ↑σ_equiv.symm
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
invPair_symm : RingHomInvPair (↑σ_equiv.symm) σ₂₃ := RingHomInvPair.symm σ₂₃ ↑σ_equiv.symm
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)

Tactic:
enter [

Goal state after:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
invPair_symm : RingHomInvPair (↑σ_equiv.symm) σ₂₃ := RingHomInvPair.symm σ₂₃ ↑σ_equiv.symm
σ_li : 𝕜₂ ≃ₛₗᵢ[σ₂₃] 𝕜₃ :=
  let __LinearEquiv := LinearEquiv.ofBijective σ₂₃.toSemilinearMap σ_bij;
  { toLinearEquiv := __LinearEquiv, norm_map' := ⋯ }
| Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ x ∈ Finset.range n, (-1 * z) ^ x

Tactic:
neg_one_mul,

Goal state after:
case e'_9
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ x ∈ Finset.range n, (-z) ^ x
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : ∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
obtain ⟨ε, hε, hε'⟩ := hd'

Goal state after:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
⊢ ‖z - 0‖ < 1 → ‖z - 0‖ < 1 / 2 → ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖

Tactic:
hz1

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
⊢ ‖z - 0‖ < 1 / 2 → ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
⊢ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi 0) volume

Tactic:
have : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1 := by
    rw [union_assoc, Ioc_union_Ioi (le_max_right _ _),
      Ioc_union_Ioi ((min_le_left _ _).trans (le_max_right _ _)), min_eq_left (lt_min hc2 hc1).le]

Goal state after:
a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Tactic:
enter [

Goal state after:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
| Tendsto (fun x ↦ ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)

Tactic:
enter [

Goal state after:
z : ℂ
hz : ‖z‖ < 1
| Tendsto (fun x ↦ ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-a)
⊢ (fun t ↦ log t • f t) =O[𝓝[>] 0] fun x ↦ x ^ (-b)

Tactic:
have : log =o[𝓝[>] 0] fun t : ℝ => t ^ (a - b) := by
    refine ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto
          tendsto_inv_nhdsGT_zero).congr'
      (.of_forall fun t => ?_)
      (eventually_mem_nhdsWithin.mono fun t ht => ?_)
    · simp
    · simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
  refine (this.isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
      (eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ?_))
  simp_rw [smul_eq_mul, ← rpow_add ht]
  congr 1
  abel

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
| HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z))

Tactic:
enter [

Goal state after:
z : ℂ
hz : ‖z‖ < 1
| HasSum (fun n ↦ z ^ n / ↑n) (-log (1 - z))