harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem aeval_iterate_derivative_of_ge (p : R[X]) (q : ℕ) {k : ℕ} (hk : q ≤ k) :
    ∃ gp : R[X], gp.natDegree ≤ p.natDegree - k ∧
      ∀ r : A, aeval r (derivative^[k] p) = q ! • aeval r gp

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
p' : R[X]
p'_le : p'.natDegree ≤ p.natDegree - k
hp' : (⇑derivative)^[k] p = k ! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk

Result:
case intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - (q + k) ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) gp

Proof state:
case intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - (q + k) ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) gp

Tactic:
refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) (↑((q + k).descFactorial k) * p')

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨p', p'_le, hp'⟩ := exists_iterate_derivative_eq_factorial_smul p k

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
p' : R[X]
p'_le : p'.natDegree ≤ p.natDegree - k
hp' : (⇑derivative)^[k] p = k ! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Proof state:
case intro.intro.intro
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) (↑((q + k).descFactorial k) * p')

Tactic:
simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
  Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
theorem toFun_spec (g : L ≃+* L) {n : ℕ} [NeZero n] (t : rootsOfUnity n L) :
    g (t : Lˣ) = (t ^ (χ₀ n g).val : Lˣ)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ g ↑↑t = ↑(↑t ^ (χ₀ n g).val)

Tactic:
rw [ModularCyclotomicCharacter_aux_spec g n t, ← zpow_natCast, ModularCyclotomicCharacter.toFun,
  ZMod.val_intCast, ← Subgroup.coe_zpow]

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ ModularCyclotomicCharacter_aux g n) =
    ↑(↑t ^ (ModularCyclotomicCharacter_aux g n % ↑(Fintype.card ↥(rootsOfUnity n L))))

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ ModularCyclotomicCharacter_aux g n) =
    ↑(↑t ^ (ModularCyclotomicCharacter_aux g n % ↑(Fintype.card ↥(rootsOfUnity n L))))

Tactic:
exact Units.ext_iff.1 <| SetCoe.ext_iff.2 <|
  zpow_eq_zpow_emod _ pow_card_eq_one (G := rootsOfUnity n L)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_of_support_subset (f : α →₀ M) {s : Finset α} (hs : f.support ⊆ s) (g : α → M → N)
    (h : ∀ i ∈ s, g i 0 = 1) : f.prod g = ∏ x ∈ s, g x (f x)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ f x = 0

Tactic:
exact not_mem_support_iff.1 hx

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ x ∈ s, g x (f x)

