harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem aeval_algHom_eq_zero (ϕ : AdjoinRoot f →ₐ[R] S) : aeval (ϕ (root f)) f = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ (aeval (ϕ (root f))) f = 0

Tactic:
have h : ϕ.toRingHom.comp (of f) = algebraMap R S := RingHom.ext_iff.mpr ϕ.commutes

Result:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ (aeval (ϕ (root f))) f = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = eval₂ (ϕ.comp (of f)) (ϕ.toRingHom (root f)) f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ (aeval (ϕ (root f))) f = 0

Tactic:
rw [aeval_def, ← h, ← RingHom.map_zero ϕ.toRingHom, ← eval₂_root f, hom_eval₂]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
h : ϕ.comp (of f) = algebraMap R S
⊢ eval₂ (ϕ.comp (of f)) (ϕ (root f)) f = eval₂ (ϕ.comp (of f)) (ϕ.toRingHom (root f)) f
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem doublingGamma_add_one (s : ℝ) (hs : s ≠ 0) :
    doublingGamma (s + 1) = s * doublingGamma s

Proof state:
s : ℝ
hs : s ≠ 0
⊢ (s + 1).doublingGamma = s * s.doublingGamma

Tactic:
rw [doublingGamma, doublingGamma, (by abel : s + 1 - 1 = s - 1 + 1), add_div, add_assoc,
  add_halves (1 : ℝ), Gamma_add_one (div_ne_zero hs two_ne_zero), rpow_add two_pos, rpow_one]

Result:
s : ℝ
hs : s ≠ 0
⊢ Gamma (s / 2 + 1 / 2) * (s / 2 * Gamma (s / 2)) * (2 ^ (s - 1) * 2) / √π =
    s * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)

Proof state:
s : ℝ
hs : s ≠ 0
⊢ s + 1 - 1 = s - 1 + 1

Tactic:
abel

Result:
no goals

Proof state:
s : ℝ
hs : s ≠ 0
⊢ Gamma (s / 2 + 1 / 2) * (s / 2 * Gamma (s / 2)) * (2 ^ (s - 1) * 2) / √π =
    s * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2) * 2 ^ (s - 1) / √π)

Tactic:
ring

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c)

Proof state:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ c ^ 2 = (-c) ^ 2

Tactic:
exact (neg_sq c).symm

Result:
no goals

Proof state:
case intro.intro.intro.left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)

Tactic:
apply And.intro ha (And.intro hb _)

Result:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ a ^ 4 + b ^ 4 = (-c) ^ 2

Proof state:
a b c : ℤ
⊢ Minimal a b c → Minimal a b (-c)

Tactic:
rintro ⟨⟨ha, hb, heq⟩, h2⟩

Result:
case intro.intro.intro
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Minimal a b (-c)

Proof state:
case intro.intro.intro
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Minimal a b (-c)

Tactic:
constructor

Result:
case intro.intro.intro.left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)

case intro.intro.intro.right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs

Proof state:
case intro.intro.intro.right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs

Tactic:
rwa [Int.natAbs_neg c]

Result:
no goals

Proof state:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ a ^ 4 + b ^ 4 = (-c) ^ 2

Tactic:
rw [heq]

Result:
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ c ^ 2 = (-c) ^ 2
-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.exists_lb_support {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) :
    ∃ N, ∀ n, n < N → coeff hℱ n = 0

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Tactic:
obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ 0 ∈ Filter.map (fun f => f.coeff n) ℱ

Tactic:
apply Filter.mem_of_superset hN (fun _ ha ↦ ha _ hn)

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Tactic:
let _ : UniformSpace K := ⊥

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ N, ∀ n < N, coeff hℱ n = 0

Tactic:
refine ⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
    ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ Filter.map (fun f => f.coeff n) ℱ ≤ pure 0

Proof state:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ Filter.map (fun f => f.coeff n) ℱ ≤ pure 0

Tactic:
simp only [pure_zero, nonpos_iff]

Result:
case intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x✝ : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ 0 ∈ Filter.map (fun f => f.coeff n) ℱ
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Qary entropy is strictly decreasing in the interval [1 - q⁻¹, 1]. -/
lemma qaryEntropy_strictAntiOn (qLe2 : 2 ≤ q) :
    StrictAntiOn (qaryEntropy q) (Icc (1 - 1/q) 1)

Proof state:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
⊢ qaryEntropy q p2 < qaryEntropy q p1

Tactic:
apply strictAntiOn_of_deriv_neg (convex_Icc (1 - 1/(q : ℝ)) 1) _ _ hp1 hp2 p1le2

Result:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc (1 - 1 / ↑q) 1)

q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
⊢ ∀ x ∈ interior (Icc (1 - 1 / ↑q) 1), deriv (qaryEntropy q) x < 0

