harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_nonpos_iff (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.803082) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfc_neg]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.803082) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfc (fun x => -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.803082) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfc (fun x => -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x

Tactic:
exact cfc_nonneg_iff (fun x ↦ -f x) a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i

Proof state:
case succ
i n : Nat
ih : ∀ (x : Nat), x.testBit (i + n) = (x / 2 ^ n).testBit i
x : Nat
⊢ x.testBit (i + (n + 1)) = (x / 2 ^ (n + 1)).testBit i

Tactic:
rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
  Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]

Result:
no goals

Proof state:
case zero
i : Nat
⊢ ∀ (x : Nat), x.testBit (i + 0) = (x / 2 ^ 0).testBit i

Tactic:
simp

Result:
no goals

Proof state:
i n : Nat
⊢ ∀ (x : Nat), x.testBit (i + n) = (x / 2 ^ n).testBit i

Tactic:
induction n with
| zero => simp
| succ n ih =>
  intro x
  rw [← Nat.add_assoc, testBit_add_one, ih (x / 2),
    Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]

Result:
no goals

Proof state:
x i n : Nat
⊢ x.testBit (i + n) = (x / 2 ^ n).testBit i

Tactic:
revert x

Result:
i n : Nat
⊢ ∀ (x : Nat), x.testBit (i + n) = (x / 2 ^ n).testBit i

Proof state:
case succ
i n : Nat
ih : ∀ (x : Nat), x.testBit (i + n) = (x / 2 ^ n).testBit i
⊢ ∀ (x : Nat), x.testBit (i + (n + 1)) = (x / 2 ^ (n + 1)).testBit i

Tactic:
intro x

Result:
case succ
i n : Nat
ih : ∀ (x : Nat), x.testBit (i + n) = (x / 2 ^ n).testBit i
x : Nat
⊢ x.testBit (i + (n + 1)) = (x / 2 ^ (n + 1)).testBit i
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_X [Nontrivial R] {s : σ} :
    m.degree (X s : MvPolynomial σ R) = Finsupp.single s 1

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree (X s) = Finsupp.single s 1

Tactic:
classical
change m.degree (monomial (Finsupp.single s 1) (1 : R)) = _
rw [degree_monomial, if_neg one_ne_zero]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree ((monomial (Finsupp.single s 1)) 1) = Finsupp.single s 1

Tactic:
rw [degree_monomial, if_neg one_ne_zero]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree (X s) = Finsupp.single s 1

Tactic:
change m.degree (monomial (Finsupp.single s 1) (1 : R)) = _

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree ((monomial (Finsupp.single s 1)) 1) = Finsupp.single s 1
-- Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean
theorem eigenvalues_eq_spectrum_real {a : Matrix n n 𝕜} (ha : IsHermitian a) :
    spectrum ℝ a = Set.range (ha.eigenvalues)

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : Matrix n n 𝕜
ha : a.IsHermitian
⊢ spectrum ℝ a = Set.range ha.eigenvalues

Tactic:
ext x

Result:
case h
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : Matrix n n 𝕜
ha : a.IsHermitian
x : ℝ
⊢ x ∈ spectrum ℝ a ↔ x ∈ Set.range ha.eigenvalues

Proof state:
case h
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : Matrix n n 𝕜
ha : a.IsHermitian
x : ℝ
⊢ x ∈ spectrum ℝ a ↔ x ∈ Set.range ha.eigenvalues

Tactic:
conv_lhs => rw [ha.spectral_theorem, unitary.spectrum.unitary_conjugate,
← spectrum.algebraMap_mem_iff 𝕜, spectrum_diagonal, RCLike.algebraMap_eq_ofReal]

Result:
case h
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : Matrix n n 𝕜
ha : a.IsHermitian
x : ℝ
⊢ ↑x ∈ Set.range (RCLike.ofReal ∘ ha.eigenvalues) ↔ x ∈ Set.range ha.eigenvalues

