mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
have hrank : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction = 1 := by
    rw [AffineSubspace.direction_mk']
    apply finrank_span_singleton hv
  have hrank' : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1 := by
    rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]
  let f : ℝ ≃L[ℝ] (AffineSubspace.mk' p (ℝ ∙ v)).direction :=
    (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) ((AffineSubspace.mk' p (ℝ ∙ v)).direction) (by simp))
  have hf : MeasurableEmbedding f := f.toHomeomorph.measurableEmbedding
  let p' : AffineSubspace.mk' p (ℝ ∙ v) := ⟨p, by simp⟩
  let g : ℝ → AffineSubspace.mk' p (ℝ ∙ v) := IsometryEquiv.vaddConst p' ∘ f
  have hadd : MeasurableEmbedding (IsometryEquiv.vaddConst p') :=
    (IsometryEquiv.vaddConst p').toHomeomorph.measurableEmbedding
  have hg : MeasurableEmbedding g := hadd.comp hf
  have hm : μHE[finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction] =
      ‖v‖ₑ • (volume : Measure ℝ).map g := by
    unfold g
    rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
      ← Measure.map_smul]
    congr
    let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩
    suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']
    exact volume_eq_of_finrank_eq_one hrank (by simpa [v'] using hv)
  have hx (x : ℝ) : x • v +ᵥ p = g x := by rfl
  simp_rw [(AffineSubspace.mk' p (ℝ ∙ v)).euclideanHausdorffMeasure_eq_lintegral ht, hx,
    hm, lintegral_smul_measure, hg.lintegral_map, smul_eq_mul, hrank', AffineSubspace.direction_mk']

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

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊔ T).mulI = S.mulI ⊔ T.mulI

Tactic:
mulI,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (mapEquiv (scalarSMulCLE H UnitI)) (S ⊔ T) = S.mulI ⊔ T.mulI
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (S ⊓ T).mulI = S.mulI ⊓ T.mulI

Tactic:
mulI,

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S T : ClosedSubmodule ℝ H
⊢ (mapEquiv (scalarSMulCLE H UnitI)) (S ⊓ T) = S.mulI ⊓ T.mulI
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
⊢ ⨅ t,
      ⨅ (_ : f '' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑C ^ d * ediam (i_1 i) ^ (↑r * d)

Tactic:
refine le_iSup₂_of_le δ δ0 <| iInf₂_mono' fun t hst ↦
      ⟨fun n => f '' (t n ∩ s), ?_, iInf_mono' fun htδ ↦
        ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩

Goal state after:
case inr.refine_1
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
⊢ f '' s ⊆ ⋃ n, (fun n ↦ f '' (t n ∩ s)) n

case inr.refine_2
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun n ↦ f '' (t n ∩ s)) n).Nonempty), ediam ((fun n ↦ f '' (t n ∩ s)) n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑C ^ d * ediam (t i) ^ (↑r * d)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case h₁
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
n : ℕ
hft : (t n ∩ s).Nonempty
⊢ ediam (f '' (t n ∩ s)) ≤ ↑C * ediam (t n) ^ ↑r

Tactic:
exact h.ediam_image_inter_le _

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

Goal state before:
pp: case inl.inl
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
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
hs : f ⁻¹' s = ∅
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

Tactic:
simp only [hs, measure_empty, zero_le]

Goal state after:
Module: Mathlib.Analysis.Matrix.LDL

Goal state before:
pp: case neg
𝕜 : 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
i j : n
hij : ¬i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j

Tactic:
simp only [LDL.diag, hij, diagonal_apply_ne, Ne, not_false_iff, mul_mul_apply]
    rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
      (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm,
      mulVec_transpose, EuclideanSpace.inner_toLp_toLp, ← RCLike.star_def, ←
      star_dotProduct_star, star_star]
    rfl

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
g : F →SWOT[σ₂₃] G
f : E →SWOT[σ₁₂] F
x : E
⊢ (g.comp f) x = g (f x)

Tactic:
simp [comp]

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

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
E : Type u_9
F : Type u_10
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
f : E →SWOT[σ₁₂] F
⊢ (ContinuousLinearMapWOT.id 𝕜₂ F).comp f = f

Tactic:
simp [comp]

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

Goal state before:
pp: 𝕜₂ : Type u_6
𝕜₃ : Type u_7
F : Type u_10
G : Type u_11
inst✝⁷ : NormedField 𝕜₂
inst✝⁶ : NormedField 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜₂ F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜₃ G
g : F →SWOT[σ₂₃] G
⊢ g.comp (ContinuousLinearMapWOT.id 𝕜₂ F) = g

Tactic:
simp [comp]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0

Tactic:
right
    simpa using h

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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
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✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (x y : F →SWOT[σ₂₃] G), (x + y).comp f = x.comp f + y.comp f

Tactic:
simp [comp]

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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
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✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (m : 𝕜₃) (x : F →SWOT[σ₂₃] G), (m • x).comp f = (RingHom.id 𝕜₃) m • x.comp f

Tactic:
simp [comp]

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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²⁵ : NormedField 𝕜₁
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝²¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁰ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
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✝⁸ : AddCommGroup H
inst✝⁷ : TopologicalSpace H
inst✝⁶ : Module 𝕜₄ H
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (x y : E →SWOT[σ₁₂] F), g.comp (x + y) = g.comp x + g.comp y

Tactic:
simp [comp]

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✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²⁵ : NormedField 𝕜₁
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝²¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁰ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
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✝⁸ : AddCommGroup H
inst✝⁷ : TopologicalSpace H
inst✝⁶ : Module 𝕜₄ H
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (m : 𝕜₂) (x : E →SWOT[σ₁₂] F), g.comp (m • x) = σ₂₃ m • g.comp x

Tactic:
simp [comp]

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y ↦ ↑(cos y)) (-↑(sin x)) x

Tactic:
simpa using (hasDerivAt_cos x).ofReal_comp

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

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖

Tactic:
apply (norm_log_sub_logTaylor_le n hz1).trans

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1) ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ (↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
        (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos ↑x ^ n - (↑n - 1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        (-Complex.cos (2 * z * ↑x) / (2 * z)))

Tactic:
mul_div,

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ (↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
        (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos ↑x ^ n - (↑n - 1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
          -Complex.cos (2 * z * ↑x) /
        (2 * z))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
hm : ∀ {x : ℝ}, 0 < x → ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
x : ℝ
hx : 0 < x
⊢ ↑(m + 1) < x → x ≤ ↑(m + 1) + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
intro hy hy'
    rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
    rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
    specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
    -- now massage gauss_product n (x - 1) into gauss_product (n - 1) x
    have :
      ∀ᶠ n : ℕ in atTop,
        logGammaSeq (x - 1) n =
          logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) := by
      refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
      have := logGammaSeq_add_one (x - 1) (n - 1)
      rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
      rw [this]
      ring
    replace hm :=
      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
        (tendsto_add_atTop_nat 1)
    have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]
    rw [this] at hm
    convert! hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
    · ring
    · have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
      rw [sub_add_cancel] at this
      rw [this]
      ring

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
⊢ ∑ j ∈ insert (↑i) (fs i), wx i j = ∑ j ∈ fs i, w i j

Tactic:
wx

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
i : ↑s
⊢ ∑ x ∈ insert (↑i) (fs i), (↑(fs i)).indicator (w i) x = ∑ j ∈ fs i, w i j
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
hwx : ∀ (i : ↑s), ∑ j ∈ fsx i, wx i j = 1
i : ↑s
⊢ (Finset.affineCombination k (insert (↑i) (fs i)) p) (wx i) = (Finset.affineCombination k (fs i) p) (w i)

Tactic:
wx

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : ↑s → Finset ι
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
fsx : ↑s → Finset ι := fun i ↦ insert (↑i) (fs i)
hfsx : ∀ (i : ↑s), ↑i ∈ fsx i
wx : ↑s → ι → k := fun i ↦ (↑(fs i)).indicator (w i)
hwx : ∀ (i : ↑s), ∑ j ∈ fsx i, wx i j = 1
i : ↑s
⊢ (Finset.affineCombination k (insert (↑i) (fs i)) p) ((↑(fs i)).indicator (w i)) =
    (Finset.affineCombination k (fs i) p) (w i)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case e'_3.e'_3
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ (Equiv.swap 1 j) i = i

Tactic:
exact Equiv.swap_apply_of_ne_of_ne hi hij

Goal state after:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
· rw [h', mul_left_comm] at h hf
      exact ⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
hw'i0 : w' i = 1
hi1 : c (i + 1) * r (i + 1) = 1
hi1' : c (i + 1) * (1 - r (i + 1)) = 0
⊢ c (i + 1) * (r (i + 1) + (1 - r (i + 1))) = 1 + 0

Tactic:
rw [mul_add, hi1, hi1']

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le : ∀ (m : ℕ), p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))
hfx : 1 < p x
⊢ ∃ b, ∀ (x_1 : ℕ), p (x ^ s (ψ x_1)) ^ (1 / ↑(ψ x_1)) ≤ b

Tactic:
use p x

Goal state after:
case h
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
h_le : ∀ (m : ℕ), p (x ^ s (ψ m)) ^ (1 / ↑(ψ m)) ≤ p x ^ (↑(s (ψ m)) / ↑(ψ m))
hfx : 1 < p x
⊢ ∀ (x_1 : ℕ), p (x ^ s (ψ x_1)) ^ (1 / ↑(ψ x_1)) ≤ p x