Proof state:
case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
⊢ ↑q - ↑q * p < 1

Tactic:
have : (q : ℝ) - 1 < p * q := by
  have tmp := mul_lt_mul_of_pos_right hp.1 qpos
  simp at tmp
  have : (q : ℝ) ≠ 0 := (ne_of_lt qpos).symm
  have asdfasfd : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q
    _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
    _ = q - 1 := by simp_all only [ne_eq, isUnit_iff_ne_zero, Rat.cast_eq_zero,
      not_false_eq_true, IsUnit.inv_mul_cancel]
  rwa [asdfasfd] at tmp

Result:
case a
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - 1 / ↑q) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - 1 / ↑q) 1
p1le2 : p1 < p2
p : ℝ
this✝ : 2 ≤ ↑q
qinv_lt_1 : (↑q)⁻¹ < 1
zero_lt_1_sub_p : 0 < 1 - p
hp : 1 - (↑q)⁻¹ < p ∧ p < 1
qpos : 0 < ↑q
this : ↑q - 1 < p * ↑q
⊢ ↑q - ↑q * p < 1
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem range_derivWithin_subset_closure_span_image
    (f : 𝕜 → F) {s t : Set 𝕜} (h : s ⊆ closure (s ∩ t)) :
    range (derivWithin f s) ⊆ closure (Submodule.span 𝕜 (f '' t))

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : x ∈ closure (s \ {x})
H' : DifferentiableWithinAt 𝕜 f s x
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
⊢ closure (s ∩ t) \ {x} ⊆ closure ((s ∩ t) \ {x})

Tactic:
convert closure_diff

Result:
case h.e'_3.h.e'_4
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : x ∈ closure (s \ {x})
H' : DifferentiableWithinAt 𝕜 f s x
A : closure (s \ {x}) ⊆ closure (closure (s ∩ t) \ {x})
⊢ {x} = closure {x}

Proof state:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x, slope f x x_1 ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure (s ∩ t)
x : 𝕜
H : (𝓝[s \ {x}] x).NeBot
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ slope f x y ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_preimage (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ (K.map f f.continuous) = μ K)
    (A : Set G) : μ.outerMeasure (f ⁻¹' A) = μ.outerMeasure A

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }

Tactic:
intro s hs

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A s : Set G
hs : IsOpen s
⊢ μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A s : Set G
hs : IsOpen s
⊢ μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }

Tactic:
convert μ.innerContent_comap f h ⟨s, hs⟩

Result:
no goals

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A

Tactic:
refine inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _
  (fun _ => f.isOpen_preimage) ?_

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
f : G ≃ₜ G
h : ∀ ⦃K : Compacts G⦄, μ (Compacts.map ⇑f ⋯ K) = μ K
A : Set G
⊢ ∀ (s : Set G) (hs : IsOpen s),
    μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
lemma functor_id (J : Type u) [LinearOrder J] :
    (functor (OrderHom.id (α := J))) = EnrichedFunctor.id _ _

