mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
⊢ Tendsto
    (fun n ↦ (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n ∂volume)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x ∂volume)
    atTop (𝓝 (f 0))

Tactic:
have c_nonneg : ∀ x : ℝ, x ∈ Icc 0 (π / 2) → 0 ≤ cos x := fun x hx =>
    cos_nonneg_of_mem_Icc ((Icc_subset_Icc_left (neg_nonpos_of_nonneg pi_div_two_pos.le)) hx)

Goal state after:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
⊢ Tendsto
    (fun n ↦ (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n ∂volume)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x ∂volume)
    atTop (𝓝 (f 0))
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (∏ i ∈ s, F i) y = (∑ i ∈ s, logDeriv (F i)) y

Tactic:
Finset.sum_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (∏ i ∈ s, F i) y = ∑ c ∈ s, logDeriv (F c) y
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
f : α → k
g : α → V
v : V
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 v)
⊢ Tendsto (fun x ↦ f x • g x) l (asymptoticNhds k V v)

Tactic:
rw [asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]
  exact tendsto_map.comp (hf.prodMk hg)

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

Goal state before:
pp: s : ℂ
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
suffices ∀ m : ℕ, ⌊1 - s.re⌋₊ = m → Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) by tauto

Goal state after:
s : ℂ
⊢ ∀ (m : ℕ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: case left
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
calc
      ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
⊢ MapsTo f s s

Tactic:
rintro e ⟨hx, hy⟩

Goal state after:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e ↦ ((e.trans R).trans e.symm).trans R
hf_dist : ∀ (e : PE ≃ᵢ PE), dist ((f e) z) z = 2 * dist (e z) z
e : PE ≃ᵢ PE
hx : e x = x
hy : e y = y
⊢ f e ∈ s
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

Goal state before:
pp: m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : T2Space 𝔸
inst✝ : Algebra ℚ 𝔸
v : m → 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • diagonal (v ^ n) = diagonal (∑' (n : ℕ), (↑n.factorial)⁻¹ • v ^ n)

Tactic:
← diagonal_smul,

Goal state after:
m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : T2Space 𝔸
inst✝ : Algebra ℚ 𝔸
v : m → 𝔸
⊢ ∑' (n : ℕ), diagonal ((↑n.factorial)⁻¹ • v ^ n) = diagonal (∑' (n : ℕ), (↑n.factorial)⁻¹ • v ^ n)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
⊢ normSq (exp q) = normSq (exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im))

Tactic:
exp_eq

Goal state after:
q : ℍ
⊢ normSq (exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) =
    normSq (exp q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im))
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h.inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
i : ℕ
hm : max 1 (‖x‖ ^ 0) = 1
hx : ‖x‖ ^ 0 ≤ 1
hi : i ∈ Finset.range (0 + 1)
⊢ ‖x‖ ^ i ≤ 1

pp: case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1

Tactic:
· simp only [pow_zero, le_refl,
        show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]

Goal state after:
case h.inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm✝ : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
hm : m ≠ 0
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedField F
inst✝ : NormedAlgebra ℝ F
⊢ Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)

Tactic:
by
  have : Algebra.IsAlgebraic ℝ F := by
    refine ⟨fun x ↦ ?_⟩
    obtain ⟨f, hf, hfx⟩ := exists_isMonicOfDegree_two_and_aeval_eq_zero x
    exact ⟨f, hf.ne_zero, hfx⟩
  exact _root_.Real.nonempty_algEquiv_or F

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

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ : AlgebraNorm R S
A : Subalgebra R S
f : AlgebraNorm R S
x : ↥A
hx : f ↑x = 0
⊢ x = 0

Tactic:
rw [← ZeroMemClass.coe_eq_zero]; exact eq_zero_of_map_eq_zero f hx

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖(Multiset.map (fun x ↦ a - x) g.roots).prod‖ = ‖eval a g‖

Tactic:
congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
⊢ iInf (seminormFromConst_seq c f (x ^ m)) = iInf (seminormFromConst_seq c f x) ^ m

