mathlib-initiative/mathlib-tactics huggingface dataset:
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 R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
(Q.prop.commute R.prop).eq,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * ↑R * ↑Pᶜ
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑R * ↑Q * ↑Pᶜ) = ↑P + ↑R * ↑Q * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) := (⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker
G' : Submodule 𝕜 F := (lift f.toMultilinearMap).range
e : ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) ≃ₗ[𝕜] ↥(lift f.toMultilinearMap).range :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ (lift f.toMultilinearMap).ker) := f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
⊢ ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x

Tactic:
induction x using PiTensorProduct.induction_on with
    | smul_tprod =>
      simp only [lift_symm, map_smul, lift.tprod, ContinuousMultilinearMap.coe_coe,
      MultilinearMap.coe_mkContinuous, LinearMap.compMultilinearMap_apply, LinearMap.coe_comp,
      LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.apply_symm_apply, SetLike.val_smul,
      LinearMap.codRestrict_apply, f', f'₀]
    | add _ _ hx hy => simp only [map_add, Submodule.coe_add, hx, hy]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
⊢ adjoint ↑y ∘SL ↑y * ↑y.symm ∘SL adjoint ↑y.symm = 1 ∧ ↑y.symm ∘SL adjoint ↑y.symm * adjoint ↑y ∘SL ↑y = 1

Tactic:
by
      simp [mul_def, ← comp_assoc, comp_assoc _ _ (adjoint y.toContinuousLinearMap),
        ← adjoint_comp, one_def, comp_assoc _ y.toContinuousLinearMap]

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Tactic:
rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ∞
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n ↦ (MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] ⟨x, hxs⟩) y ≤
      edist ⟨x, hxs⟩ (MapsTo.restrict f s s hsf ⟨x, hxs⟩) * ↑K ^ n / (1 - ↑K)
⊢ ∃ y ∈ s,
    IsFixedPt f y ∧
      Tendsto (fun n ↦ f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ β⁻¹ * β = 1

Tactic:
refine inv_mul_cancel₀ ?_

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this : IsUnit (adjoint ↑y ∘SL ↑y)
hα_re : α = ↑(RCLike.re α)
hα_ne_zero : α ≠ 0
hα_nonneg : 0 ≤ α
hα_pos : 0 < RCLike.re α
h_comp_adjoint : ↑y ∘SL adjoint ↑y = α • ContinuousLinearMap.id 𝕜 W
β : 𝕜 := ↑(RCLike.re α ^ (-(1 / 2)))
hβ : β * β = α⁻¹
U : V ≃ₗᵢ[𝕜] W := auxIsometry y hα_ne_zero hβ ⋯ h_comp_adjoint ⋯
⊢ β ≠ 0
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ∫ (τ : ℝ) in uIoc ↑t₀ ↑t, ↑K ^ (n + 1) * |τ - ↑t₀| ^ n / ↑n ! * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
apply le_of_abs_le

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ |∫ (τ : ℝ) in uIoc ↑t₀ ↑t, ↑K ^ (n + 1) * |τ - ↑t₀| ^ n / ↑n ! * dist α β| ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
t : ↑(Icc tmin tmax)
⊢ dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β

Tactic:
induction n generalizing t with
  | zero => simpa using!
      ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _
  | succ n hn =>
    rw [iterate_succ_apply', iterate_succ_apply', dist_eq_norm, next_apply,
      next_apply, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      ← intervalIntegral.integral_sub (intervalIntegrable_comp_compProj hf _ t)
        (intervalIntegrable_comp_compProj hf _ t)]
    calc
      _ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β := by
        rw [intervalIntegral.norm_intervalIntegral_eq]
        apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
        apply ae_restrict_mem measurableSet_Ioc |>.mono
        intro t' ht'
        -- Can `grind` do this in the future?
        have ht' : t' ∈ Icc tmin tmax :=
          subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
        rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
        exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
      _ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1) ! * dist α β := by
        apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]

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

Goal state before:
pp: p : ℂ[X]
this :
  ∑' (i : ℤ), ‖fourierCoeff (⇑(toAddCircle p)) i‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1

Tactic:
fourierCoeff_toAddCircle

Goal state after:
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atTop

