harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/WellQuasiOrder.lean
theorem wellQuasiOrderedLE_iff :
    WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ s : Set α, IsAntichain (· ≤ ·) s → s.Finite

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite

Tactic:
refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
  fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩

Result:
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
f : ℕ → α
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) (f m) (f n)

Proof state:
case intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
⊢ ¬(Set.range (f ∘ ⇑g)).Finite

Tactic:
refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_

Result:
case intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
⊢ m = n

Proof state:
case intro.inr.refine_1.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) n
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) n
h : m < n
⊢ False

Tactic:
exact hc _ _ (g.strictMono h) hf

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) (f m) (f n)

Tactic:
exfalso

Result:
case intro.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f (g m) > f (g n)
⊢ False
-- Mathlib/Order/SuccPred/Basic.lean
theorem lt_succ_bot_iff [NoMaxOrder α] : a < succ ⊥ ↔ a = ⊥

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a < succ ⊥ ↔ a = ⊥

Tactic:
rw [lt_succ_iff, le_bot_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpTo_top_iff' (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpTo N f p ↔
      (∀ x, (p x 0).curry0 = f x) ∧
        ∀ (m : ℕ) (x), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpTo N f p ↔
    (∀ (x : E), (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x

Tactic:
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff' hN, mem_univ,
  forall_true_left, hasFDerivWithinAt_univ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
/-- The length of a hamiltonian path is one less than the number of vertices of the graph. -/
lemma IsHamiltonian.length_eq (hp : p.IsHamiltonian) : p.length = Fintype.card α - 1 :=
  eq_tsub_of_add_eq <| by
    rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
      ← card_eq_sum_ones, hp.support_toFinset, card_univ]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ p.length + 1 = Fintype.card α

Tactic:
rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
  ← card_eq_sum_ones, hp.support_toFinset, card_univ]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netMaxcard_univ (T : X → X) {F : Set X} (h : F.Nonempty) (n : ℕ) :
    netMaxcard T F univ n = 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ netMaxcard T F univ n = 1

Tactic:
apply (iSup₂_le _).antisymm ((one_le_netMaxcard_iff T F univ n).2 h)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ ∀ (i : Finset X), IsDynNetIn T F univ n ↑i → ↑i.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ ∀ (i : Finset X), IsDynNetIn T F univ n ↑i → ↑i.card ≤ 1

Tactic:
intro s ⟨_, s_net⟩

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => ball x (dynEntourage T univ n)
⊢ ↑s.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Tactic:
exact PairwiseDisjoint.elim_set s_net x_s y_s x (mem_univ x) (mem_univ x)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ s.card ≤ 1

Tactic:
refine Finset.card_le_one.2 (fun x x_s y y_s ↦ ?_)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
x : X
x_s : x ∈ s
y : X
y_s : y ∈ s
⊢ x = y

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ ↑s.card ≤ 1

Tactic:
norm_cast

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ s.card ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => ball x (dynEntourage T univ n)
⊢ ↑s.card ≤ 1

Tactic:
simp only [ball, dynEntourage_univ, preimage_univ] at s_net

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x => univ
⊢ ↑s.card ≤ 1
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem derivative_succ_aux (n ν : ℕ) :
    Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) =
      (n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

Proof state:
case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * ↑(n - ν) = ↑(n + 1) * (↑(n.choose (ν + 1)) * X ^ (ν + 1))

Tactic:
rw [mul_comm, ← mul_assoc, ← mul_assoc]

Result:
case refine_2.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
⊢ ↑(n - ν) * ↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) = ↑(n + 1) * ↑(n.choose (ν + 1)) * X ^ (ν + 1)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_lt_sin_of_lt_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hy₂ : y ≤ π / 2)
    (hxy : x < y) : sin x < sin y

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith

Result:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y - x) / 2)
this : 0 < cos ((y + x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith

Result:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ sin x < sin y

Tactic:
rw [← sub_pos, sin_sub_sin]

Result:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y - x) / 2)

Tactic:
apply sin_pos_of_pos_of_lt_pi <;> linarith

