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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ (fun x ↦ c + x) x✝¹ ≤ (fun x ↦ c + x) x✝

Tactic:
dsimp

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ c + x✝¹ ≤ c + x✝
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddRightMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ (fun x ↦ x + c) x✝¹ ≤ (fun x ↦ x + c) x✝

Tactic:
dsimp

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddRightMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ x✝¹ + c ≤ x✝ + c
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ (fun x ↦ c + x) x✝¹ ≤ (fun x ↦ c + x) x✝

Tactic:
dsimp

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ c + x✝¹ ≤ c + x✝
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddRightMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ (fun x ↦ x + c) x✝¹ ≤ (fun x ↦ x + c) x✝

Tactic:
dsimp

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
F : Filter ι
inst✝³ : F.NeBot
inst✝² : Add R
inst✝¹ : ContinuousAdd R
inst✝ : AddRightMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) F f
x✝¹ x✝ : R
h : x✝¹ ≤ x✝
⊢ x✝¹ + c ≤ x✝ + c
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
⊢ (∑ i < f.natDegree, C (c i) * X ^ i).natDegree ≤ f.natDegree - 1

Tactic:
apply Polynomial.natDegree_sum_le_of_forall_le

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
⊢ ∀ i ∈ Finset.Iio f.natDegree, (C (c i) * X ^ i).natDegree ≤ f.natDegree - 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

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

Tactic:
simp only [seminormFromBounded', mul_assoc, hx, mul_div_assoc,
    Real.mul_iSup_of_nonneg (f_nonneg _)]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
n : ℕ
hn : 1 ≤ n
⊢ 0 < n

Tactic:
exact succ_le_iff.mp hn

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g✝)) ⋯))) x

Tactic:
dsimp

Goal state after:
V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom f - Hom.hom g✝) ⋯))) x
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

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

Tactic:
have : normedMk x = 0 := by
      rw [h]
      simp only [NormedAddGroupHom.zero_apply]

Goal state after:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = 0
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑' (b : β), (f n b - g b)‖ < ε

Tactic:
← (h_suma.of_norm.sub h_sumg.of_norm).sum_add_tsum_compl (s := T),