Tactic:
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ f x = 0
-- Mathlib/Analysis/Convex/Deriv.lean
lemma antitoneOn_derivWithin (hfc : ConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    AntitoneOn (derivWithin f S) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S y ≤ derivWithin f S x

Tactic:
rcases eq_or_lt_of_le hxy with rfl | hxy'

Result:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S y ≤ derivWithin f S x

Proof state:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

Tactic:
rfl

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ AntitoneOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S y ≤ derivWithin f S x

Proof state:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S y ≤ derivWithin f S x

Tactic:
exact (hfc.derivWithin_le_slope hx hy hxy' (hfd y hy)).trans
  (hfc.slope_le_derivWithin hx hy hxy' (hfd x hx))

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem MultilinearMap.mkContinuous_norm_le' (f : MultilinearMap 𝕜 E G) {C : ℝ}
    (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : ‖f.mkContinuous C H‖ ≤ max C 0 :=
  ContinuousMultilinearMap.opNorm_le_bound (le_max_right _ _) fun m ↦ (H m).trans <|
    mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
⊢ 0 ≤ ∏ i : ι, ‖m i‖

Tactic:
positivity

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem _root_.IsMax.withBot (h : IsMax a) : IsMax (a : WithBot α) :=
  fun x ↦ by cases x <;> simp; simpa using @h _

Proof state:
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
x : WithBot α
⊢ ↑a ≤ x → x ≤ ↑a

Tactic:
cases x <;> simp

Result:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ a ≤ a✝ → a✝ ≤ a

Proof state:
case coe
α : Type u_1
a : α
inst✝ : LE α
h : IsMax a
a✝ : α
⊢ a ≤ a✝ → a✝ ≤ a

Tactic:
simpa using @h _

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem transpose_eq_iff {μ ν : YoungDiagram} : μ.transpose = ν.transpose ↔ μ = ν

Proof state:
μ ν : YoungDiagram
⊢ μ.transpose = ν.transpose ↔ μ = ν

Tactic:
rw [transpose_eq_iff_eq_transpose]

Result:
μ ν : YoungDiagram
⊢ μ = ν.transpose.transpose ↔ μ = ν

Proof state:
μ ν : YoungDiagram
⊢ μ = ν.transpose.transpose ↔ μ = ν

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem sum_integral_adjacent_intervals {a : ℕ → ℝ} {n : ℕ}
    (hint : ∀ k < n, IntervalIntegrable f μ (a k) (a <| k + 1)) :
    ∑ k ∈ Finset.range n, ∫ x in a k..a <| k + 1, f x ∂μ = ∫ x in (a 0)..(a n), f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ

Tactic:
exact sum_integral_adjacent_intervals_Ico (zero_le n) fun k hk => hint k hk.2

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ

Tactic:
rw [← Nat.Ico_zero_eq_range]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0 ..a n, f x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
  | ⟨0, _⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
  | ⟨_ + 1, _⟩, _ => rfl

Proof state:
n : Nat
isLt✝ : 0 < n + 1
hi : ⟨0, isLt✝⟩ ≠ 0
⊢ (⟨0, isLt✝⟩.pred hi).succ = ⟨0, isLt✝⟩

Tactic:
simp only [mk_zero, ne_eq, not_true] at hi

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize.reduced' {num : Int} {den g : Nat} (den_nz : den ≠ 0)
    (e : g = num.natAbs.gcd den) : (num / g).natAbs.Coprime (den / g)

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = num.natAbs.gcd den
⊢ (num.tdiv ↑g).natAbs.Coprime (den / g)

Tactic:
exact normalize.reduced den_nz e

Result:
no goals

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = num.natAbs.gcd den
⊢ (num / ↑g).natAbs.Coprime (den / g)

Tactic:
rw [← Int.tdiv_eq_ediv_of_dvd (e ▸ Int.ofNat_dvd_left.2 (Nat.gcd_dvd_left ..))]

Result:
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = num.natAbs.gcd den
⊢ (num.tdiv ↑g).natAbs.Coprime (den / g)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem power_lt_aleph0 {a b : Cardinal} (ha : a < ℵ₀) (hb : b < ℵ₀) : a ^ b < ℵ₀ :=
  match a, b, lt_aleph0.1 ha, lt_aleph0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by rw [power_natCast, ← Nat.cast_pow]; apply nat_lt_aleph0

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀

Tactic:
apply nat_lt_aleph0

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ ↑n < ℵ₀

Tactic:
rw [power_natCast, ← Nat.cast_pow]

Result:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀
-- Mathlib/Topology/MetricSpace/Perfect.lean
theorem IsClosed.exists_nat_bool_injection_of_not_countable {α : Type*} [TopologicalSpace α]
    [PolishSpace α] {C : Set α} (hC : IsClosed C) (hunc : ¬C.Countable) :
    ∃ f : (ℕ → Bool) → α, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Tactic:
obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Function.Injective f
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Function.Injective f
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Tactic:
exact ⟨f, hfD.trans hDC, hf⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Tactic:
obtain ⟨D, hD, Dnonempty, hDC⟩ := exists_perfect_nonempty_of_isClosed_of_not_countable hC hunc

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Tactic:
letI := upgradePolishSpace α

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
lemma mahlerTerm_apply : mahlerTerm a n x = mahler n x • a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ_[p] E
a : E
n : ℕ
x : ℤ_[p]
⊢ (mahlerTerm a n) x = (mahler n) x • a

Tactic:
simp only [mahlerTerm, ContinuousMap.smul_apply', ContinuousMap.const_apply]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma divNat_zero (n : ℕ) : divNat n 0 = 0

Proof state:
n : ℕ
⊢ divNat n 0 = 0

Tactic:
simp [divNat]

Result:
n : ℕ
⊢ ⟨0, ⋯⟩ = 0

Proof state:
n : ℕ
⊢ ⟨0, ⋯⟩ = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem bind₁_frobeniusPoly_wittPolynomial (n : ℕ) :
    bind₁ (frobeniusPoly p) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) ((bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) =
    (MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))

Tactic:
simp only [map_bind₁, map_frobeniusPoly, bind₁_frobeniusPolyRat_wittPolynomial,
  map_wittPolynomial]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) ((bind₁ (frobeniusPoly p)) (wittPolynomial p ℤ n)) =
    (MvPolynomial.map (Int.castRingHom ℚ)) (wittPolynomial p ℤ (n + 1))
-- Mathlib/Algebra/DirectSum/Module.lean
theorem coeLinearMap_eq_dfinsupp_sum [DecidableEq M] (x : DirectSum ι fun i => A i) :
    coeLinearMap A x = DFinsupp.sum x fun i => (fun x : A i => ↑x)

Proof state:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x

Tactic:
simp only [LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype]

Result:
no goals

Proof state:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x

Tactic:
rw [DFinsupp.sumAddHom_apply]

Result:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x

Proof state:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x

Tactic:
simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk,
  AddHom.coe_mk]

Result:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem eq_bot_of_comap_eq_bot [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S]
    (hI : I.comap (algebraMap R S) = ⊥) : I = ⊥

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
⊢ x ∈ ⊥

Tactic:
by_cases hx0 : x = 0

Result:
case pos
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ x ∈ ⊥

case neg
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ x ∈ ⊥

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
⊢ I = ⊥

Tactic:
refine eq_bot_iff.2 fun x hx => ?_

Result:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
⊢ x ∈ ⊥

Proof state:
case pos
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ x ∈ ⊥

Tactic:
exact hx0.symm ▸ Ideal.zero_mem ⊥

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
I : Ideal S
inst✝³ : Algebra R S
inst✝² : Nontrivial R
inst✝¹ : IsDomain S
inst✝ : Algebra.IsIntegral R S
hI : comap (algebraMap R S) I = ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ x ∈ ⊥

Tactic:
exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

Result:
no goals
-- Mathlib/Algebra/CharP/Basic.lean
lemma charZero_iff_forall_prime_ne_zero [NonAssocRing R] [NoZeroDivisors R] [Nontrivial R] :
    CharZero R ↔ ∀ p : ℕ, p.Prime → (p : R) ≠ 0

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R

Tactic:
let p := ringChar R

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R

Proof state:
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R

Tactic:
have : CharP R 0 := h ▸ inferInstance

Result:
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R

Proof state:
case inl
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
hp : Nat.Prime p
⊢ CharZero R

Tactic:
simpa using h p hp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0

Tactic:
simp [hp.ne_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R

Tactic:
cases CharP.char_is_prime_or_zero R p with
| inl hp => simpa using h p hp
| inr h => have : CharP R 0 := h ▸ inferInstance; exact CharP.charP_to_charZero R

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0

Tactic:
refine ⟨fun h p hp => by simp [hp.ne_zero], fun h => ?_⟩

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R

Proof state:
case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R

Tactic:
exact CharP.charP_to_charZero R

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblY_smul (P : Fin 3 → R) (u : R) : W'.dblY (u • P) = u ^ 4 * W'.dblY P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.negDblY P) - W'.a₁ * (u ^ 4 * W'.dblX P) - W'.a₃ * (u ^ 4 * W'.dblZ P) =
    u ^ 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblY (u • P) = u ^ 4 * W'.dblY P

Tactic:
simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.negDblY P) - W'.a₁ * (u ^ 4 * W'.dblX P) - W'.a₃ * (u ^ 4 * W'.dblZ P) =
    u ^ 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem sum_repr_symm (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) :
    ∑ i, v i • b i = b.repr.symm v

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
v : EuclideanSpace 𝕜 ι
⊢ ∑ i : ι, v i • b i = b.repr.symm v

Tactic:
simpa using (b.toBasis.equivFun_symm_apply v).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_append_left {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :
    (l₁ ++ l₂)[i]? = l₁[i]?

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
hn : i < l₁.length
⊢ (l₁ ++ l₂)[i]? = l₁[i]?

Tactic:
have hn' : i < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
  length_append .. ▸ Nat.le_add_right ..

Result:
α : Type u_1
l₁ l₂ : List α
i : Nat
hn : i < l₁.length
hn' : i < (l₁ ++ l₂).length
⊢ (l₁ ++ l₂)[i]? = l₁[i]?

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
hn : i < l₁.length
hn' : i < (l₁ ++ l₂).length
⊢ (l₁ ++ l₂)[i]? = l₁[i]?

Tactic:
simp_all [getElem?_eq_getElem, getElem_append]

Result:
no goals