harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_le_pow_of_le_one [ZeroLEOneClass M₀] [PosMulMono M₀] [MulPosMono M₀] (ha₀ : 0 ≤ a)
    (ha₁ : a ≤ 1) : ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m
  | _, _, Nat.le.refl => le_rfl
  | _, _, Nat.le.step h => by
    rw [pow_succ']
    exact (mul_le_of_le_one_left (pow_nonneg ha₀ _) ha₁).trans <| pow_le_pow_of_le_one ha₀ ha₁ h

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n✝ m✝ : ℕ
h : n✝.le m✝
⊢ a * a ^ m✝ ≤ a ^ n✝

Tactic:
exact (mul_le_of_le_one_left (pow_nonneg ha₀ _) ha₁).trans <| pow_le_pow_of_le_one ha₀ ha₁ h

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n✝ m✝ : ℕ
h : n✝.le m✝
⊢ a ^ m✝.succ ≤ a ^ n✝

Tactic:
rw [pow_succ']

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n✝ m✝ : ℕ
h : n✝.le m✝
⊢ a * a ^ m✝ ≤ a ^ n✝
-- Mathlib/Algebra/Quaternion.lean
theorem star_mul_self : star a * a = normSq a

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

Tactic:
rw [star_comm_self, self_mul_star]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
lemma const {y : Y} :
    HolderWith C r (Function.const X y) := fun x₁ x₂ => by
  simp only [Function.const_apply, edist_self, zero_le]

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
y : Y
x₁ x₂ : X
⊢ edist (Function.const X y x₁) (Function.const X y x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Tactic:
simp only [Function.const_apply, edist_self, zero_le]

Result:
no goals
-- Mathlib/Algebra/GradedMonoid.lean
theorem list_prod_ofFn_mem_graded {n} (i : Fin n → ι) (r : Fin n → R) (h : ∀ j, r j ∈ A (i j)) :
    (List.ofFn r).prod ∈ A (List.ofFn i).sum

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.ofFn r).prod ∈ A (List.ofFn i).sum

Tactic:
rw [List.ofFn_eq_map, List.ofFn_eq_map]

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum

Tactic:
exact list_prod_map_mem_graded _ _ _ fun _ _ => h _

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem Int.Prime.dvd_pow {n : ℤ} {k p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ n ^ k) :
    p ∣ n.natAbs

Proof state:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ n.natAbs ^ k
⊢ p ∣ n.natAbs

Tactic:
exact hp.dvd_of_dvd_pow h

Result:
no goals

Proof state:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs

Tactic:
rw [Int.natCast_dvd, Int.natAbs_pow] at h

Result:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ n.natAbs ^ k
⊢ p ∣ n.natAbs
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
/--
The closure of a singleton `{a}` in the upper set topology is the right-closed left-infinite
interval (-∞,a].
-/
@[simp] lemma closure_singleton {a : α} : closure {a} = Iic a

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ closure {a} = Iic a

Tactic:
rw [closure_eq_lowerClosure, lowerClosure_singleton]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
@[reassoc (attr := simp)]
lemma hom_left_inv_left {f g : Over X} (e : f ≅ g) :
    e.hom.left ≫ e.inv.left = 𝟙 f.left

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
e : f ≅ g
⊢ e.hom.left ≫ e.inv.left = 𝟙 f.left

Tactic:
simp [← Over.comp_left]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem not_rankInfinite (M : Matroid α) [RankFinite M] : ¬ RankInfinite M

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
⊢ False

Tactic:
obtain ⟨B,hB⟩ := M.exists_isBase

Result:
case intro
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
⊢ ¬M.RankInfinite

Tactic:
intro h

Result:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
⊢ False

Proof state:
case intro
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
h : M.RankInfinite
B : Set α
hB : M.IsBase B
⊢ False

Tactic:
exact hB.infinite hB.finite

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [Field K] (f : K[X]) (a : K)
    (hf' : f.derivative.eval a ≠ 0) : IsCoprime (X - C a : K[X]) (f /ₘ (X - C a))

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ ¬X - C a ∣ f /ₘ (X - C a)

Tactic:
contrapose! hf' with h

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
⊢ eval a (derivative f) = 0

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
⊢ eval a (derivative f) = 0

Tactic:
have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : X - C a ∣ derivative f
⊢ eval a (derivative f) = 0

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : C (eval a (derivative f)) = 0
⊢ eval a (derivative f) = 0

Tactic:
rwa [← C_inj, C_0]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ IsCoprime (X - C a) (f /ₘ (X - C a))

Tactic:
refine Or.resolve_left
    (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
      (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ ¬X - C a ∣ f /ₘ (X - C a)

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf' : eval a (derivative f) ≠ 0
⊢ IsCoprime (X - C a) (f /ₘ (X - C a))

Tactic:
classical
refine Or.resolve_left
    (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
      (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_
contrapose! hf' with h
have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this
rwa [← C_inj, C_0]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : X - C a ∣ derivative f
⊢ eval a (derivative f) = 0

Tactic:
rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : C (eval a (derivative f)) = 0
⊢ eval a (derivative f) = 0
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_div_const (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝕜') :
    derivWithin (fun x => c x / d) s x = derivWithin c s x / d

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝕜'
⊢ derivWithin (fun x => c x / d) s x = derivWithin c s x / d

Tactic:
simp [div_eq_inv_mul, derivWithin_const_mul, hc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ List.map f l₁ <:+: List.map f l₂

Tactic:
obtain ⟨r₁, r₂, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r₁ r₂ : List α
⊢ List.map f l₁ <:+: List.map f (r₁ ++ l₁ ++ r₂)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r₁ r₂ : List α
⊢ List.map f l₁ <:+: List.map f r₁ ++ List.map f l₁ ++ List.map f r₂

Tactic:
apply infix_append

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r₁ r₂ : List α
⊢ List.map f l₁ <:+: List.map f (r₁ ++ l₁ ++ r₂)

Tactic:
rw [map_append, map_append]

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ r₁ r₂ : List α
⊢ List.map f l₁ <:+: List.map f r₁ ++ List.map f l₁ ++ List.map f r₂
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
@[simp]
lemma rnDeriv_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
    μ.rnDeriv ν =ᵐ[ν] 0 ↔ μ ⟂ₘ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ ⟂ₘ ν

Tactic:
rw [← withDensity_rnDeriv_eq_zero, withDensity_eq_zero_iff (measurable_rnDeriv _ _).aemeasurable]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_union_Ici (h : c ≤ max a b) : Ico a b ∪ Ici c = Ici (min a c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ a ⊔ b
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
rcases le_total a b with hab | hab <;> simp [hab] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c ≤ a
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Ico a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
exact Ico_union_Ici' h

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_factors (I : FractionalIdeal R⁰ K) :
    ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite, count K v I = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
by_cases hI : I = 0

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
convert finite_factors' hI (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2

Result:
case h.e'_2.h.h.e'_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : ¬I = 0
x✝ : HeightOneSpectrum R
⊢ count K x✝ I =
    ↑((Associates.mk x✝.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk x✝.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I = 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, count K v I = 0

Tactic:
simp only [hI, count_zero, Filter.eventually_cofinite, not_true_eq_false, setOf_false,
  finite_empty]

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : ¬I = 0
x✝ : HeightOneSpectrum R
⊢ count K x✝ I =
    ↑((Associates.mk x✝.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk x✝.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
rw [count_ne_zero K _ hI]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem powerBasis_gen_mem_adjoin_zeta_sub_one :
    (hζ.powerBasis K).gen ∈ adjoin K ({ζ - 1} : Set L)

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ (aeval (ζ - 1)) (X + 1) = ζ

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ ∃ x, (aeval (ζ - 1)) x = ζ

Tactic:
exact ⟨X + 1, by simp⟩

Result:
no goals

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ (IsPrimitiveRoot.powerBasis K hζ).gen ∈ adjoin K {ζ - 1}

Tactic:
rw [powerBasis_gen, adjoin_singleton_eq_range_aeval, AlgHom.mem_range]

Result:
n : ℕ+
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ ∃ x, (aeval (ζ - 1)) x = ζ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_ofList_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.getD_insertMany_empty_list_of_mem k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_log_b_mul_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < log (b i * n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < log (b i * ↑n)

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
h : Tendsto (fun n => log (b i * ↑n)) atTop atTop
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Tactic:
exact h.eventually_gt_atTop 0

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Tactic:
intro i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)

Tactic:
have h : Tendsto (fun (n : ℕ) => log (b i * n)) atTop atTop :=
  Tendsto.comp tendsto_log_atTop
    <| Tendsto.const_mul_atTop (b_pos R i) tendsto_natCast_atTop_atTop

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
h : Tendsto (fun n => log (b i * ↑n)) atTop atTop
⊢ ∀ᶠ (x : ℕ) in atTop, 0 < log (b i * ↑x)
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordCompl_mul (a b p : ℕ) : ordCompl[p] (a * b) = ordCompl[p] a * ordCompl[p] b

Proof state:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp only [ordProj_mul p ha hb]

Result:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / (p ^ a.factorization p * p ^ b.factorization p) = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Proof state:
a b p : ℕ
ha : ¬a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
if hb : b = 0 then simp [hb] else
simp only [ordProj_mul p ha hb]
rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Result:
no goals

Proof state:
a b p : ℕ
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
if ha : a = 0 then simp [ha] else
if hb : b = 0 then simp [hb] else
simp only [ordProj_mul p ha hb]
rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Result:
no goals

Proof state:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / (p ^ a.factorization p * p ^ b.factorization p) = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

Result:
no goals

Proof state:
a b p : ℕ
ha : a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp [ha]

Result:
no goals

Proof state:
a b p : ℕ
ha : ¬a = 0
hb : b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_bsup_le_lift {o : Ordinal} {f : ∀ a < o, Ordinal} (H : ∀ i h, f i h < bsup.{u, v} o f) :
    cof (bsup.{u, v} o f) ≤ Cardinal.lift.{v, u} o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
exact cof_blsub_le_lift.{u, v} f

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [H]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma of_id_fst : IsPullback (𝟙 _) f f (𝟙 _) := IsPullback.of_horiz_isIso ⟨by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tanh_ofReal_im (x : ℝ) : (tanh x).im = 0

Proof state:
x : ℝ
⊢ (tanh ↑x).im = 0

Tactic:
rw [← ofReal_tanh_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSimpleModule_iff_toSpanSingleton_surjective : IsSimpleModule R M ↔
    Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (LinearMap.toSpanSingleton R M x) :=
  ⟨fun h ↦ ⟨h.nontrivial, fun _ ↦ h.toSpanSingleton_surjective⟩, fun ⟨_, h⟩ ↦
    ⟨fun m ↦ or_iff_not_imp_left.mpr fun ne_bot ↦
      have ⟨x, hxm, hx0⟩ := m.ne_bot_iff.mp ne_bot
      top_unique <| fun z _ ↦ by obtain ⟨y, rfl⟩ := h x hx0 z; exact m.smul_mem _ hxm⟩⟩

Proof state:
case intro
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
left✝ : Nontrivial M
h : ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
y : R
x✝ : (LinearMap.toSpanSingleton R M x) y ∈ ⊤
⊢ (LinearMap.toSpanSingleton R M x) y ∈ m

Tactic:
exact m.smul_mem _ hxm

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
left✝ : Nontrivial M
h : ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
z : M
x✝ : z ∈ ⊤
⊢ z ∈ m

Tactic:
obtain ⟨y, rfl⟩ := h x hx0 z

Result:
case intro
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
left✝ : Nontrivial M
h : ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
m : Submodule R M
ne_bot : ¬m = ⊥
x : M
hxm : x ∈ m
hx0 : x ≠ 0
y : R
x✝ : (LinearMap.toSpanSingleton R M x) y ∈ ⊤
⊢ (LinearMap.toSpanSingleton R M x) y ∈ m
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem W.mk_dest (p : W P) : W.mk (W.dest p) = p

Proof state:
P : PFunctor.{u}
p : P.W
⊢ mk p.dest = p

Tactic:
cases p

Result:
case mk
P : PFunctor.{u}
a✝ : P.A
f✝ : P.B a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝

Proof state:
case mk
P : PFunctor.{u}
a✝ : P.A
f✝ : P.B a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_top_coe (a : ℝ) :
    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, a)

Proof state:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 + a.2

Tactic:
refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
  (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_

Result:
a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Proof state:
a : ℝ
⊢ ContinuousAt (fun p => p.1 + p.2) (⊤, ↑a)

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]

Result:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 + a.2

Proof state:
a r : ℝ
x✝ : EReal × EReal
h : ↑(r - (a - 1)) < x✝.1 ∧ ↑(a - 1) < x✝.2
⊢ ↑r < x✝.1 + x✝.2

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Result:
no goals