harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem HasFTaylorSeriesUpToOn.contDiffOn {n : ℕ∞} {f' : E → FormalMultilinearSeries 𝕜 E F}
    (hf : HasFTaylorSeriesUpToOn n f f' s) : ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
⊢ ContDiffOn 𝕜 (↑n) f s

Tactic:
intro x hx m hm

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p s

Tactic:
exact ⟨f', hf.of_le (mod_cast hm)⟩

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ s ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p s

Tactic:
simp only [Set.insert_eq_of_mem hx, self_mem_nhdsWithin, true_and]

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
use s

Result:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
f' : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn (↑n) f f' s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ s ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p s
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_norm_left : (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ c, IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∃ c, IsBigOWith c l f' g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ c, IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∃ c, IsBigOWith c l f' g

Tactic:
exact exists_congr fun _ => isBigOWith_norm_left

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem top_le_iff : ∀ {a : WithTop α}, ⊤ ≤ a ↔ a = ⊤
  | (a : α) => by simp [not_top_le_coe _]
  | ⊤ => by simp

Proof state:
α : Type u_1
inst✝ : LE α
⊢ ⊤ ≤ ⊤ ↔ ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LE α
a : α
⊢ ⊤ ≤ ↑a ↔ ↑a = ⊤

Tactic:
simp [not_top_le_coe _]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_comp_two_mul_X (n : ℤ) : (S R n).comp (2 * X) = U R n

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ (S R 1).comp (2 * X) = U R 1

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (↑n + 1)).comp (2 * X) = U R (↑n + 1)
ih2 : (S R ↑n).comp (2 * X) = U R ↑n
⊢ (S R (↑n + 2)).comp (2 * X) = U R (↑n + 2)

Tactic:
simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (S R n).comp (2 * X) = U R n

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
| neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : (S R (-↑n)).comp (2 * X) = U R (-↑n)
ih2 : (S R (-↑n + 1)).comp (2 * X) = U R (-↑n + 1)
⊢ (S R (-↑n - 1)).comp (2 * X) = U R (-↑n - 1)

Tactic:
simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ (S R 0).comp (2 * X) = U R 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' heights.

This version of the lemma assumes that `α` is nonempty. In this case, the coercion from `ℕ∞` to
`WithBot ℕ∞` is on the outside fo the right-hand side, which is usually more convenient.

If `α` were empty, then `krullDim α = ⊥`. See `krullDim_eq_iSup_height` for the more general
version, with the coercion under the supremum.
-/
lemma krullDim_eq_iSup_height_of_nonempty [Nonempty α] : krullDim α = ↑(⨆ (a : α), height a)

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ i, ↑(height i) ≤ krullDim α

Tactic:
apply iSup_le

Result:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : α), ↑(height i) ≤ krullDim α

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α

Tactic:
rw [WithBot.coe_iSup (by bddDefault)]

Result:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ i, ↑(height i) ≤ krullDim α

Proof state:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : LTSeries α), ↑i.length ≤ ↑(⨆ a, height a)

Tactic:
intro p

Result:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
p : LTSeries α
⊢ ↑p.length ≤ ↑(⨆ a, height a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove (Set.range height)

Tactic:
bddDefault

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
p : LTSeries α
⊢ ↑p.length ≤ ↑(⨆ a, height a)

Tactic:
suffices p.length ≤ ⨆ (a : α), height a from (WithBot.unbotD_le_iff fun _ => this).mp this

Result:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
p : LTSeries α
⊢ ↑p.length ≤ ⨆ a, height a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, height a)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α

Proof state:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
p : LTSeries α
⊢ ↑p.length ≤ ⨆ a, height a

Tactic:
apply le_iSup_of_le p.last (length_le_height_last (p := p))

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : α), ↑(height i) ≤ krullDim α

Tactic:
apply height_le_krullDim

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)

Tactic:
apply iSup_le

