harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_append_left {a : α} (pa : p a) {l₁ : Array α} l₂ (h : a ∈ l₁) :
    (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂

Proof state:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p = { toList := l₁ }.eraseP p ++ { toList := l₂ }

Tactic:
simpa using List.eraseP_append_left pa l₂ (by simpa using h)

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₂ : Array α
l₁ : List α
h : a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).eraseP p = { toList := l₁ }.eraseP p ++ l₂

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p = { toList := l₁ }.eraseP p ++ { toList := l₂ }

Proof state:
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₁ l₂ : Array α
h : a ∈ l₁
⊢ (l₁ ++ l₂).eraseP p = l₁.eraseP p ++ l₂

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l₂ : Array α
l₁ : List α
h : a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).eraseP p = { toList := l₁ }.eraseP p ++ l₂
-- Mathlib/Algebra/Quaternion.lean
theorem star_eq_two_re_sub : star a = ↑(2 * a.re) - a

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a = ↑(2 * a.re) - a

Tactic:
simp [a.star_eq_two_re_sub, Quaternion.coe]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- A version of σ_comp_σ with indices in ℕ satisfying relevant inequalities. -/
lemma σ_comp_σ_nat {n} (i j : ℕ) (hi : i < n + 1) (hj : j < n + 1) (H : i ≤ j) :
    σ ⟨i, by omega⟩ ≫ σ ⟨j, hj⟩ = σ ⟨j + 1, by omega⟩ ≫ σ ⟨i, hi⟩ :=
  σ_comp_σ (n := n) (i := ⟨i, by omega⟩) (j := ⟨j, by omega⟩) (by simpa)

Proof state:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ ⟨i, ⋯⟩ ≤ ⟨j, ⋯⟩

Tactic:
simpa

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ j < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ j + 1 < n + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ i < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n i j : ℕ
hi : i < n + 1
hj : j < n + 1
H : i ≤ j
⊢ i < n + 1 + 1

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem numeric_powHalf (n) : (powHalf n).Numeric

Proof state:
case succ
n : ℕ
hn : (powHalf n).Numeric
⊢ (powHalf (n + 1)).Numeric

Tactic:
constructor

Result:
case succ.left
n : ℕ
hn : (powHalf n).Numeric
⊢ ∀ (i j : PUnit.{u_1 + 1}), 0 i < (fun x => powHalf n) j

case succ.right
n : ℕ
hn : (powHalf n).Numeric
⊢ (∀ (i : PUnit.{u_1 + 1}), (0 i).Numeric) ∧ ∀ (j : PUnit.{u_1 + 1}), ((fun x => powHalf n) j).Numeric

Proof state:
case zero

⊢ (powHalf 0).Numeric

Tactic:
exact numeric_one

Result:
no goals

Proof state:
case succ.left
n : ℕ
hn : (powHalf n).Numeric
⊢ ∀ (i j : PUnit.{u_1 + 1}), 0 i < (fun x => powHalf n) j

Tactic:
simpa using hn.moveLeft_lt default

Result:
no goals

Proof state:
case succ.right
n : ℕ
hn : (powHalf n).Numeric
⊢ (∀ (i : PUnit.{u_1 + 1}), (0 i).Numeric) ∧ ∀ (j : PUnit.{u_1 + 1}), ((fun x => powHalf n) j).Numeric

Tactic:
exact ⟨fun _ => numeric_zero, fun _ => hn⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem L1.norm_eq_integral_norm (f : α →₁[μ] H) : ‖f‖ = ∫ a, ‖f a‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal = ∫ (a : α), ‖↑↑f a‖ ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall (by simp [norm_nonneg]))
    (Lp.aestronglyMeasurable f).norm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖↑↑f a‖ ∂μ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ ∀ (x : α), 0 x ≤ ‖↑↑f x‖

Tactic:
simp [norm_nonneg]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ ‖f‖ = ∫ (a : α), ‖↑↑f a‖ ∂μ

Tactic:
simp only [eLpNorm, eLpNorm'_eq_lintegral_enorm, ENNReal.one_toReal, ENNReal.rpow_one,
  Lp.norm_def, if_false, ENNReal.one_ne_top, one_ne_zero, _root_.div_one]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal = ∫ (a : α), ‖↑↑f a‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖↑↑f a‖ ∂μ).toReal