Proof state:
case w.h
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝ a✝ =
    ((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝ a✝

Tactic:
exact Functor.ext (by aesop_cat)

Result:
no goals

Proof state:
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    (((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝ a✝).obj X =
      (((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝ a✝).obj X

Tactic:
aesop_cat

Result:
no goals

Proof state:
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ (functor OrderHom.id).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.id SSet (SimplicialThickening J)).map i j

Tactic:
ext

Result:
case w.h
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝ a✝ =
    ((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝ a✝

Proof state:
J : Type u
inst✝ : LinearOrder J
⊢ functor OrderHom.id = EnrichedFunctor.id SSet (SimplicialThickening J)

Tactic:
refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Result:
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ (functor OrderHom.id).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.id SSet (SimplicialThickening J)).map i j
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma IsNilpotent.pow_succ (n : ℕ) {S : Type*} [MonoidWithZero S] {x : S}
    (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ)

Proof state:
case intro
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
N : ℕ
hN : x ^ N = 0
⊢ IsNilpotent (x ^ n.succ)

Tactic:
use N

Result:
case h
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0

Proof state:
case h
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
N : ℕ
hN : x ^ N = 0
⊢ (x ^ n.succ) ^ N = 0

Tactic:
rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]

Result:
no goals

Proof state:
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
⊢ IsNilpotent (x ^ n.succ)

Tactic:
obtain ⟨N, hN⟩ := hx

Result:
case intro
n : ℕ
S : Type u_3
inst✝ : MonoidWithZero S
x : S
N : ℕ
hN : x ^ N = 0
⊢ IsNilpotent (x ^ n.succ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_bmod {x : Int} {m : Nat} (h : 0 < m) : - (m/2) ≤ Int.bmod x m

Proof state:
case isTrue
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ x % ↑m

Tactic:
refine Int.le_trans ?_ (Int.emod_nonneg _ ?_)

Result:
case isTrue.refine_1
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ 0

case isTrue.refine_2
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ ↑m ≠ 0

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ 1 * q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
rw [← Int.add_mul, show (1 + -2 : Int) = -1 by decide]

Result:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ -1 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 1 + -2 = -1

Tactic:
decide

Result:
no goals

Proof state:
case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean
theorem IsZero.obj [HasZeroObject D] {F : C ⥤ D} (hF : IsZero F) (X : C) : IsZero (F.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)

Tactic:
have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
⊢ IsZero (F.obj X)

Tactic:
let e : F ≅ G := hF.iso hG

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := hF.iso hG
⊢ IsZero (F.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)

Tactic:
let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
⊢ IsZero (F.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
G : C ⥤ D := (Functor.const C).obj 0
hG : IsZero G
e : F ≅ G := hF.iso hG
⊢ IsZero (F.obj X)

Tactic:
exact (isZero_zero _).of_iso (e.app X)

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem cancel_left_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g :=
  ⟨fun h => by simpa using RespectsIso.precomp P (inv f) (f ≫ g) h, RespectsIso.precomp P f g⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g

Tactic:
simpa using RespectsIso.precomp P (inv f) (f ≫ g) h

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem pi_zero : pi (fun _ => 0 : (i : ι) → M₂ →ₗ[R] φ i) = 0

Proof state:
case h.h
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
x✝¹ : M₂
x✝ : ι
⊢ (pi fun x => 0) x✝¹ x✝ = 0 x✝¹ x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
⊢ (pi fun x => 0) = 0

Tactic:
ext

Result:
case h.h
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
x✝¹ : M₂
x✝ : ι
⊢ (pi fun x => 0) x✝¹ x✝ = 0 x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem mem_cons {v : α} {c} {f : CNF α} :
    Mem v (c :: f : CNF α) ↔ (Clause.Mem v c ∨ Mem v f)

Proof state:
α : Type u_1
v : α
c : Clause α
f : CNF α
⊢ Mem v (c :: f) ↔ Clause.Mem v c ∨ Mem v f

Tactic:
simp [Mem]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : ZMod n).val = a

Proof state:
n a : ℕ
h : a < n
⊢ (↑a).val = a

Tactic:
rw [val_natCast, Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_singleton'' (s : Finset β) (f : β → α) :
    (s.sup fun b => {f b}) = s.image f

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ s.sup fun b => {f b}) ↔ a ∈ image f s

Tactic:
rw [mem_sup, mem_image]

Result:
case h
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ i ∈ s, a ∈ {f i}) ↔ ∃ a_1 ∈ s, f a_1 = a

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ i ∈ s, a ∈ {f i}) ↔ ∃ a_1 ∈ s, f a_1 = a

Tactic:
simp only [mem_singleton, eq_comm]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
⊢ (s.sup fun b => {f b}) = image f s

Tactic:
ext a

Result:
case h
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ s.sup fun b => {f b}) ↔ a ∈ image f s
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem tendsto_integral_smul_of_tendsto_average_norm_sub
    [CompleteSpace E]
    {ι : Type*} {a : ι → Set α} {l : Filter ι} {f : α → E} {c : E} {g : ι → α → ℝ} (K : ℝ)
    (hf : Tendsto (fun i ↦ ⨍ y in a i, ‖f y - c‖ ∂μ) l (𝓝 0))
    (f_int : ∀ᶠ i in l, IntegrableOn f (a i) μ)
    (hg : Tendsto (fun i ↦ ∫ y, g i y ∂μ) l (𝓝 1))
    (g_supp : ∀ᶠ i in l, Function.support (g i) ⊆ a i)
    (g_bound : ∀ᶠ i in l, ∀ x, |g i x| ≤ K / (μ (a i)).toReal) :
    Tendsto (fun i ↦ ∫ y, g i y • f y ∂μ) l (𝓝 c)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i => ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / (μ (a i)).toReal
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / (μ (a i)).toReal
A : (support fun y => g i y • f y) ⊆ a i
⊢ IntegrableOn (fun y => g i y • f y) (a i) μ

Tactic:
apply Integrable.smul_of_top_right hif

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i => ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / (μ (a i)).toReal
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / (μ (a i)).toReal
A : (support fun y => g i y • f y) ⊆ a i
⊢ MemLp (g i) ⊤ (μ.restrict (a i))
-- Mathlib/Data/Set/Function.lean
theorem bijOn_empty_iff_right : BijOn f ∅ t ↔ t = ∅ :=
  ⟨fun h ↦ by simpa using h.surjOn, by rintro rfl; exact bijOn_empty f⟩

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
simpa using h.surjOn

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
exact bijOn_empty f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ t = ∅ → BijOn f ∅ t

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