Proof state:
case h
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : Matrix n n 𝕜
ha : a.IsHermitian
x : ℝ
⊢ ↑x ∈ Set.range (RCLike.ofReal ∘ ha.eigenvalues) ↔ x ∈ Set.range ha.eigenvalues

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_mapM (f : γ → α → m β) (xs : Option α) (hmono : monotone f) :
    monotone (fun x => xs.mapM (f x))

Proof state:
case some.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone fun x_1 => f x_1 x

Tactic:
apply monotone_apply

Result:
case some.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone f

Proof state:
case none
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
⊢ monotone fun x => Option.mapM (f x) none

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case some.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone fun x __do_lift => pure (some __do_lift)

Tactic:
apply monotone_const

Result:
no goals

Proof state:
case some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone fun x_1 => Option.mapM (f x_1) (some x)

Tactic:
apply monotone_bind

Result:
case some.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone fun x_1 => f x_1 x

case some.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone fun x __do_lift => pure (some __do_lift)

Proof state:
case some.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → α → m β
hmono : monotone f
x : α
⊢ monotone f

Tactic:
apply hmono

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ f.range = map f ⊤

Tactic:
ext

Result:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_nonneg_of_isNegNat {n : ℕ} (h : NormNum.IsInt e (.negOfNat n)) :
    0 ≤ Real.log (e : ℝ)

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log e

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Result:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
⊢ 0 ≤ Real.log (-↑n)

Tactic:
exact Real.log_neg_natCast_nonneg _

Result:
no goals
-- Mathlib/Topology/Instances/RatLemmas.lean
theorem not_countably_generated_nhds_infty_opc : ¬IsCountablyGenerated (𝓝 (∞ : ℚ∞))

Proof state:
a✝ : (𝓝 ∞).IsCountablyGenerated
⊢ False

Tactic:
have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance

Result:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated
⊢ False

Proof state:
⊢ ¬(𝓝 ∞).IsCountablyGenerated

Tactic:
intro

Result:
a✝ : (𝓝 ∞).IsCountablyGenerated
⊢ False

Proof state:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated
⊢ False

Tactic:
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this

Result:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (cocompact ℚ).IsCountablyGenerated
⊢ False

Proof state:
a✝ : (𝓝 ∞).IsCountablyGenerated
⊢ (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated

Tactic:
infer_instance

Result:
no goals

Proof state:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (cocompact ℚ).IsCountablyGenerated
⊢ False

Tactic:
exact not_countably_generated_cocompact this

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma algebraMap_le_iff_le_spectrum {r : R} {a : A} (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.823519) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
nth_rw 1 [← cfc_id R a]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.823519) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ cfc id a ↔ ∀ x ∈ spectrum R a, r ≤ x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.823519) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ (algebraMap R A) r ≤ cfc id a ↔ ∀ x ∈ spectrum R a, r ≤ x

Tactic:
exact algebraMap_le_cfc_iff id r a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem lt_rpow_inv_iff {x y : ℝ≥0∞} {z : ℝ} (hz : 0 < z) : x < y ^ z⁻¹ ↔ x ^ z < y

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
simp [hz]

Result:
no goals

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]

Result:
no goals

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← rpow_one x]

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 < y ^ z⁻¹ ↔ x ^ z < y
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
/-- Auxiliary lemma showing that for any `k : ℤ` and `(a : Fin 2 → ℤ)`
the extension of `eisSummand` is differentiable on `{z : ℂ | 0 < z.im}`. -/
lemma eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
    DifferentiableOn ℂ (↑ₕeisSummand k a) {z : ℂ | 0 < z.im}

Proof state:
k : ℤ
a : Fin 2 → ℤ
⊢ ∀ x ∈ {z | 0 < z.im}, (eisSummand k a ∘ ↑ofComplex) x = (↑(a 0) * x + ↑(a 1)) ^ (-k)

Tactic:
intro z hz