Tactic:
apply tendsto_nhds_unique hlim

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' c f (x ^ m)))
⊢ Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (iInf (seminormFromConst_seq c f x) ^ m))
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: case a
K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Normal K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := ⋯
this✝¹ : FiniteDimensional K ↥K⟮y⟯
this✝ : IsUltrametricDist L
y' : ↥K⟮y⟯ := ⋯
zsep : IsSeparable (↥K⟮y⟯) z
this : z ∈ K⟮y⟯ ↔ z ∈ ⊥
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = σ.symm z
⊢ IsConjRoot (↥K⟮y⟯) x (z' + y)

Tactic:
simpa [z, y'] using IsConjRoot.add_algebraMap y' h1

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Krasner

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
xC' : C
hx' : xC' ∈ (minpoly K (iL x)).rootSet C
hne : iL x ≠ xC'
⊢ xC' ∈ (minpoly K x).rootSet C

Tactic:
minpoly.algHom_eq iL iL.injective x

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : NormedField L
inst✝⁴ : NontriviallyNormedField K
inst✝³ : CompleteSpace K
inst✝² : IsUltrametricDist K
inst✝¹ : NormedAlgebra K L
inst✝ : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this✝² : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this✝¹ : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst✝ : Algebra L C := iL.toAlgebra
this✝ : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := of_completeSpace_of_normal K C
norm_iL : ∀ (x : L), ‖iL x‖ = ‖x‖
xC' : C
hx' : xC' ∈ (minpoly K x).rootSet C
hne : iL x ≠ xC'
⊢ xC' ∈ (minpoly K x).rootSet C
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ 1 ∈ upperBounds (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ μ x ∈ upperBounds (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
simp only [mem_upperBounds, Set.mem_range, forall_exists_index]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ ∀ (x_1 : ℝ) (x_2 : ℕ), μ (x ^ s (ψ x_2)) ^ (1 / ↑(ψ x_2)) = x_1 → x_1 ≤ μ x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g : V ⟶ W
v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier
⊢ (Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f)) v =
    (Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g)) v

Tactic:
have : v.1 ∈ (f - g).hom.ker := v.2

Goal state after:
V W : SemiNormedGrp
f g : V ⟶ W
v : { carrier := ↥(Hom.hom (f - g)).ker, str := AddSubgroup.seminormedAddCommGroup }.carrier
this : ↑v ∈ (Hom.hom (f - g)).ker
⊢ (Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ f)) v =
    (Hom.hom (ofHom (NormedAddGroupHom.incl (Hom.hom (f - g)).ker) ≫ g)) v
Module: Mathlib.Analysis.Normed.Operator.Fredholm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 E
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
E₁ : Submodule 𝕜 E
E₁_closed : IsClosed[inst✝⁶] ↑E₁
E₁_coFG : E₁.CoFG
F₁ : Submodule 𝕜 F
F₁_closed : IsClosed[inst✝⁵] ↑F₁
F₁_coFG : F₁.CoFG
h_mapsto : MapsTo ⇑u ↑E₁ ↑F₁
h_inv : (u.restrict h_mapsto).IsInvertible
⊢ u.IsFredholm

Tactic:
by
  obtain ⟨e, he⟩ := h_inv
  have eqL : u.domRestrict E₁ = F₁.subtypeL ∘L e := congr(F₁.subtypeL ∘L $he).symm
  have eqₗ : u.toLinearMap.domRestrict E₁ = F₁.subtype ∘ₗ e := congr(($eqL).toLinearMap)
  have h : Topology.IsStrictMap u ∧ IsClosed (u.range : Set F) := by
    rw [u.isStrictMap_isClosed_range_iff_restrict E₁ E₁_closed, eqL]
    exact ⟨F₁.isEmbedding_subtype.comp e.isHomeomorph.isEmbedding |>.isStrictMap, by simpa⟩
  have disj : Disjoint E₁ u.ker := by
    rw [disjoint_iff_comap_eq_bot, ← LinearMap.ker_domRestrict, eqₗ,
      LinearMap.ker_comp, ker_subtype, comap_bot, LinearEquiv.ker]
  refine ⟨h.1, h.2, ?_, ?_, ?_⟩
  · rw [← Submodule.fg_iff_finiteDimensional]
    exact E₁_coFG.fg_of_disjoint disj.symm
  · refine F₁_coFG.of_le (le_trans ?_ (u.range_domRestrict_le_range E₁))
    rw [eqₗ, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top, range_subtype]
  · exact .of_disjoint_of_finiteDimensional_quotient E₁_closed disj.symm

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range

Tactic:
have v_ker : Disjoint v.ker B := by
    simp [disjoint_iff, v, B, toLinearMap_liftQL, ker_liftQ,
      map_inf_eq_map_inf_comap, comap_map_mkQ, N, inf_comm]

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁶] ↑A
inst✝ : A.CoFG
N : Submodule 𝕜 E := A ⊓ (↑u).ker
π : E →L[𝕜] E ⧸ N := N.mkQL
v : E ⧸ N →L[𝕜] F := N.liftQL u ⋯
π_quot : IsOpenQuotientMap ⇑π
u_eq : u = v ∘SL π
B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A
B_cofg : B.CoFG
v_ker : Disjoint (↑v).ker B
⊢ IsStrictMap ⇑u ∧ IsClosed[inst✝³] ↑(↑u).range ↔
    IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed[inst✝³] ↑(↑(u.domRestrict A)).range
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case mp
E : Type u_1
inst✝ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
r L : ℝ≥0
α : ↑(Icc tmin tmax) → E
hα1 : LipschitzWith L α
hα2 : α t₀ ∈ closedBall x₀ ↑r
⊢ (fun α ↦ toContinuousMap α) { toFun := α, lipschitzWith := hα1, mem_closedBall₀ := hα2 } ∈
    {α | LipschitzWith L ⇑α ∧ α t₀ ∈ closedBall x₀ ↑r}

