harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- If `λ` does not divide `x`, then `λ ^ 4` divides `x ^ 3 - 1` or `x ^ 3 + 1`. -/
lemma lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd {x : 𝓞 K} (h : ¬ λ ∣ x) :
    λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Proof state:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
contradiction

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with H | H | H

Result:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Proof state:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
right

Result:
case inr.inr.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Proof state:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
left

Result:
case inr.inl.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1

Proof state:
case inr.inr.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
exact lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

Result:
no goals

Proof state:
case inr.inl.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_add_of_diff {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) :
    v A + v (B \ A) = v B

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h : A ⊆ B
⊢ ↑v A + ↑v (B \ A) = ↑v B

Tactic:
rw [← of_union (@Set.disjoint_sdiff_right _ A B) hA (hB.diff hA), Set.union_diff_cancel h]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem principal_univ : 𝓟 (univ : Set α) = ⊤ :=
  top_unique <| by simp only [le_principal_iff, mem_top, eq_self_iff_true]

Proof state:
α : Type u
⊢ ⊤ ≤ 𝓟 univ

Tactic:
simp only [le_principal_iff, mem_top, eq_self_iff_true]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.mul_eq [DecidableEq I] (he : OrthogonalIdempotents e) (i j) :
    e i * e j = if i = j then e i else 0

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
⊢ e i * e j = if i = j then e i else 0

Tactic:
split

Result:
case isTrue
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : i = j
⊢ e i * e j = e i

case isFalse
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : ¬i = j
⊢ e i * e j = 0

Proof state:
case isFalse
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : ¬i = j
⊢ e i * e j = 0

Tactic:
exact he.ortho ‹_›

Result:
no goals

Proof state:
case isTrue
R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
h✝ : i = j
⊢ e i * e j = e i

Tactic:
simp [*, (he.idem j).eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

Tactic:
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
lemma pi {J : Type w} {C : J → Type u} {D : J → Type u'}
    [∀ j, Category.{v} (C j)] [∀ j, Category.{v'} (D j)]
    (W : ∀ j, MorphismProperty (C j)) (F : ∀ j, C j ⥤ D j)
    (hF : ∀ j, (W j).IsInvertedBy (F j)) :
    (MorphismProperty.pi W).IsInvertedBy (Functor.pi F)

Proof state:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
⊢ (MorphismProperty.pi W).IsInvertedBy (Functor.pi F)

Tactic:
intro _ _ f hf

Result:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ IsIso ((Functor.pi F).map f)

Proof state:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
j : J
⊢ IsIso ((Functor.pi F).map f j)

Tactic:
exact hF j _ (hf j)

Result:
no goals

Proof state:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ IsIso ((Functor.pi F).map f)

Tactic:
rw [isIso_pi_iff]

Result:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)

Proof state:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)

Tactic:
intro j

Result:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
j : J
⊢ IsIso ((Functor.pi F).map f j)
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_pow' {n : ℕ} (h : leadingCoeff p ^ n ≠ 0) : natDegree (p ^ n) = n * natDegree p :=
  letI := Classical.decEq R
  if hp0 : p = 0 then
    if hn0 : n = 0 then by simp [*] else by rw [hp0, zero_pow hn0]; simp
  else
    have hpn : p ^ n ≠ 0 := fun hpn0 => by
      have h1 := h
      rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h; exact h rfl
    Option.some_inj.1 <|
      show (natDegree (p ^ n) : WithBot ℕ) = (n * natDegree p : ℕ) by
        rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]; simp

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
simp [*]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ ↑(p ^ n).natDegree = ↑(n * p.natDegree)

Tactic:
rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ n • ↑p.natDegree = ↑(n * p.natDegree)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
rw [hp0, zero_pow hn0]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : 0 ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ n • ↑p.natDegree = ↑(n * p.natDegree)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
⊢ False

Tactic:
have h1 := h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : 0 ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
exact h rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree 0 = n * natDegree 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- The following statement says that summing over `N`-smooth numbers
for large enough `N` gets us arbitrarily close to the sum over all natural numbers
(assuming `f` is norm-summable and `f 0 = 0`; the latter since `0` is not smooth). -/
lemma norm_tsum_smoothNumbers_sub_tsum_lt (hsum : Summable f) (hf₀ : f 0 = 0)
    {ε : ℝ} (εpos : 0 < ε) :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ‖(∑' m : ℕ, f m) - ∑' m : N.smoothNumbers, f m‖ < ε

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
⊢ ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε

Tactic:
conv => enter [1, N₀, N]; rw [smoothNumbers_eq_factoredNumbers]

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
⊢ ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
N : ℕ
hN : N ≥ N₀
p : ℕ
hp : p ∈ N₀.primesBelow
⊢ p ∈ range N

Tactic:
exact mem_range.mpr <| (lt_of_mem_primesBelow hp).trans_le hN

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
⊢ ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε

Tactic:
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum hf₀ εpos

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
⊢ ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
⊢ ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers (range N))), f ↑m‖ < ε