Goal state after:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable fun x ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖∑ x ∈ T, (f n x - g x) + ∑' (x : ↑(↑T)ᶜ), (f n ↑x - g ↑x)‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
by
  obtain ⟨r₁, hr₁⟩ := exists_gt (max 0 <| ∏' i, v i)
  rw [max_lt_iff] at hr₁
  have := hv.hasProd.eventually_le_const hr₁.2
  rw [unconditional, eventually_atTop] at this
  exact ⟨r₁, hr₁.1, this⟩

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

Goal state before:
pp: case e'_6
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
inst✝¹ : CompleteSpace R
inst✝ : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
hKe : ¬K = ∅
hCK : CompactSpace ↑K
hne : Nonempty ↑K
f' : ι → C(↑K, R) := fun i ↦ { toFun := K.domRestrict (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable fun i ↦ 1 + f' i
⊢ (fun x ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val = ⇑(∏' (b : ι), (1 + f' b))

Tactic:
· exact funext fun k ↦ ContinuousMap.tprod_apply hM k

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

Goal state before:
pp: case pos
𝕜 : 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✝ : Subsingleton V
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
by_cases! Subsingleton W

Goal state after:
case pos
𝕜 : 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✝¹ : Subsingleton V
h✝ : Subsingleton W
⊢ ∃ U, f = U.conjStarAlgEquiv

case neg
𝕜 : 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✝¹ : Subsingleton V
h✝ : Nontrivial W
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : 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 α
⊢ ∃ U, f = U.conjStarAlgEquiv

Tactic:
have h_comp_adjoint : y.toContinuousLinearMap ∘L adjoint y.toContinuousLinearMap =
      α • ContinuousLinearMap.id 𝕜 _ := by
    ext x
    simpa using congr(y (($hα ∘L y.symm.toContinuousLinearMap) x)).symm

Goal state after:
case neg
𝕜 : 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
⊢ ∃ U, f = U.conjStarAlgEquiv
Module: Mathlib.Topology.MetricSpace.Contracting

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy

Tactic:
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
    <;> try apply efixedPoint_isFixedPt

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : EMetricSpace α
K : ℝ≥0
f : α → α
inst✝ : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasDerivWithinAt (γ ∘ fun x ↦ x * a) ((a • v ∘ fun x ↦ x * a) t ((γ ∘ fun x ↦ x * a) t)) {t | t * a ∈ s} t

Tactic:
simp only [comp_apply, Pi.smul_apply]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
⊢ HasDerivWithinAt (γ ∘ fun x ↦ x * a) (a • v (t * a) (γ (t * a))) {t | t * a ∈ s} t
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ EqOn f g (Icc a b)

Tactic:
by
  rw [← Icc_union_Icc_eq_Icc (le_of_lt ht.1) (le_of_lt ht.2)]
  apply EqOn.union
  · have hss : Ioc a t₀ ⊆ Ioo a b := Ioc_subset_Ioo_right ht.2
    exact ODE_solution_unique_of_mem_Icc_left (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq
  · have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1
    exact ODE_solution_unique_of_mem_Icc_right (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
⊢ f t' = g t'

Tactic:
have hss : Icc t' t₀ ⊆ Ioo a b :=
      fun _ ht'' ↦ ⟨lt_of_lt_of_le ht'.1 ht''.1, lt_of_le_of_lt ht''.2 ht.2⟩

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
hss : Icc t' t₀ ⊆ Ioo a b
⊢ f t' = g t'
Module: Mathlib.Analysis.Polynomial.Basic

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

Tactic:
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)

Goal state after:
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
h : Q = 0
⊢ False

Tactic:
by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.false

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : (coeff n) f ≠ 0
⊢ 0 < v ((coeff n) f) * ∏ i ∈ n.support, c i ^ n i

Tactic:
by
    apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)
    specialize h_eq_zero (f.coeff n)
    grind

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

Goal state before:
pp: p : ℂ[X]
⊢ 1 ≤ (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
by
  grind [Multiset.one_le_prod, Multiset.mem_map]

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

Goal state before:
pp: p : ℂ[X]
⊢ ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

Tactic:
← mul_one ‖_‖,

Goal state after:
p : ℂ[X]
⊢ ‖p.leadingCoeff‖ * 1 ≤ p.mahlerMeasure
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case neg.right
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝¹ : Ring R
inst✝ : DecidableEq σ
f g : MvPowerSeries σ R
hf : HasGaussNorm v c f
hg : HasGaussNorm v c g
hfg : HasGaussNorm v c (f * g)
vNonneg : ∀ (a : R), v a ≥ 0
vZero : v 0 = 0
vNA : IsNonarchimedean v
vMulEq : ∀ (a b : R), v (a * b) = v a * v b
vNeg : ∀ (a : R), v (-a) = v a
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hdom :
  ∃ i j,
    AchievesGaussNorm v c f i ∧
      AchievesGaussNorm v c g j ∧
        ∀ p ∈ Finset.antidiagonal (i + j),
          p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)
hf' : ¬f = 0
hg' : ¬g = 0
hf1 : gaussNorm v c f ≠ 0
hg1 : gaussNorm v c g ≠ 0
⊢ gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g

Tactic:
exact gaussNorm_mul_le v c f g (StrongLT.le hc) vNonneg (by grind) vNA vZero hf hg

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

Goal state before:
pp: p : ℂ[X]
⊢ √(↑p.natDegree + 1) * p.supNorm = √((↑p.natDegree + 1) * p.supNorm ^ 2)

Tactic:
Real.sqrt_mul (by positivity),

Goal state after:
p : ℂ[X]
⊢ √(↑p.natDegree + 1) * p.supNorm = √(↑p.natDegree + 1) * √(p.supNorm ^ 2)
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)) - ofDigits fun i ↦ y (i + n)| ≤ (↑b ^ n)⁻¹

Tactic:
abs_of_nonneg (by positivity)

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 : ℕ
⊢ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by
    rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
    focus
      apply sin_lt
      apply div_pos pi_pos
    all_goals apply pow_pos; norm_num
  refine lt_of_le_of_lt (le_of_eq ?_) this
  rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]; simp

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
⊢ u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)

Tactic:
simp [u₂, v₂, f, ← two_mul]

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

Goal state before:
pp: x y : ℝ≥0
⊢ Tendsto (fun n ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun _ ↦ dist_nonneg) dist_agmSequences_fst_snd
  conv =>
    rw [← zero_mul (dist x y / 2)]
    enter [1, n]
    rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]
  exact (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)).mul_const _

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

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ p < sqrt (p * q)

Tactic:
← mul_self_sqrt p,

Goal state after:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ sqrt p * sqrt p < sqrt (p * q)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log ↑(↑q - 1) + binEntropy p

Tactic:
positivity [binEntropy_pos hp₀ hp₁]

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)

Tactic:
cases n with
    | zero => simp [u₂']
    | succ n => ring!

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

Goal state before:
pp: case a
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)⁻¹
⊢ p < (↑q - 1) * (1 - p)

Tactic:
have qpos : 0 < (q : ℝ) := by positivity

Goal state after:
case a
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
⊢ p < (↑q - 1) * (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
⊢ (↑q - 1) * (1 - p) < p

Tactic:
have qpos : 0 < (q : ℝ) := by positivity

Goal state after:
case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
⊢ (↑q - 1) * (1 - p) < p