Result:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ (eisSummand k a ∘ ↑ofComplex) z = (↑(a 0) * z + ↑(a 1)) ^ (-k)

Proof state:
case intro
k : ℤ
a : Fin 2 → ℤ
z : ℍ
⊢ (eisSummand k a ∘ ↑ofComplex) ↑z = (↑(a 0) * ↑z + ↑(a 1)) ^ (-k)

Tactic:
apply comp_ofComplex

Result:
no goals

Proof state:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : z ∈ {z | 0 < z.im}
⊢ (eisSummand k a ∘ ↑ofComplex) z = (↑(a 0) * z + ↑(a 1)) ^ (-k)

Tactic:
lift z to ℍ using hz

Result:
case intro
k : ℤ
a : Fin 2 → ℤ
z : ℍ
⊢ (eisSummand k a ∘ ↑ofComplex) ↑z = (↑(a 0) * ↑z + ↑(a 1)) ^ (-k)

Proof state:
k : ℤ
a : Fin 2 → ℤ
⊢ DifferentiableOn ℂ (eisSummand k a ∘ ↑ofComplex) {z | 0 < z.im}

Tactic:
apply DifferentiableOn.congr (div_linear_zpow_differentiableOn k a)

Result:
k : ℤ
a : Fin 2 → ℤ
⊢ ∀ x ∈ {z | 0 < z.im}, (eisSummand k a ∘ ↑ofComplex) x = (↑(a 0) * x + ↑(a 1)) ^ (-k)
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma id_lift_eqToHom_domain {p : 𝒳 ⥤ 𝒮} {R S : 𝒮} (hRS : R = S) {a : 𝒳} (ha : p.obj a = R) :
    p.IsHomLift (eqToHom hRS) (𝟙 a)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
hRS : R = S
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (eqToHom hRS) (𝟙 a)

Tactic:
subst hRS ha

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 a)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_one (x : ℝ≥0∞) : x ^ (1 : ℝ) = x

Proof state:
x : ℝ≥0∞
⊢ x ^ 1 = x

Tactic:
cases x

Result:
case top

⊢ ⊤ ^ 1 = ⊤

case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝

Proof state:
case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝

Tactic:
change ite _ _ _ = _

Result:
case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 1 < 0 then ⊤ else ↑(x✝ ^ 1)) = ↑x✝

Proof state:
case coe
x✝ : ℝ≥0
⊢ x✝ = 0 → 1 < 0 → False

Tactic:
exact fun _ => zero_le_one.not_lt

Result:
no goals

Proof state:
case top

⊢ ⊤ ^ 1 = ⊤

Tactic:
exact dif_pos zero_lt_one

Result:
no goals

Proof state:
case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 1 < 0 then ⊤ else ↑(x✝ ^ 1)) = ↑x✝

Tactic:
simp only [NNReal.rpow_one, some_eq_coe, ite_eq_right_iff, top_ne_coe, and_imp]

Result:
case coe
x✝ : ℝ≥0
⊢ x✝ = 0 → 1 < 0 → False
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
/-- Upper bound for the summand `|c * z + d| ^ (-k)`, as a product of a function of `z` and a
function of `c, d`. -/
lemma summand_bound {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) :
    ‖x 0 * (z : ℂ) + x 1‖ ^ (-k) ≤ (r z) ^ (-k) * ‖x‖ ^ (-k)

Proof state:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]

Result:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)

Proof state:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Tactic:
rw [Real.zero_rpow h, mul_zero]

Result:
no goals

Proof state:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Tactic:
by_cases h : -k = 0

Result:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Proof state:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]

Result:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Proof state:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ 0 ^ (-k) ≤ r z ^ (-k) * 0 ^ (-k)

Tactic:
rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]

Result:
no goals

Proof state:
case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)

Tactic:
exact Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx)
  (neg_nonpos.mpr hk)

Result:
no goals

Proof state:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

Tactic:
by_cases hx : x = 0