Tactic:
refine ⟨N₀, fun N hN ↦ hN₀ (range N) fun p hp ↦ ?_⟩

Result:
case intro
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
N : ℕ
hN : N ≥ N₀
p : ℕ
hp : p ∈ N₀.primesBelow
⊢ p ∈ range N
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
/-- The measurability of a set `A` is equivalent to the measurability of the indicator function
which takes a constant value `b ≠ 0` on a set `A` and `0` elsewhere. -/
lemma measurable_indicator_const_iff [Zero β] [MeasurableSingletonClass β] (b : β) [NeZero b] :
    Measurable (s.indicator (fun (_ : α) ↦ b)) ↔ MeasurableSet s

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
⊢ s = (s.indicator fun x => b) ⁻¹' {0}ᶜ

Tactic:
ext a

Result:
case h.e'_3.h
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
a : α
⊢ a ∈ s ↔ a ∈ (s.indicator fun x => b) ⁻¹' {0}ᶜ

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x => b)

Tactic:
exact measurable_const.indicator h

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
⊢ MeasurableSet s

Tactic:
convert h (MeasurableSet.singleton (0 : β)).compl

Result:
case h.e'_3
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
⊢ s = (s.indicator fun x => b) ⁻¹' {0}ᶜ

Proof state:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ Measurable (s.indicator fun x => b) ↔ MeasurableSet s

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
⊢ MeasurableSet s

case mpr
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : MeasurableSet s
⊢ Measurable (s.indicator fun x => b)

Proof state:
case h.e'_3.h
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : Zero β
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
h : Measurable (s.indicator fun x => b)
a : α
⊢ a ∈ s ↔ a ∈ (s.indicator fun x => b) ⁻¹' {0}ᶜ

Tactic:
simp [NeZero.ne b]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
theorem mulShift_zero (ψ : AddChar R M) : mulShift ψ 0 = 1

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 0) x✝ = 1 x✝

Tactic:
rw [mulShift_apply, zero_mul, map_zero_eq_one, one_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 0 = 1

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 0) x✝ = 1 x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b

Proof state:
⊢ ∀ {a b : Bool}, a = (!a && b) ↔ (!a) = true ∧ (!b) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem hundred_div_ε_pow_five_le_m [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
    (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) : 100 / ε ^ 5 ≤ m :=
  (div_le_of_le_mul₀ (eps_pow_five_pos hPε).le (by positivity) hPε).trans <| by
    norm_cast
    rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
      univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 0 ≤ 4 ^ #P.parts

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts ≤ m

Tactic:
rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <|
  univ_nonempty.ne_empty).card_pos), stepBound, mul_left_comm, ← mul_pow]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts ≤ ↑m

Tactic:
norm_cast

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts ≤ m
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem padic_polynomial_dist {p : ℕ} [Fact p.Prime] (F : Polynomial ℤ_[p]) (x y : ℤ_[p]) :
    ‖F.eval x - F.eval y‖ ≤ ‖x - y‖ :=
  let ⟨z, hz⟩ := F.evalSubFactor x y
  calc
    ‖F.eval x - F.eval y‖ = ‖z‖ * ‖x - y‖

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1

Tactic:
apply PadicInt.norm_le_one

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖Polynomial.eval x F - Polynomial.eval y F‖ = ‖z‖ * ‖x - y‖

Tactic:
simp [hz]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖

Tactic:
gcongr

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1
-- Mathlib/Data/List/Cycle.lean
theorem isRotated_next_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
    l.next x hx = l'.next x (h.mem_iff.mp hx)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next (l.rotate n)[(l.length - n % l.length + k) % l.length] ⋯

Tactic:
rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ (l.rotate n)[(l.length - n % l.length + (k + 1) % l.length) % l.length] =
    (l.rotate n)[((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length]

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ (l.rotate n)[(l.length - n % l.length + (k + 1) % l.length) % l.length] =
    (l.rotate n)[((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length]

Tactic:
simp [add_assoc]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l.next l[k] hx = (l.rotate n).next l[k] ⋯

Tactic:
rw [next_getElem _ hn]

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next l[k] ⋯

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next l[k] ⋯

Tactic:
simp_rw [getElem_eq_getElem_rotate _ n k]

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next (l.rotate n)[(l.length - n % l.length + k) % l.length] ⋯

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.next l[k] hx = l'.next l[k] ⋯

Tactic:
obtain ⟨n, rfl⟩ := id h

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l.next l[k] hx = (l.rotate n).next l[k] ⋯

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.next x hx = l'.next x ⋯

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.next l[k] hx = l'.next l[k] ⋯
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_X (hk : 1 < k) : hasseDeriv k (X : R[X]) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (hasseDeriv k) X = 0

Tactic:
rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
  zero_mul, monomial_zero_right]

Result:
no goals