mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case refine_1
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
j : ℕ
⊢ ediam (u j) ≤ ε

pp: case refine_2
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
⊢ ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c

Tactic:
· rw [ediam_iUnion_mem_option]
    exact iSup₂_le fun _ _ => (htn _).trans hrn.le

Goal state after:
case refine_2
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
⊢ ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ f.normDet ^ 2 = (∏ i ∈ Finset.range (finrank 𝕜 U), f.singularValues i) ^ 2

Tactic:
← RCLike.ofReal_inj (K := 𝕜),

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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ ↑(f.normDet ^ 2) = ↑((∏ i ∈ Finset.range (finrank 𝕜 U), f.singularValues i) ^ 2)
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑Sᗮ.mulI).carrier ↔ x ∈ (↑S.symplComp).carrier

Tactic:
← mem_iff,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ Sᗮ.mulI ↔ x ∈ (↑S.symplComp).carrier
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ Sᗮ.mulI ↔ x ∈ (↑S.symplComp).carrier

Tactic:
← mem_iff,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ Sᗮ.mulI ↔ x ∈ S.symplComp
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ Sᗮ.mulI = S.symplComp

Tactic:
ext x
  rw [← mem_iff, ← mem_iff, mem_symplComp_iff, mem_mapEquiv_iff, scalarSMulCLE_symm_apply,
    Units.inv_mk, Units.smul_mk_apply]
  simp [inner_real_eq_re_inner]

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

Goal state before:
pp: H : Type u_1
inst✝¹ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : ClosedSubmodule ℝ H
⊢ S.symplComp.symplComp = S

Tactic:
by simp [symplComp]

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

Goal state before:
pp: case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s

Tactic:
have hKd0 : (K : ℝ≥0∞) ^ d ≠ 0 := by simp [h0]

Goal state after:
case inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
⊢ μH[d] (f ⁻¹' s) ≤ ↑K ^ d * μH[d] s
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
i : Fin (Nat.succ 1)
⊢ ![x, y] i = (![y, x] ∘ ⇑(Equiv.swap 0 1)) i

Tactic:
fin_cases i

Goal state after:
case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩) = (![y, x] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩) = (![y, x] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩)
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
h : ⟪x, y⟫ = 0
i j : Fin 2
hij : i ≠ j
⊢ ⟪![x, y] i, ![x, y] j⟫ = 0

Tactic:
fin_cases i

Goal state after:
case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, y] j⟫ = 0

case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, y] j⟫ = 0
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
i : Fin (Nat.succ 0).succ
⊢ (⇑φ.symm ∘ ![x, y]) i = ![φ.symm x, φ.symm y] i

Tactic:
fin_cases i

Goal state after:
case «0»
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
⊢ (⇑φ.symm ∘ ![x, y]) ((fun i ↦ i) ⟨0, ⋯⟩) = ![φ.symm x, φ.symm y] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
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
⊢ (⇑φ.symm ∘ ![x, y]) ((fun i ↦ i) ⟨1, ⋯⟩) = ![φ.symm x, φ.symm y] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.LocallyConvex.StrongTopology

Goal state before:
pp: R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
⊢ LocallyConvexSpace R (E →SLᵤ[σ, 𝔖] F)

Tactic:
apply LocallyConvexSpace.ofBasisZero _ _ _ _
    (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
      (LocallyConvexSpace.convex_basis_zero R F)) _

Goal state after:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
⊢ ∀ (i : Set E × Set F), i.1 ∈ 𝔖 ∧ i.2 ∈ 𝓝 0 ∧ Convex R i.2 → Convex R {f | ∀ x ∈ i.1, f x ∈ id i.2}
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 : E
⊢ o.rightAngleRotation (o.rightAngleRotation x) = -x

Tactic:
by
  rw [rightAngleRotation]
  exact o.rightAngleRotationAux₁_rightAngleRotationAux₁ x

Goal state after:
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 : E
hx : x ≠ 0
i : Fin 2
⊢ ![x, o.rightAngleRotation x] i ≠ 0

Tactic:
fin_cases i

Goal state after:
case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0

case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
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 : E
hx : x ≠ 0
i j : Fin 2
hij : i ≠ j
⊢ ⟪![x, o.rightAngleRotation x] i, ![x, o.rightAngleRotation x] j⟫ = 0

Tactic:
fin_cases i

Goal state after:
case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, o.rightAngleRotation x] j⟫ = 0

case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, o.rightAngleRotation x] j⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

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

Tactic:
fin_cases i

Goal state after:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim.2771185604._hygCtx._hyg.87.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨0, ⋯⟩))

case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim.2771185604._hygCtx._hyg.87.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

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

Tactic:
fin_cases i

Goal state after:
case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim.1235492232._hygCtx._hyg.87.«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨0, ⋯⟩))