Result:
no goals

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y - x) / 2)
this : 0 < cos ((y + x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
positivity

Result:
no goals

Proof state:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < cos ((y + x) / 2)

Tactic:
refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_neg (x y : BitVec w) : x * -y = -(x * y)

Proof state:
w : Nat
x y : BitVec w
⊢ x * -y = -(x * y)

Tactic:
rw [BitVec.mul_comm, BitVec.neg_mul, BitVec.mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_nat_three_mod_four {n : ℕ} (hn : n % 4 = 3) : χ₄ n = -1

Proof state:
n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
rw [χ₄_nat_mod_four, hn]

Result:
n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1

Proof state:
n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑3 = -1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma degree_eq_one_of_irreducible_of_root (hi : Irreducible p) {x : R} (hx : IsRoot p x) :
    degree p = 1 :=
  let ⟨g, hg⟩ := dvd_iff_isRoot.2 hx
  have : IsUnit (X - C x) ∨ IsUnit g := hi.isUnit_or_isUnit hg
  this.elim
    (fun h => by
      have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
      have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
      rw [h₁] at h₂; exact absurd h₂ (by decide))
    fun hgu => by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ ¬1 = 0

Tactic:
decide

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
⊢ p.degree = 1

Tactic:
have h₁ : degree (X - C x) = 1 := degree_X_sub_C x

Result:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
⊢ p.degree = 1

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ p.degree = 1

Tactic:
exact absurd h₂ (by decide)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
⊢ p.degree = 1

Tactic:
have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h

Result:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : (X - C x).degree = 0
⊢ p.degree = 1

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ p.degree = 1

Tactic:
rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : (X - C x).degree = 0
⊢ p.degree = 1

Tactic:
rw [h₁] at h₂

Result:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ p.degree = 1
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem tendsto_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f)
    (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) :
    Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1)

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine this ⌈x - 1⌉₊ ?_ ?_

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ ↑⌈x - 1⌉₊ < x

case refine_2
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ x ≤ ↑⌈x - 1⌉₊ + 1

Proof state:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
n : ℕ
hn : 1 ≤ n
this :
  logGammaSeq (x - 1 + 1) (n - 1) =
    logGammaSeq (x - 1) (n - 1 + 1) + log (x - 1) - (x - 1 + 1) * (log (↑(n - 1) + 1) - log ↑(n - 1))
⊢ logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)

Tactic:
rw [sub_add_cancel, Nat.sub_add_cancel hn] at this

Result:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
n : ℕ
hn : 1 ≤ n
this : logGammaSeq x (n - 1) = logGammaSeq (x - 1) n + log (x - 1) - x * (log (↑(n - 1) + 1) - log ↑(n - 1))
⊢ logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldr_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → β → β} {g : α → β → β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
    l.foldr f x = l.unattach.foldr g x

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldr f x l = foldr g x (map (fun x => x.val) l)
x : β
⊢ foldr f x (a :: l) = foldr g x (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x (map (fun x => x.val) l)

Tactic:
induction l generalizing x with
| nil => simp
| cons a l ih => simp [ih, hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → β
g : α → β → β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldr f x l = foldr g x (map (fun x => x.val) l)

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β → β
g : α → β → β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
x : β
⊢ foldr f x [] = foldr g x (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (map₂ f a b).map g = map₂ f' (a.map g₁) (b.map g₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)

Tactic:
cases a <;> cases b <;> simp [h_distrib]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_pow {n : ℕ} : (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
by_cases h : n = 0

Result:
case pos
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

case neg
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_pow]

Result:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Proof state:
case pos
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
simp only [h, zero_smul, Multiset.toFinset_zero, Finset.card_empty, ite_true]

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
simp only [h, Multiset.toFinset_nsmul _ n h, ite_false]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
theorem cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt [hp : Fact p.Prime] (n : ℕ) :
    ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).IsEisensteinAt 𝓟

Proof state:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ (if p ∣ i then ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) else 0) = 0

Tactic:
simp only [ite_eq_right_iff]

Result:
case refine_2.succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ p ∣ i → ((cyclotomic (p ^ (n + 1)) (ZMod p)).comp (X + 1)).coeff (i / p) = 0
-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `‖f n‖` is bounded by a constant times `n^x`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`. -/
lemma LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ}
    (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ x) : abscissaOfAbsConv f ≤ x + 1

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x
⊢ x = x + 1 - 1

Tactic:
ring

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
rw [show x = x + 1 - 1 by ring] at h

Result:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H

Result:
case intro.intro
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
by_contra! H

Result:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
⊢ False

Proof state:
case intro.intro
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False

Tactic:
exact (LSeriesSummable_of_le_const_mul_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
  |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem moveRight_card {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
    Finset.card (moveRight b m) + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b

Tactic:
exact tsub_add_cancel_of_le (card_of_mem_right h)

Result:
no goals

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ ((Finset.erase b m).erase (m.1 - 1, m.2)).card + 2 = Finset.card b

Tactic:
rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ (Finset.erase b m).card - 1 + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ (Finset.erase b m).card - 1 + 2 = Finset.card b

Tactic:
rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card b - 1 - 1 + 2 = Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) + 2 = Finset.card b

Tactic:
dsimp only [moveRight]

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ ((Finset.erase b m).erase (m.1 - 1, m.2)).card + 2 = Finset.card b
-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem minpoly_dvd_x_pow_sub_one : minpoly ℤ μ ∣ X ^ n - 1

Proof state:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ (Polynomial.aeval μ) (X ^ n - 1) = 0

Tactic:
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow, eq_intCast, Int.cast_one,
  aeval_one, map_sub, sub_self]

Result:
no goals

Proof state:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ minpoly ℤ μ ∣ X ^ n - 1

Tactic:
apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)

Result:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ (Polynomial.aeval μ) (X ^ n - 1) = 0

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ X ^ n - 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | h0)

Result:
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
h : IsPrimitiveRoot μ 0
⊢ minpoly ℤ μ ∣ X ^ 0 - 1

case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
h0 : n > 0
⊢ minpoly ℤ μ ∣ X ^ n - 1

Proof state:
case inl
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
h : IsPrimitiveRoot μ 0
⊢ minpoly ℤ μ ∣ X ^ 0 - 1

Tactic:
simp

Result:
no goals