Result:
case pos
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)

case neg
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
-- Mathlib/Data/Seq/Seq.lean
theorem mem_append_left {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂

Tactic:
intros

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ s'✝.append s₂
⊢ a ∈ (cons b✝ s'✝).append s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ a ∈ s₁.append s₂

Tactic:
apply mem_rec_on h

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ s'✝.append s₂
⊢ a ∈ (cons b✝ s'✝).append s₂

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma edgeSet_eq_empty : G.edgeSet = ∅ ↔ G = ⊥

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.edgeSet = ∅ ↔ G = ⊥

Tactic:
rw [← edgeSet_bot, edgeSet_inj]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithTop.lt_toDual_iff {x : WithBot αᵒᵈ} {y : WithTop α} :
    x < WithTop.toDual y ↔ y < WithBot.ofDual x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithBot αᵒᵈ
y : WithTop α
⊢ x < WithTop.toDual y ↔ y < WithBot.ofDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_of_limit {a b c : Ordinal} (a0 : a ≠ 0) (h : IsLimit b) :
    a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Proof state:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : b.IsLimit
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
rfl

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : b.IsLimit
⊢ a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c

Tactic:
rw [opow_limit a0 h, Ordinal.iSup_le_iff, Subtype.forall]

Result:
a b c : Ordinal.{u_1}
a0 : a ≠ 0
h : b.IsLimit
⊢ (∀ (a_1 : Ordinal.{u_1}) (b_1 : a_1 ∈ Iio b), a ^ ↑⟨a_1, b_1⟩ ≤ c) ↔ ∀ b' < b, a ^ b' ≤ c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
  | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
  | ofNat m, -[n+1] => by
    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
    rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
  | -[_+1], 0 => by rw [emod_zero]; rfl
  | -[m+1], succ n => aux m n.succ
  | -[m+1], -[n+1] => aux m n.succ
where
  aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1]

Proof state:
m n : Nat
⊢ ↑m % ↑n.succ + ↑n.succ * ↑(m / n.succ) = ↑m

Tactic:
exact congrArg ofNat <| Nat.mod_add_div ..

Result:
no goals

Proof state:
m n : Nat
⊢ ↑m % ↑n.succ + -↑n.succ * -↑(m / n.succ) = ↑m

Tactic:
rw [Int.neg_mul_neg]

Result:
m n : Nat
⊢ ↑m % ↑n.succ + ↑n.succ * ↑(m / n.succ) = ↑m

Proof state:
a✝ : Nat
⊢ -[a✝+1] + 0 * (-[a✝+1] / 0) = -[a✝+1]

Tactic:
rfl

Result:
no goals

Proof state:
a✝ : Nat
⊢ -[a✝+1] % 0 + 0 * (-[a✝+1] / 0) = -[a✝+1]

Tactic:
rw [emod_zero]

Result:
a✝ : Nat
⊢ -[a✝+1] + 0 * (-[a✝+1] / 0) = -[a✝+1]

Proof state:
x✝¹ x✝ : Int
m n : Nat
⊢ ↑n - (↑m % ↑n + 1) - (↑n * (↑m / ↑n) + ↑n) = -[m+1]

Tactic:
rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
  ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]

Result:
x✝¹ x✝ : Int
m n : Nat
⊢ -(↑(m % n) + ↑n * ↑(m / n) + 1) = -(↑m + 1)

Proof state:
m n : Nat
⊢ ofNat m % -[n+1] + -[n+1] * (ofNat m / -[n+1]) = ofNat m

Tactic:
show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m

Result:
m n : Nat
⊢ ↑m % ↑n.succ + -↑n.succ * -↑(m / n.succ) = ↑m

Proof state:
x✝¹ x✝ : Int
m n : Nat
⊢ -(↑(m % n) + ↑n * ↑(m / n) + 1) = -(↑m + 1)

Tactic:
exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)

Result:
no goals