Result:
case a.h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (i : LTSeries α), ↑i.length ≤ ↑(⨆ a, height a)
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_deleteMin {s : Heap α} (h : s.NoSibling) (eq : s.deleteMin le = some (a, s')) :
    s.size = s'.size + 1

Proof state:
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c : Heap α
⊢ (node a c nil).size = (combine le c).size + 1

Tactic:
rw [size_combine, size, size]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
h : s.NoSibling
eq : deleteMin le s = some (a, s')
⊢ s.size = s'.size + 1

Tactic:
cases h with cases eq | node a c => rw [size_combine, size, size]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem countP_cons (b : α) (s) : countP p (b ::ₘ s) = countP p s + if p b then 1 else 0 :=
  Quot.inductionOn s <| by simp [List.countP_cons]

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α),
    countP p (b ::ₘ Quot.mk (⇑(isSetoid α)) a) = countP p (Quot.mk (⇑(isSetoid α)) a) + if p b then 1 else 0

Tactic:
simp [List.countP_cons]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem naturality_1 (α : F ≅ G) (f : X ⟶ Y) : α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) : ((Ico n m).filter fun x => x < l) = [] :=
  filter_eq_nil_iff.2 fun k hk => by
     simp only [decide_eq_true_eq, not_lt]
     apply le_trans hln
     exact (mem.1 hk).1

Proof state:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true

Tactic:
simp only [decide_eq_true_eq, not_lt]

Result:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Proof state:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
apply le_trans hln

Result:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k

Proof state:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k

Tactic:
exact (mem.1 hk).1

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem compMultilinearMap_domDomCongr (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃)
    (f : MultilinearMap R (fun _ : ι₁ => M') M₂) :
    (g.compMultilinearMap f).domDomCongr σ = g.compMultilinearMap (f.domDomCongr σ)

Proof state:
case H
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x => M') M₂
x✝ : ι₂ → M'
⊢ (MultilinearMap.domDomCongr σ (g.compMultilinearMap f)) x✝ =
    (g.compMultilinearMap (MultilinearMap.domDomCongr σ f)) x✝

Tactic:
simp [MultilinearMap.domDomCongr]

Result:
no goals

Proof state:
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x => M') M₂
⊢ MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap (MultilinearMap.domDomCongr σ f)

Tactic:
ext

Result:
case H
R : Type uR
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M'
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M'
ι₁ : Type u_1
ι₂ : Type u_2
σ : ι₁ ≃ ι₂
g : M₂ →ₗ[R] M₃
f : MultilinearMap R (fun x => M') M₂
x✝ : ι₂ → M'
⊢ (MultilinearMap.domDomCongr σ (g.compMultilinearMap f)) x✝ =
    (g.compMultilinearMap (MultilinearMap.domDomCongr σ f)) x✝
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
lemma mFourier_zero : mFourier (0 : d → ℤ) = 1

Proof state:
case h
d : Type u_1
inst✝ : Fintype d
x : UnitAddTorus d
⊢ (mFourier 0) x = 1 x

Tactic:
simp only [mFourier, Pi.zero_apply, fourier_zero, Finset.prod_const_one, ContinuousMap.coe_mk,
  ContinuousMap.one_apply]

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ mFourier 0 = 1

Tactic:
ext x

Result:
case h
d : Type u_1
inst✝ : Fintype d
x : UnitAddTorus d
⊢ (mFourier 0) x = 1 x
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Finite α] [CommGroup α] :
    IsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Nat.card α)
this : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α

Tactic:
exact isSimpleGroup_of_prime_card rfl

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
h : IsSimpleGroup α
⊢ IsCyclic α ∧ Nat.Prime (Nat.card α)

Tactic:
exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
⊢ IsCyclic α ∧ Nat.Prime (Nat.card α) → IsSimpleGroup α

Tactic:
rintro ⟨_, hp⟩

Result:
case mpr.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Nat.card α)
⊢ IsSimpleGroup α

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Nat.card α)
⊢ IsSimpleGroup α

Tactic:
haveI : Fact (Nat.card α).Prime := ⟨hp⟩