case neg.«_@».Mathlib.Analysis.InnerProductSpace.TwoDim.1235492232._hygCtx._hyg.87.«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ (⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    (‖a‖ ^ 2 • o.areaForm x) ((o.basisRightAngleRotation a ha) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
⊢ ⇑(toWeakSpace 𝕜 E) '' (closedConvexHull 𝕜) s = (closedConvexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)

Tactic:
closedConvexHull_eq_closure_convexHull (𝕜 := 𝕜),

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
⊢ ⇑(toWeakSpace 𝕜 E) '' closure ((convexHull 𝕜) s) = (closedConvexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ (2 * π)⁻¹ • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)

Tactic:
← abs_of_pos (show 0 < (2 * π)⁻¹ by simp [pi_pos])

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
⊢ mellinInv σ (mellin f) x = f x

Tactic:
replace hf : Integrable g := by
    rw [MellinConvergent, ← rexp_neg_image_aux, integrableOn_image_iff_integrableOn_abs_deriv_smul
      MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux] at hf
    replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by
      simpa [rexp_cexp_aux] using hf
    norm_cast at hf

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
⊢ mellinInv σ (mellin f) x = f x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
hsre : -↑n < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ Gamma s

Tactic:
induction n generalizing s with

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

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℝ Gamma s

Tactic:
refine (Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt
  simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
  exact hs

Goal state after:
Module: Mathlib.Analysis.MellinTransform

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

Tactic:
by
  refine
    ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).isBigO.smul hf).congr'
      (Eventually.of_forall fun t => by rfl)
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun t ht => ?_))
  simp only
  rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]

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

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

Tactic:
by
  refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_
  · refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_
    intro n
    simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]
    rcases n.eq_zero_or_pos with rfl | hn
    · simp
    conv => enter [2]; rw [← div_one (‖z‖ ^ n)]
    gcongr
    norm_cast
  · rw [← tendsto_sub_nhds_zero_iff]
    conv => enter [1, x]; rw [← div_one (_ - _), ← logTaylor]
    rw [← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim]
    refine IsLittleO.trans_isBigO ?_ <| isBigO_const_one ℂ (1 : ℝ) atTop
    have H : (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] (fun n : ℕ ↦ ‖z‖ ^ n) := by
      have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
      exact (isBigOWith_of_le' atTop this).isBigO
    refine IsBigO.trans_isLittleO H ?_
    convert! isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz
    exact (one_pow _).symm

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

Goal state before:
pp: case e'_4.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - ↑(-x) = ↑(x + 1)

Tactic:
push_cast; ring

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

Goal state before:
pp: case e'_4.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) = 1 - ↑(x + 1)

Tactic:
push_cast; ring

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

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ s + t - 1 = 1 + (s - 1) + (t - 1)

Tactic:
by abel

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3.e'_5.e'_5
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = ↑(2 * n + 2) - 1

Tactic:
push_cast; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3.e'_5.e'_6
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 2)

Tactic:
push_cast; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑(π / 2) = ↑π * z

Tactic:
push_cast; ring

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f x ≤ f 1 + x * log (↑n + 1) - x * log ↑n + logGammaSeq x n

Tactic:
logGammaSeq,

Goal state after:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f x ≤ f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + ↑m))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)

Tactic:
rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]

Goal state after:
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
v : V
p : P
⊢ ⨆ i, map (fun x ↦ (x +ᵥ i) +ᵥ p) (atTop • 𝓝 v) = ⨆ p, map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)

Tactic:
refine (Equiv.vaddConst p).iSup_congr fun _ => ?_

Goal state after:
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
v : V
p : P
x✝ : V
⊢ map (fun x ↦ x +ᵥ (Equiv.vaddConst p) x✝) (atTop • 𝓝 v) = map (fun x ↦ (x +ᵥ x✝) +ᵥ p) (atTop • 𝓝 v)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : s ≠ 0
⊢ s + 1 - 1 = s - 1 + 1

Tactic:
by abel

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), Meromorphic (F i)
h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[codiscrete 𝕜] fun z ↦ ∑ᶠ (i : ι), d i • logDeriv (F i) z

Tactic:
apply MeromorphicOn.logDeriv_finprod_zpow_eventuallyEq hd (fun i ↦ meromorphicOn_univ.mpr (h i))

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), Meromorphic (F i)
h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤
⊢ ∀ (i : ι), ∀ x ∈ univ, meromorphicOrderAt (F i) x ≠ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ 1 - 2 * s = -(2 * s - 1)

Tactic:
by abel

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

Goal state before:
pp: s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma ↑(1 - s) = ↑π / Complex.sin (↑π * ↑s)

Tactic:
Complex.ofReal_sub,

Goal state after:
s : ℝ
⊢ Complex.Gamma ↑s * Complex.Gamma (↑1 - ↑s) = ↑π / Complex.sin (↑π * ↑s)