harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylorWithin_succ (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) :
    taylorWithin f (n + 1) s x₀ = taylorWithin f n s x₀ +
      PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)
      (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀))

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ taylorWithin f (n + 1) s x₀ =
    taylorWithin f n s x₀ +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))

Tactic:
dsimp only [taylorWithin]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ k ∈ Finset.range (n + 1 + 1),
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) =
    ∑ k ∈ Finset.range (n + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ k ∈ Finset.range (n + 1 + 1),
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) =
    ∑ k ∈ Finset.range (n + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        ((PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))

Tactic:
rw [Finset.sum_range_succ]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_iff (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
rw [isBasis_iff', and_iff_left hX]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
theorem equivalence₂CounitIso_eq :
    (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Proof state:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

Tactic:
ext Y'

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ 𝟙 (eB.inverse.obj (F.obj ((equivalence₁ hF).inverse.obj (eB.functor.obj Y')))) ≫
      eB.inverse.map
          (𝟙 (F.obj ((equivalence₁ hF).inverse.obj (eB.functor.obj Y'))) ≫
            (equivalence₁ hF).counitIso.hom.app (eB.functor.obj Y') ≫ 𝟙 (eB.functor.obj Y')) ≫
        eB.unitIso.inv.app Y' =
    (equivalence₂CounitIso eB hF).hom.app Y'

Tactic:
simp only [equivalence₁CounitIso_eq, equivalence₁CounitIso_hom_app, comp_id, id_comp,
  Functor.map_comp, assoc, equivalence₂CounitIso_hom_app]

Result:
no goals

Proof state:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ (equivalence₂ eB hF).counitIso.hom.app Y' = (equivalence₂CounitIso eB hF).hom.app Y'

Tactic:
dsimp [equivalence₂, Iso.refl]

Result:
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
Y' : B
⊢ 𝟙 (eB.inverse.obj (F.obj ((equivalence₁ hF).inverse.obj (eB.functor.obj Y')))) ≫
      eB.inverse.map
          (𝟙 (F.obj ((equivalence₁ hF).inverse.obj (eB.functor.obj Y'))) ≫
            (equivalence₁ hF).counitIso.hom.app (eB.functor.obj Y') ≫ 𝟙 (eB.functor.obj Y')) ≫
        eB.unitIso.inv.app Y' =
    (equivalence₂CounitIso eB hF).hom.app Y'
-- Mathlib/Topology/Category/Profinite/Extend.lean
/--
If the projection maps in the cone are epimorphic and the cone is limiting, then
`Profinite.Extend.functor` is initial.

TODO: investigate how to weaken the assumption `∀ i, Epi (c.π.app i)` to
`∀ i, ∃ j (_ : j ⟶ i), Epi (c.π.app j)`.
-/
lemma functor_initial (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Initial (functor c)

Proof state:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ∃ c' t, ((e.inverse ⋙ functor c).map t).right ≫ s = ((e.inverse ⋙ functor c).map t).right ≫ s'

Tactic:
refine ⟨⟨i⟩, 𝟙 _, ?_⟩

Result:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ ((e.inverse ⋙ functor c).map (𝟙 { down := i })).right ≫ s = ((e.inverse ⋙ functor c).map (𝟙 { down := i })).right ≫ s'
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_coe_mul (x : ℝ) (t : ℝ) :
    ‖(↑(t * x) : AddCircle (t * p))‖ = |t| * ‖(x : AddCircle p)‖

Proof state:
case inr.e_a.h.mpr.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ t * w - t * x ∈ zmultiples (t * p)

Tactic:
rw [← mul_sub]

Result:
case inr.e_a.h.mpr.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z w : ℝ
hw : w - x ∈ zmultiples p
hw' : |w| = |t|⁻¹ * z
⊢ t * (w - x) ∈ zmultiples (t * p)

Proof state:
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})

Tactic:
conv_rhs => rw [← smul_eq_mul, ← Real.sInf_smul_of_nonneg (abs_nonneg t)]

Result:
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = sInf (|t| • (fun a => |a|) '' {m | ↑m = ↑x})

Proof state:
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖

Tactic:
simp only [quotient_norm_eq, Real.norm_eq_abs]

Result:
case inr
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
⊢ sInf ((fun a => |a|) '' {m | ↑m = ↑(t * x)}) = |t| * sInf ((fun a => |a|) '' {m | ↑m = ↑x})

Proof state:
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ z ∈ |t| • (fun a => |a|) '' {m | m - x ∈ zmultiples p}

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ ht']

Result:
case inr.e_a.h
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
z : ℝ
⊢ z ∈ (fun a => |a|) '' {m | m - t * x ∈ zmultiples (t * p)} ↔ |t|⁻¹ • z ∈ (fun a => |a|) '' {m | m - x ∈ zmultiples p}

Proof state:
p x t a b c : ℝ
h : a ∈ zmultiples b
⊢ c * a ∈ zmultiples (c * b)

Tactic:
simp only [mem_zmultiples_iff] at h ⊢

Result:
p x t a b c : ℝ
h : ∃ k, k • b = a
⊢ ∃ k, k • (c * b) = c * a

Proof state:
case intro
p x t b c : ℝ
n : ℤ
⊢ ∃ k, k • (c * b) = c * n • b

Tactic:
exact ⟨n, (mul_smul_comm n c b).symm⟩

Result:
no goals

Proof state:
case inr.e_a.h.mp.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * y - x ∈ zmultiples p

Tactic:
rw [← inv_mul_cancel_left₀ ht x, ← inv_mul_cancel_left₀ ht p, ← mul_sub]

Result:
case inr.e_a.h.mp.intro.intro
p x t : ℝ
aux : ∀ {a b c : ℝ}, a ∈ zmultiples b → c * a ∈ zmultiples (c * b)
ht : t ≠ 0
ht' : |t| ≠ 0
y : ℝ
hy : y - t * x ∈ zmultiples (t * p)
⊢ t⁻¹ * (y - t * x) ∈ zmultiples (t⁻¹ * (t * p))
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem toSubring_zero : toSubring (0 : R[X]) T (by simp [coeffs]) = 0

Proof state:
R : Type u
S : Type u_1
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ ↑(coeffs 0) ⊆ ↑T

Tactic:
simp [coeffs]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0

Tactic:
ext i

Result:
case a.a
R : Type u
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 0 T ⋯).coeff i) = ↑(coeff 0 i)

Proof state:
case a.a
R : Type u
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 0 T ⋯).coeff i) = ↑(coeff 0 i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem head?_zipIdx (l : List α) (k : Nat) :
    (zipIdx l k).head? = l.head?.map fun a => (a, k)

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ (l.zipIdx k).head? = Option.map (fun a => (a, k)) l.head?

Tactic:
simp [head?_eq_getElem?]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental ℤ x

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < 1 / A

Tactic:
refine (lt_div_iff₀' hA).mpr ?_

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
-- Mathlib/Algebra/Lie/DirectSum.lean
theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
    ⁅of L i x, of L j y⁆ = if hij : i = j then of L i ⁅x, hij.symm.recOn y⁆ else 0

Proof state:
case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i : ι
x y : L i
⊢ ⁅(of L i) x, (of L i) y⁆ = if hij : i = i then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
simp only [lie_of_same L x y, dif_pos]

Result:
no goals

Proof state:
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i : ι
x y : L i
⊢ ⁅(of L i) x, (of L i) y⁆ = if hij : i = i then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Proof state:
case inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
x : L i
y : L j
hij : i ≠ j
⊢ ⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0

Tactic:
simp only [lie_of_of_ne L hij x y, hij, dif_neg, dite_false]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_eq_zero_iff (x : mixedSpace K) :
    convexBodySumFun x = 0 ↔ x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x = 0 ↔ x = 0

Tactic:
rw [← forall_normAtPlace_eq_zero_iff, convexBodySumFun, Finset.sum_eq_zero_iff_of_nonneg
  fun _ _ ↦ mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∀ i ∈ Finset.univ, ↑i.mult * (normAtPlace i) x = 0) ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∀ i ∈ Finset.univ, ↑i.mult * (normAtPlace i) x = 0) ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
conv =>
  enter [1, w, hw]
  rw [mul_left_mem_nonZeroDivisors_eq_zero_iff
    (mem_nonZeroDivisors_iff_ne_zero.mpr <| Nat.cast_ne_zero.mpr mult_ne_zero)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∀ w ∈ Finset.univ, (normAtPlace w) x = 0) ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∀ w ∈ Finset.univ, (normAtPlace w) x = 0) ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
simp_rw [Finset.mem_univ, true_implies]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.ball_eq_Ioo (x r : ℝ) : ball x r = Ioo (x - r) (x + r) :=
  Set.ext fun y => by
    rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add',
      sub_lt_comm]

Proof state:
x r y : ℝ
⊢ y ∈ ball x r ↔ y ∈ Ioo (x - r) (x + r)

Tactic:
rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add',
  sub_lt_comm]

Result:
no goals
-- Mathlib/Algebra/CharP/LocalRing.lean
theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [IsLocalRing R] (q : ℕ)
    [char_R_q : CharP R q] : q = 0 ∨ IsPrimePow q

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_zero : r = 0
K_char_p_0 : CharP K 0
K_char_zero : CharZero K
R_char_zero : CharZero R
q_zero : q = 0
⊢ IsPrimePow q

Tactic:
exact absurd q_zero q_pos

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
⊢ IsPrimePow q

Tactic:
let r := ringChar K

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
⊢ IsPrimePow q
-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and regular, they coincide up to a multiplicative constant. -/
@[to_additive isAddLeftInvariant_eq_smul_of_regular]
lemma isMulLeftInvariant_eq_smul_of_regular [LocallyCompactSpace G]
    (μ' μ : Measure G) [IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ']
    [Regular μ] [Regular μ'] :
    μ' = haarScalarFactor μ' μ • μ

Proof state:
G : Type u_1
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Group G
inst✝⁸ : IsTopologicalGroup G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : LocallyCompactSpace G
μ' μ : Measure G
inst✝⁴ : μ.IsHaarMeasure
inst✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : μ'.Regular
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
have A : ∀ U, IsOpen U → μ' U = (haarScalarFactor μ' μ • μ) U := by
  intro U hU
  rw [hU.measure_eq_iSup_isCompact, hU.measure_eq_iSup_isCompact]
  congr! 4 with K _KU K_comp
  exact measure_isMulLeftInvariant_eq_smul_of_ne_top μ' μ K_comp.measure_lt_top.ne
    K_comp.measure_lt_top.ne

Result:
G : Type u_1
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Group G
inst✝⁸ : IsTopologicalGroup G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : LocallyCompactSpace G
μ' μ : Measure G
inst✝⁴ : μ.IsHaarMeasure
inst✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : μ'.Regular
A : ∀ (U : Set G), IsOpen U → μ' U = (μ'.haarScalarFactor μ • μ) U
⊢ μ' = μ'.haarScalarFactor μ • μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_le_length_insert {l : List α} {a : α} : l.length ≤ (l.insert a).length

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.length ≤ (List.insert a l).length

Tactic:
rw [length_insert_of_mem h]

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.length ≤ l.length

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ (List.insert a l).length

Tactic:
rw [length_insert_of_not_mem h]

Result:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ l.length + 1

Proof state:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.length ≤ l.length

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ l.length ≤ (List.insert a l).length

Tactic:
by_cases h : a ∈ l

Result:
case pos
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : a ∈ l
⊢ l.length ≤ (List.insert a l).length

case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ (List.insert a l).length

Proof state:
case neg
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
h : ¬a ∈ l
⊢ l.length ≤ l.length + 1

Tactic:
exact Nat.le_succ _

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
/-- The order of an analytic function `f` at a `z₀` is infinity iff `f` vanishes locally around
`z₀`. -/
lemma order_eq_top_iff (hf : AnalyticAt 𝕜 f z₀) : hf.order = ⊤ ↔ ∀ᶠ z in 𝓝 z₀, f z = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ hf.order = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
unfold order

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤ else ↑⋯.choose) = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ↑⋯.choose = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
simpa only [ne_eq, ENat.coe_ne_top, false_iff] using h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (if h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0 then ⊤ else ↑⋯.choose) = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ⊤ = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ↑⋯.choose = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
h : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ⊤ = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
rwa [eq_self, true_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem natFloor_logb_natCast (b : ℕ) (n : ℕ) : ⌊logb b n⌋₊ = Nat.log b n

Proof state:
b n : ℕ
⊢ ⌊logb ↑b ↑n⌋₊ = Nat.log b n

Tactic:
obtain _ | _ | b := b

Result:
case zero
n : ℕ
⊢ ⌊logb ↑0 ↑n⌋₊ = Nat.log 0 n

case succ.zero
n : ℕ
⊢ ⌊logb ↑(0 + 1) ↑n⌋₊ = Nat.log (0 + 1) n

case succ.succ
n b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Proof state:
case succ.succ
n b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case succ.succ.inl
b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑0⌋₊ = Nat.log (b + 1 + 1) 0

case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Proof state:
case succ.zero
n : ℕ
⊢ ⌊logb ↑(0 + 1) ↑n⌋₊ = Nat.log (0 + 1) n

Tactic:
simp [Real.logb]

Result:
no goals

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 1 < ↑(b + 1 + 1)

Tactic:
simp [Nat.cast_add_one_pos]

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ ⌊logb ↑0 ↑n⌋₊ = Nat.log 0 n

Tactic:
simp [Real.logb]

Result:
no goals

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ ↑n

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ.inl
b : ℕ
⊢ ⌊logb ↑(b + 1 + 1) ↑0⌋₊ = Nat.log (b + 1 + 1) 0

Tactic:
simp

Result:
no goals

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌊logb ↑(b + 1 + 1) ↑n⌋₊ = Nat.log (b + 1 + 1) n

Tactic:
rw [← Nat.cast_inj (R := ℤ), Int.natCast_floor_eq_floor, floor_logb_natCast (by simp),
  Int.log_natCast]

Result:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n

Proof state:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n

Tactic:
exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by omega))

Result:
no goals