Tactic:
have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.false
  rw [← natDegree_lt_natDegree_iff hQ] at hdeg
  refine (isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_
  apply Tendsto.const_mul_atTop hpos
  apply tendsto_zpow_atTop_atTop
  lia

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case neg
R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
h_supp : ¬p.support.Nonempty
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
· simp_all

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
x✝ : ℝ
ht : x✝ ∈ Icc tmin tmax
⊢ ContDiffWithinAt ℝ (↑n) α (Icc tmin tmax) x✝

Tactic:
rw [Icc_eq_empty (not_le.mpr h)] at ht

Goal state after:
case neg.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
tmin tmax : ℝ
n : ℕ∞
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
hmem : MapsTo α (Icc tmin tmax) u
h : tmax < tmin
x✝ : ℝ
ht : x✝ ∈ ∅
⊢ ContDiffWithinAt ℝ (↑n) α (Icc tmin tmax) x✝
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
by
  rcases eq_or_ne (p * q) 0 with hpq | hpq
  · simp [hpq, hc, gaussNorm_nonneg, mul_nonneg]
  have h_supp_p : p.support.Nonempty := support_nonempty.mpr <| left_ne_zero_of_mul hpq
  have h_supp_q : q.support.Nonempty := support_nonempty.mpr <| right_ne_zero_of_mul hpq
  simp only [gaussNorm, support_nonempty, ne_eq, hpq, not_false_eq_true, ↓reduceDIte, h_supp_p,
    h_supp_q, sup'_le_iff, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk]
  intro i _
  obtain ⟨j, _, _⟩ := IsNonarchimedean.finset_image_add_of_nonempty hna _ nonempty_range_add_one
  calc
  v (∑ j ∈ range (i + 1), p.coeff j * q.coeff (i - j)) * c ^ i
  _ ≤ v (p.coeff j * q.coeff (i - j)) * c ^ i := by gcongr
  _ = (v (p.coeff j) * c ^ j) * (v (q.coeff (i - j)) * c ^ (i - j)) := by
      have : c ^ j * c ^ (i - j) = c ^ i := by simp_all [← pow_add]
      grind
  _ ≤ (p.support.sup' _ fun i ↦ v (p.coeff i) * c ^ i)
    * q.support.sup' _ fun i ↦ v (q.coeff i) * c ^ i := by
      have hp_le := p.le_gaussNorm v hc j
      have hq_le := q.le_gaussNorm v hc (i - j)
      have := p.gaussNorm_nonneg v hc
      simp_all only [gaussNorm, ↓reduceDIte]
      gcongr

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E → E
t₀ ε : ℝ
hε : 0 < ε
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a r L K
a' r' : ℝ≥0
ha : a' ≤ a
hr : r' < a'
⊢ ∃ ε', ∃ (hε' : 0 < ε'), IsPicardLindelof f ⟨t₀, ⋯⟩ x₀ a' r' L K

Tactic:
by
  have ha'r' : (0 : ℝ) < a' - r' := by simp only [sub_pos, NNReal.coe_lt_coe, hr]
  let ε' := min ε ((a' - r') / (L + 1))
  have hε'pos : 0 < ε' := lt_min hε (by positivity)
  have hε'_le : ε' ≤ ε := min_le_left _ _
  refine ⟨ε', hε'pos, hf.shrink ⟨t₀, by simp [le_of_lt hε'pos]⟩ (by linarith) (by linarith) ha ?_⟩
  simp only [add_sub_cancel_left, sub_sub_cancel, max_self]
  calc (L : ℝ) * ε'
    _ ≤ L * ((a' - r') / (L + 1)) := by gcongr; exact min_le_right _ _
    _ = L / (L + 1) * (a' - r') := by ring
    _ ≤ 1 * (a' - r') := by gcongr; rw [div_le_one (by positivity : (0 : ℝ) < L + 1)]; linarith
    _ = a' - r' := one_mul _

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case cons
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ ∃ b ∈ Finset.cons j s hj, g (∑ i ∈ Finset.cons j s hj, f i) ≤ g (f b)

Tactic:
simp only [Finset.sum_cons, Finset.mem_cons, exists_eq_or_imp]

Goal state after:
case cons
α : Type u_5
S : Type u_6
inst✝¹ : LinearOrder S
inst✝ : AddCommMonoid α
g : α → S
ι : Type u_7
s✝ : Finset ι
f : ι → α
na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)
j : ι
s : Finset ι
hj : j ∉ s
hs✝ : s.Nonempty
IH : ∃ b ∈ s, g (∑ i ∈ s, f i) ≤ g (f b)
⊢ g (f j + ∑ i ∈ s, f i) ≤ g (f j) ∨ ∃ a ∈ s, g (f j + ∑ i ∈ s, f i) ≤ g (f a)
Module: Mathlib.Order.Filter.FilterProduct

Goal state before:
pp: α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(min x y) = min ↑x ↑y

Tactic:
rw [min_def, map₂_const]

Goal state after:
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ |((↑b ^ n)⁻¹ * ofDigits fun i ↦ x (i + n)) - (↑b ^ n)⁻¹ * ofDigits fun i ↦ y (i + n)| ≤ (↑b ^ n)⁻¹

Tactic:
← mul_sub,

Goal state after:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i
⊢ |(↑b ^ n)⁻¹ * ((ofDigits fun i ↦ x (i + n)) - ofDigits fun i ↦ y (i + n))| ≤ (↑b ^ n)⁻¹
Module: Mathlib.Analysis.Real.Pi.Bounds

Goal state before:
pp: n : ℕ
a : ℝ
h : 2 - ((a - 1 / 4 ^ n) / 2 ^ (n + 1)) ^ 2 ≤ (↑0 / ↑1).sqrtTwoAddSeries n
h₂ : 1 / 4 ^ n ≤ a
⊢ π < a

Tactic:
refine lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_
  rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]
  · rwa [Nat.cast_zero, zero_div] at h
  · exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _)
  · exact pow_pos zero_lt_two _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case a
x : ℝ≥0
⊢ min x x ≤ x.agm x

Tactic:
exact min_le_agm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
have : log p < log (1 - p) := by
      rw [← log_neg_eq_log]
      exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)