Result:
case mpr.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Nat.card α)
this : Fact (Nat.Prime (Nat.card α))
⊢ IsSimpleGroup α

Proof state:
case mp
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
⊢ IsSimpleGroup α → IsCyclic α ∧ Nat.Prime (Nat.card α)

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
h : IsSimpleGroup α
⊢ IsCyclic α ∧ Nat.Prime (Nat.card α)

Proof state:
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
⊢ IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Nat.card α)

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
⊢ IsSimpleGroup α → IsCyclic α ∧ Nat.Prime (Nat.card α)

case mpr
α : Type u_1
inst✝¹ : Finite α
inst✝ : CommGroup α
⊢ IsCyclic α ∧ Nat.Prime (Nat.card α) → IsSimpleGroup α
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- In a `p`-th cyclotomic extension of `ℚ`, we have that `ζ - 1` divides `p` in `𝓞 K`. -/
lemma toInteger_sub_one_dvd_prime' [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) : ((hζ.toInteger - 1)) ∣ p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ hζ✝.toInteger - 1 ∣ ↑↑p

Tactic:
exact toInteger_sub_one_dvd_prime hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ hζ✝.toInteger - 1 ∣ ↑↑p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa using hcycl

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ hζ.toInteger - 1 ∣ ↑↑p
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem self_comp_symm (e : M₁ ≃SL[σ₁₂] M₂) : (e : M₁ → M₂) ∘ (e.symm : M₂ → M₁) = id

Proof state:
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e ∘ ⇑e.symm = id

Tactic:
ext x

Result:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ (⇑e ∘ ⇑e.symm) x = id x

Proof state:
case h
R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_6
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_7
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ (⇑e ∘ ⇑e.symm) x = id x

Tactic:
exact apply_symm_apply e x

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem setOf_wSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) :
    { y | s.WSameSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) s

Proof state:
case h
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y ↔ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
constructor

Result:
case h.mp
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y → ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

case h.mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ (∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y) → s.WSameSide x y

Proof state:
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x -ᵥ p = 0
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y

Tactic:
rw [vsub_eq_zero_iff_eq] at h

Result:
case h.mp.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y p₂ : P
hp₂ : p₂ ∈ s
h : x = p
⊢ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Real.logDeriv_cos : logDeriv (Real.cos) = -Real.tan

Proof state:
⊢ logDeriv cos = -tan

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logDeriv cos x✝ = (-tan) x✝

Proof state:
case h
x✝ : ℝ
⊢ logDeriv cos x✝ = (-tan) x✝

Tactic:
rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem compQuasiMeasurePreserving_toGerm {β : Type*} [MeasurableSpace β] {f : α → β} {ν}
    (g : β →ₘ[ν] γ) (hf : Measure.QuasiMeasurePreserving f μ ν) :
    (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f hf.tendsto_ae

Proof state:
α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
⊢ (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯

Tactic:
rcases g

Result:
case mk
α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) f hf).toGerm =
    (toGerm (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compTendsto f ⋯

Proof state:
case mk
α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) f hf).toGerm =
    (toGerm (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compTendsto f ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem liftOn_zero {p : Type*} (f : M → S → p) (H) : liftOn 0 f H = f 0 1

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
⊢ liftOn 0 f H = f 0 1

Tactic:
rw [← mk_zero 1, liftOn_mk]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem piEquivFin_apply (n : ℕ) (x : AdicCompletion I (Fin n → R)) :
    piEquivFin I n x = pi I (fun _ : Fin n ↦ R) x

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : AdicCompletion I (Fin n → R)
⊢ (piEquivFin I n) x = (pi I fun x => R) x

Tactic:
simp only [piEquivFin, piEquivOfFintype_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_finset' {s : Finset α} (hs : MeasurableSet (s : Set α)) :
    count (↑s : Set α) = s.card

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Finset α
hs : MeasurableSet ↑s
⊢ count ↑s = ↑s.card

Tactic:
simp [count_apply hs]

Result:
no goals