Tactic:
exact ⟨hα1, hα2⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t ∈ {t | t * a ∈ Metric.ball t₀ ε}

Tactic:
mem_ofPred_eq,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
⊢ t ∈ Metric.ball (t₀ / a) (ε / |a|) ↔ t * a ∈ Metric.ball t₀ ε
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 y : 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
t₁ t₂ : ↑(Icc tmin tmax)
⊢ dist (picard f (↑t₀) x α.compProj ↑t₁) (picard f (↑t₀) x α.compProj ↑t₂) ≤ ↑L * dist t₁ t₂

Tactic:
by
    rw [dist_eq_norm, picard_apply, picard_apply, add_sub_add_left_eq_sub,
      integral_interval_sub_left (intervalIntegrable_comp_compProj hf _ t₁)
        (intervalIntegrable_comp_compProj hf _ t₂), Subtype.dist_eq, Real.dist_eq]
    apply intervalIntegral.norm_integral_le_of_norm_le_const
    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
    exact hf.norm_le _ ht _ <| α.mem_closedBall hf.mul_max_le

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) ~[atTop] fun x ↦
    P.leadingCoeff * x ^ P.natDegree

Tactic:
exact
      IsLittleO.add_isEquivalent
        (IsLittleO.fun_sum fun i hi =>
          IsLittleO.const_mul_left
            ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
              isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
            _)
        IsEquivalent.refl

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

Goal state before:
pp: P Q : ℤ[X]
mQ : Q.Monic
h : {a | eval a Q ∣ eval a P}.Infinite
R : ℤ[X] := P %ₘ Q
eqR : R + Q * (P /ₘ Q) = P
degR : R.degree < Q.degree
x : ℤ
mx : |eval x Q| ∣ eval x R ∧ |eval x R| < |eval x Q|
⊢ x ∈ {x | R.IsRoot x}

Tactic:
exact Int.eq_zero_of_abs_lt_dvd mx.1 mx.2

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

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : ¬tmin < tmax
t : ℝ
ht : t ∈ {t₀}
⊢ ContDiffWithinAt ℝ (↑n) (picard f t₀ x₀ α) {t₀} t

Tactic:
rw [eq_of_mem_singleton ht]

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E → E
α : ℝ → E
u : Set E
t₀ tmin tmax : ℝ
ht₀ : t₀ ∈ Icc tmin tmax
n : ℕ
hf : ContDiffOn ℝ (↑n) (uncurry f) (Icc tmin tmax ×ˢ u)
hα : ContinuousOn α (Icc tmin tmax)
hmem : ∀ t ∈ Icc tmin tmax, α t ∈ u
x₀ : E
heqon : ∀ t ∈ Icc tmin tmax, α t = picard f t₀ x₀ α t
hlt : ¬tmin < tmax
t : ℝ
ht : t ∈ {t₀}
⊢ ContDiffWithinAt ℝ (↑n) (picard f t₀ x₀ α) {t₀} t₀
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case neg.inr
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✝ ∈ {tmin}
⊢ ContDiffWithinAt ℝ (↑n) α {tmin} x✝

Tactic:
rw [eq_of_mem_singleton ht]

Goal state after:
case neg.inr
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✝ ∈ {tmin}
⊢ ContDiffWithinAt ℝ (↑n) α {tmin} tmin
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case inl
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h✝ : Even P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

pp: case inr
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h✝ : Odd P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

Tactic:
case inl h =>
    rw [Int.negOnePow_even] at hlc' ⊢
    · push_cast at hlc' ⊢; rw [one_mul] at hlc' ⊢
      have := zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg hroots' hlc'
      simpa using this
    · simpa
    · simpa [natDegree_comp]

Goal state after:
case inr
P : ℝ[X]
x : ℝ
hroots : ∀ (y : ℝ), P.IsRoot y → x < y
hlc : 0 ≤ P.leadingCoeff
hroots' : ∀ (y : ℝ), (P.comp (-X)).IsRoot y → y < -x
hlc' : 0 ≤ ↑↑(↑(P.comp (-X)).natDegree).negOnePow * (P.comp (-X)).leadingCoeff
h✝ : Odd P.natDegree
⊢ 0 < ↑↑(↑P.natDegree).negOnePow * eval x P