Tactic:
simp [ofReal_norm_eq_enorm]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem absorbent_closedBall (hpr : p x < r) : Absorbent 𝕜 (closedBall p x r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
⊢ Absorbent 𝕜 (p.closedBall x r)

Tactic:
refine (p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => ?_

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : y ∈ p.closedBall 0 (r - p x)
⊢ y ∈ p.closedBall x r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : y ∈ p.closedBall 0 (r - p x)
⊢ y ∈ p.closedBall x r

Tactic:
rw [p.mem_closedBall_zero] at hy

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y ≤ r - p x
⊢ y ∈ p.closedBall x r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
hpr : p x < r
y : E
hy : p y ≤ r - p x
⊢ y ∈ p.closedBall x r

Tactic:
exact p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_or_eq_of_mem_set {v : Vector α n} {i : Nat} {a b : α} {w : i < n} (h : a ∈ v.set i b) : a ∈ v ∨ a = b

Proof state:
α : Type u_1
n i : Nat
a b : α
w : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.set i b w
⊢ a ∈ toArray✝.set ?m.158133 b ?m.158136

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
a b : α
w : i < n
h : a ∈ v.set i b w
⊢ a ∈ v ∨ a = b

Tactic:
cases v

Result:
case mk
α : Type u_1
n i : Nat
a b : α
w : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.set i b w
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ a = b

Proof state:
case mk
α : Type u_1
n i : Nat
a b : α
w : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.set i b w
⊢ a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ a = b

Tactic:
simpa using Array.mem_or_eq_of_mem_set (by simpa using h)

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn {f : E → F} {s : Set E} {a : E}
    (h : ContDiffWithinAt 𝕜 n f s a) (hs : UniqueDiffOn 𝕜 s) (ha : a ∈ s) {m : ℕ} (hm : m ≤ n) :
    ∀ᶠ t in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn m f (ftaylorSeriesWithin 𝕜 f s) t

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (insert a s ∩ U)
⊢ ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U

Tactic:
rw [eventually_smallSets_subset]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (insert a s ∩ U)
⊢ s ∩ U ∈ 𝓝[s] a

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
⊢ ↑m = ∞ → n = ω

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
theorem hasStrictDerivAt_tan {x : ℂ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x

Proof state:
case h.e'_9
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (1 / cos x ^ 2) x

Tactic:
convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1

Result:
case h.e'_9
x : ℂ
h : cos x ≠ 0
⊢ 1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2

Proof state:
case h.e'_9
x : ℂ
h : cos x ≠ 0
⊢ 1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2

Tactic:
rw_mod_cast [← sin_sq_add_cos_sq x]

Result:
case h.e'_9
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {p q : ℝ}
    (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) :
    (∫⁻ a, f a * g a ^ (p - 1) ∂μ) ≤
      (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) * (∫⁻ a, g a ^ p ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), f a * g a ^ (p - 1) ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
refine le_trans (ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf (hg.pow_const _)) ?_

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤

Tactic:
by_contra h

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
h : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = ⊤
⊢ False

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (g a ^ (p - 1)) ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Tactic:
rw [hf_zero_rpow, zero_mul]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
⊢ 0 ≤ 0 * (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / q)

Proof state:
case neg.e_a.e_f.h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hf_zero_rpow : ¬(∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) = 0
hf_top_rpow : (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) ≠ ⊤
a : α
⊢ (g a ^ (p - 1)) ^ q = g a ^ p

Tactic:
rw [← ENNReal.rpow_mul, hpq.sub_one_mul_conj]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem not_strictAnti_of_wellFoundedLT [Preorder α] [WellFoundedLT α] (f : ℕ → α) :
    ¬ StrictAnti f := fun hf ↦
  (RelEmbedding.natGT f (fun n ↦ hf (by simp))).not_wellFounded_of_decreasing_seq wellFounded_lt

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
f : ℕ → α
hf : StrictAnti f
n : ℕ
⊢ n < n + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem mk'_eq_bot {l u : ι → ℝ} : mk' l u = ⊥ ↔ ∃ i, u i ≤ l i

Proof state:
ι : Type u_1
l u : ι → ℝ
⊢ mk' l u = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
rw [mk']

Result:
ι : Type u_1
l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i

Proof state:
ι : Type u_1
l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i

Tactic:
split_ifs with h <;> simpa using h

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS_odd_ofNat (m : ℕ) : preNormEDS b c d (2 * (m + 2) + 1) =
    preNormEDS b c d (m + 4) * preNormEDS b c d (m + 2) ^ 3 * (if Even m then b else 1) -
      preNormEDS b c d (m + 1) * preNormEDS b c d (m + 3) ^ 3 * (if Even m then 1 else b)

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 2) + 1) =
    (preNormEDS b c d (↑m + 4) * preNormEDS b c d (↑m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) ^ 3 * if Even m then 1 else b

Tactic:
repeat erw [preNormEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b

Tactic:
exact preNormEDS'_odd ..

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS b c d (↑m + 3) ^ 3 * if Even m then 1 else b

Tactic:
erw [preNormEDS_ofNat]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
-- Mathlib/Algebra/Group/Subgroup/Finsupp.lean
theorem mem_closure_range_iff_of_fintype [Fintype ι] :
    x ∈ closure (Set.range f) ↔ ∃ a : ι → ℤ, x = ∏ i, f i ^ a i

Proof state:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) ↔ ∃ b, x = ∏ i : ι, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = ∏ i : ι, f i ^ a i

Tactic:
rw [Finsupp.equivFunOnFinite.symm.exists_congr_left, mem_closure_range_iff]

Result:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) ↔ ∃ b, x = ∏ i : ι, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atTop_on_Ioi (hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (hg' : ∀ x ∈ Ioi a, g' x ≠ 0)
    (hftop : Tendsto f atTop (𝓝 0)) (hgtop : Tendsto g atTop (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) atTop l) : Tendsto (fun x => f x / g x) atTop l

Proof state:
case right
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ ((fun x => f' x / g' x) ∘ fun x => x⁻¹) x = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x

Tactic:
unfold Function.comp

Result:
case right
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f' x / g' x) ((fun x => x⁻¹) x) = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x
-- Mathlib/Logic/Relation.lean
theorem ReflTransGen.swap (h : ReflTransGen r b a) : ReflTransGen (swap r) a b

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen (Function.swap r) b b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : ReflTransGen r b a
⊢ ReflTransGen (Function.swap r) a b

Tactic:
induction h with
| refl => rfl
| tail _ hbc ih => exact ih.head hbc

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hbc : r b✝ c✝
ih : ReflTransGen (Function.swap r) b✝ b
⊢ ReflTransGen (Function.swap r) c✝ b

Tactic:
exact ih.head hbc

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_smul_of_not_equiv {P Q : Fin 3 → R} (h : ¬P ≈ Q) {u v : R} (hu : IsUnit u)
    (hv : IsUnit v) : W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]

Result:
no goals
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem toZ_iterate_pred_of_not_isMin (n : ℕ) (hn : ¬IsMin (pred^[n] i0)) :
    toZ i0 (pred^[n] i0) = -n

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
⊢ IsMin (pred^[n + 1] i0)

Tactic:
have h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0 := by
  rwa [Function.iterate_zero, id]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
h_pred_iterate_eq : pred^[n.succ] i0 = i0
h_pred_eq_pred : pred^[n.succ] i0 = pred^[0] i0
⊢ IsMin (pred^[n + 1] i0)

Proof state:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑m

Tactic:
rw [Int.toNat_eq_max, toZ_of_lt this, max_eq_left, neg_neg]

Result:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ 0 ≤ - -↑(Nat.find ⋯)

Proof state:
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
let m := (-toZ i0 (pred^[n.succ] i0)).toNat

Result:
case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_four : sin (π / 4) = √2 / 2

Proof state:
⊢ sin (π / 4) = √2 / 2

Tactic:
trans sin (π / 2 ^ 2)

Result:
⊢ sin (π / 4) = sin (π / 2 ^ 2)


⊢ sin (π / 2 ^ 2) = √2 / 2

Proof state:
⊢ sin (π / 4) = sin (π / 2 ^ 2)

Tactic:
congr

Result:
case e_x.e_a

⊢ 4 = 2 ^ 2

Proof state:
case e_x.e_a

⊢ 4 = 2 ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomialX (P : Fin 3 → R) : eval P W'.polynomialX =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)) =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
rw [polynomialX_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)) =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem sUnion {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ) :
    NullMeasurableSet (⋃₀ s) μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃₀ s) μ

Tactic:
rw [sUnion_eq_biUnion]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ

Tactic:
exact MeasurableSet.biUnion hs h

Result:
no goals