Goal state after:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
this : log p < log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z ↦ cexp (↑b * z)) =o[l] fun z ↦ z ^ a

Tactic:
by simpa using hl.isLittleO_cpow_mul_exp hb 0 a

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictMonoOn (qaryEntropy q) (Icc 0 (1 - 1 / ↑q))

Tactic:
intro p1

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
⊢ p1 ∈ Icc 0 (1 - 1 / ↑q) → ∀ ⦃b : ℝ⦄, b ∈ Icc 0 (1 - 1 / ↑q) → p1 < b → qaryEntropy q p1 < qaryEntropy q b
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case e'_4
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
qpos : 0 < ↑q
⊢ ↑q - 1 = ↑q * (1 - (↑q)⁻¹)

Tactic:
simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
⊢ StrictAntiOn (qaryEntropy q) (Icc (1 - 1 / ↑q) 1)

Tactic:
intro p1

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
⊢ p1 ∈ Icc (1 - 1 / ↑q) 1 → ∀ ⦃b : ℝ⦄, b ∈ Icc (1 - 1 / ↑q) 1 → p1 < b → qaryEntropy q b < qaryEntropy q p1
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
⊢ False

Tactic:
obtain ⟨z, hz⟩ : ∃ z : ℤ, (sinPoly n).eval₂ (Int.castRingHom ℝ) (a / b) * b ^ (2 * n + 1) = z :=
    is_integer a b ((sinPoly_natDegree_le _).trans (by lia))

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : ¬IsStrictlyPositive a
⊢ Tendsto (fun i ↦ if a ∈ {b | IsStrictlyPositive b} then cfc (fun x ↦ i⁻¹ * (x ^ i - 1)) a else 0) (𝓝[>] 0)
    (𝓝 (if a ∈ {b | IsStrictlyPositive b} then log a else 0))

Tactic:
· simp_all

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

Goal state before:
pp: case ha
s : ℂ
hs : 0 < s.re
⊢ ↑π ^ (-s / 2) ≠ 0

pp: case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0

Tactic:
· simp [pi_ne_zero]

Goal state after:
case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / (2 * t) ≤ 1 / (t + 1)

Tactic:
one_div_le_one_div (by positivity) (by positivity)

Goal state after:
case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t + 1 ≤ 2 * t
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ StrictMono eulerMascheroniSeq

Tactic:
by
  refine strictMono_nat_of_lt_succ (fun n ↦ ?_)
  rw [eulerMascheroniSeq, eulerMascheroniSeq, ← sub_pos, sub_sub_sub_comm,
    harmonic_succ, add_comm, Rat.cast_add, add_sub_cancel_right,
    ← log_div (by positivity) (by positivity), add_div, Nat.cast_add_one,
    Nat.cast_add_one, div_self (by positivity), sub_pos, one_div, Rat.cast_inv, Rat.cast_add,
    Rat.cast_one, Rat.cast_natCast]
  refine (log_lt_sub_one_of_pos ?_ (ne_of_gt <| lt_add_of_pos_right _ ?_)).trans_le (le_of_eq ?_)
  · positivity
  · positivity
  · simp only [add_sub_cancel_left]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ ↑(harmonic (n + 1)) - log ↑(n + 1) < ↑(harmonic n) - log ↑n

Tactic:
rw [← sub_pos, sub_sub_sub_comm,
    harmonic_succ, Rat.cast_add, ← sub_sub, sub_self, zero_sub, sub_eq_add_neg, neg_sub,
    ← sub_eq_neg_add, sub_pos, ← log_div (by positivity) (by positivity), ← neg_lt_neg_iff,
    ← log_inv]

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ log (↑(n + 1) / ↑n)⁻¹ < -↑(↑(n + 1))⁻¹
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n

Tactic:
simp_rw [eulerMascheroniSeq', hn, if_false]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hg2
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ici 0) volume

Tactic:
exact Integrable.mul_const (integrableOn_rpowIntegrand₀₁_Ici hp zero_le_one) _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x

Tactic:
simp [hx_zero, Real.zero_rpow (by linarith)]

Goal state after: