harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsRightRegular.of_mul (ab : IsRightRegular (b * a)) : IsRightRegular b

Proof state:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b

Tactic:
refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))

Result:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)

Proof state:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)

Tactic:
rw [← mul_assoc, ← mul_assoc]

Result:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * b * a = y * b * a
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfcHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(spectrum R a, R)} :
    0 ≤ cfcHom ha f ↔ 0 ≤ f

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.626029) [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
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ 0 ≤ (cfcHom ha) f ↔ 0 ≤ f

Tactic:
constructor

Result:
case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.626029) [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
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ 0 ≤ (cfcHom ha) f → 0 ≤ f

case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.626029) [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
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ 0 ≤ f → 0 ≤ (cfcHom ha) f

Proof state:
case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.626029) [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
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ 0 ≤ (cfcHom ha) f → 0 ≤ f

Tactic:
exact fun hf x ↦ (cfcHom_map_spectrum ha (R := R) _ ▸ spectrum_nonneg_of_nonneg hf) ⟨x, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_pow (x : 𝕎 R) (m : ℕ) : truncateFun n (x ^ m) = truncateFun n x ^ m

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
m : ℕ
⊢ truncateFun n (x ^ m) = truncateFun n x ^ m

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_left_inj (a b c : BitVec w) : (a + c == b + c) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a + c == b + c) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (a + c == b + c) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b c : BitVec w
⊢ (a + c == b + c) = true ↔ (a == b) = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod_eq_add_emod_left {m n k : Int} (i : Int)
    (H : m % n = k % n) : (i + m) % n = (i + k) % n

Proof state:
m n k i : Int
H : m % n = k % n
⊢ (i + m) % n = (i + k) % n

Tactic:
rw [Int.add_comm, add_emod_eq_add_emod_right _ H, Int.add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_reverse [Monad m] (l : Array α) (f : β → α → m β) (b) :
    l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
⊢ foldlM f b l.reverse = foldrM (fun x y => f y x) b l

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem map_inl_inv_coprodComparison [IsIso (coprodComparison F A B)] :
    F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
  | 0 => rfl
  | n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]

Proof state:
n : Nat
⊢ iota (n + 1) = (range' 1 (n + 1)).reverse

Tactic:
simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma single₀_map_f_zero {A B : V} (f : A ⟶ B) :
    ((single₀ V).map f).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B).inv =
    f

Tactic:
dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]

Result:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Tactic:
rw [comp_id, id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ ((single₀ V).map f).f 0 = f

Tactic:
rw [HomologicalComplex.single_map_f_self]

Result:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B).inv =
    f
-- Mathlib/RingTheory/KrullDimension/Basic.lean
theorem ringKrullDim_le_of_surjective (f : R →+* S) (hf : Function.Surjective f) :
    ringKrullDim S ≤ ringKrullDim R :=
  krullDim_le_of_strictMono (fun I ↦ ⟨Ideal.comap f I.asIdeal, inferInstance⟩)
    (Monotone.strictMono_of_injective (fun _ _ hab ↦ Ideal.comap_mono hab)
      (fun _ _ h => PrimeSpectrum.ext_iff.mpr <| Ideal.comap_injective_of_surjective f hf <| by
        simpa using h))

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
x✝¹ x✝ : PrimeSpectrum S
h : { asIdeal := Ideal.comap f x✝¹.asIdeal, isPrime := ⋯ } = { asIdeal := Ideal.comap f x✝.asIdeal, isPrime := ⋯ }
⊢ Ideal.comap f x✝¹.asIdeal = Ideal.comap f x✝.asIdeal

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
⊢ span K ↑(span ℤ (Set.range ⇑b)) = ⊤

Tactic:
simp [span_span_of_tower]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_edist_comm (f g : WithLp p (α × β)) : edist f g = edist g f

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
⊢ edist f g = edist g f

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Result:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp 0 (α × β)
⊢ edist f g = edist g f

case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp ⊤ (α × β)
⊢ edist f g = edist g f

case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Proof state:
case inr.inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp p (α × β)
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_add h, edist_comm]

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp 0 (α × β)
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_card, edist_comm]

Result:
no goals

Proof state:
case inr.inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : WithLp ⊤ (α × β)
⊢ edist f g = edist g f

Tactic:
simp only [prod_edist_eq_sup, edist_comm]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map₂_map_left (f₁ : γ → β → ζ) (f₂ : α → γ) :
    map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_const [IsProbabilityMeasure μ] (c : ℝ) : cgf (fun _ => c) μ t = t * c

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsProbabilityMeasure μ
c : ℝ
⊢ cgf (fun x => c) μ t = t * c

Tactic:
simp only [cgf, mgf_const, log_exp]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem abs_neg : ∀ x : EReal, (-x).abs = x.abs
  | ⊤ => rfl
  | ⊥ => rfl
  | (x : ℝ) => by rw [abs_def, ← coe_neg, abs_def, abs_neg]

Proof state:
x : ℝ
⊢ (-↑x).abs = (↑x).abs

Tactic:
rw [abs_def, ← coe_neg, abs_def, abs_neg]

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel_prod_left' {f : β × α → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun y => ∫⁻ x, f (x, y) ∂κ y

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β × α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun y => ∫⁻ (x : β), f (x, y) ∂κ y

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] protected lemma lt_mul_iff_one_lt_right (ha : 0 < a) : a < a * b ↔ 1 < b

Proof state:
a b : ℕ
ha : 0 < a
⊢ a < a * b ↔ 1 < b

Tactic:
simpa using Nat.mul_lt_mul_left (b := 1) ha

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem exists_mem_nhds_isClosed_subset {x : X} {s : Set X} (h : s ∈ 𝓝 x) :
    ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

Tactic:
have h' := (regularSpace_TFAE X).out 0 3

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s

Tactic:
exact h'.mp ‹_› _ _ h

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_one_apply (h : UniqueDiffWithinAt 𝕜 s x) (m : Fin 1 → E) :
    iteratedFDerivWithin 𝕜 1 f s x m = fderivWithin 𝕜 f s x (m 0)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ (iteratedFDerivWithin 𝕜 1 f s x) m = (fderivWithin 𝕜 f s x) (m 0)

Tactic:
simp only [iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_comp,
  (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_fderivWithin h]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ (((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          (fderivWithin 𝕜 f s x))
        (m 0))
      (tail m) =
    (fderivWithin 𝕜 f s x) (m 0)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : UniqueDiffWithinAt 𝕜 s x
m : Fin 1 → E
⊢ (((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
                continuous_invFun := ⋯ }).comp
          (fderivWithin 𝕜 f s x))
        (m 0))
      (tail m) =
    (fderivWithin 𝕜 f s x) (m 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- Variant of `of_isLimit` for an arbitrary cone on a diagram `WalkingCospan ⥤ C`. -/
lemma of_isLimit_cone {D : WalkingCospan ⥤ C} {c : Cone D} (hc : IsLimit c) :
    IsPullback (c.π.app .left) (c.π.app .right) (D.map WalkingCospan.Hom.inl)
      (D.map WalkingCospan.Hom.inr) where
  w

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingCospan ⥤ C
c : Cone D
hc : IsLimit c
⊢ c.π.app WalkingCospan.left ≫ D.map WalkingCospan.Hom.inl = c.π.app WalkingCospan.right ≫ D.map WalkingCospan.Hom.inr

Tactic:
simp_rw [Cone.w]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem range_natCast : range ((↑) : ℕ → Cardinal) = Iio ℵ₀ :=
  ext fun x => by simp only [mem_Iio, mem_range, eq_comm, lt_aleph0]

Proof state:
x : Cardinal.{u_1}
⊢ x ∈ range Nat.cast ↔ x ∈ Iio ℵ₀

Tactic:
simp only [mem_Iio, mem_range, eq_comm, lt_aleph0]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_ofReal_cpow_eventually_eq_atTop (c : ℂ) :
    (fun t : ℝ ↦ ‖(t : ℂ) ^ c‖) =ᶠ[atTop] fun t ↦ t ^ c.re

Proof state:
case h
c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖↑t ^ c‖ = t ^ c.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ht]

Result:
no goals

Proof state:
c : ℂ
⊢ (fun t => ‖↑t ^ c‖) =ᶠ[atTop] fun t => t ^ c.re

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖↑t ^ c‖ = t ^ c.re
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_factorial_le_div_pred {p : ℕ} (hp : p.Prime) (n : ℕ) :
    emultiplicity p n ! ≤ (n / (p - 1) : ℕ)

Proof state:
case a
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)

Tactic:
exact Nat.geom_sum_Ico_le hp.two_le _ _

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ emultiplicity p n ! ≤ ↑(n / (p - 1))

Tactic:
rw [hp.emultiplicity_factorial (lt_succ_self _)]

Result:
p : ℕ
hp : Prime p
n : ℕ
⊢ ↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) ≤ ↑(n / (p - 1))

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ ↑(∑ i ∈ Ico 1 (log p n).succ, n / p ^ i) ≤ ↑(n / (p - 1))

Tactic:
apply WithTop.coe_mono

Result:
case a
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)
-- Mathlib/Data/Vector/Defs.lean
theorem toList_drop {n m : ℕ} (v : Vector α m) : toList (drop n v) = List.drop n (toList v)

Proof state:
α : Type u_1
n m : ℕ
v : Vector α m
⊢ (drop n v).toList = List.drop n v.toList

Tactic:
cases v

Result:
case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (drop n ⟨val✝, property✝⟩).toList = List.drop n (toList ⟨val✝, property✝⟩)

Proof state:
case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (drop n ⟨val✝, property✝⟩).toList = List.drop n (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ Tendsto (fun x => (f x, f b)) (𝓝 b) (𝓤 α)

Tactic:
rw [ContinuousAt, tendsto_nhds_left]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem card_rootSet_eq_natDegree [Algebra F K] {p : F[X]} (hsep : p.Separable)
    (hsplit : Splits (algebraMap F K) p) : Fintype.card (p.rootSet K) = p.natDegree

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (algebraMap F K) p
⊢ Fintype.card ↑(p.rootSet K) = p.natDegree

Tactic:
classical
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← natDegree_eq_card_roots hsplit]

Result:
no goals

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (algebraMap F K) p
⊢ #(p.aroots K).toFinset = p.natDegree

Tactic:
rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← natDegree_eq_card_roots hsplit]

Result:
no goals

Proof state:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (algebraMap F K) p
⊢ Fintype.card ↑(p.rootSet K) = p.natDegree

Tactic:
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Result:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (algebraMap F K) p
⊢ #(p.aroots K).toFinset = p.natDegree
-- Mathlib/GroupTheory/Abelianization.lean
theorem commutator_eq_normalClosure : commutator G = Subgroup.normalClosure (commutatorSet G)

Proof state:
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.normalClosure (commutatorSet G)

Tactic:
simp [commutator, Subgroup.commutator_def', commutatorSet]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_eq_Icc' (x y : 𝕜) : [x -[𝕜] y] = Icc (min x y) (max x y)

Proof state:
case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : y ≤ x
⊢ [x-[𝕜]y] = Icc (x ⊓ y) (x ⊔ y)

Tactic:
rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x ≤ y
⊢ [x-[𝕜]y] = Icc (x ⊓ y) (x ⊔ y)

Tactic:
rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
⊢ [x-[𝕜]y] = Icc (x ⊓ y) (x ⊔ y)

Tactic:
rcases le_total x y with h | h

Result:
case inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x ≤ y
⊢ [x-[𝕜]y] = Icc (x ⊓ y) (x ⊔ y)

case inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : y ≤ x
⊢ [x-[𝕜]y] = Icc (x ⊓ y) (x ⊔ y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·)

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ range' a b

Tactic:
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm

Result:
no goals

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ map (fun x => a + x) (range b)

Tactic:
rw [← range'_eq_map_range]

Result:
a b : Nat
⊢ range (a + b) = range a ++ range' a b
-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_opens : IsTopologicalBasis { U : Set α | IsOpen U } :=
  isTopologicalBasis_of_isOpen_of_nhds (by tauto) (by tauto)

Proof state:
α : Type u
t : TopologicalSpace α
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ {U | IsOpen U}, a ∈ v ∧ v ⊆ u

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
⊢ ∀ u ∈ {U | IsOpen U}, IsOpen u

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem mul_inv_cancel_left (a : αˣ) (b : α) : (a : α) * (↑a⁻¹ * b) = b

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ ↑a * (↑a⁻¹ * b) = b

Tactic:
rw [← mul_assoc, mul_inv, one_mul]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_pow {ea₁ b c₁ : ℕ} {xa₁ : R}
    (_ : ea₁ * b = c₁) (_ : a₂ ^ b = c₂) : (xa₁ ^ ea₁ * a₂ : R) ^ b = xa₁ ^ c₁ * c₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₂ c₂ : R
ea₁ b c₁ : ℕ
xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b

Tactic:
simp [_root_.mul_pow, pow_mul]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Function.Injective.wbtw_map_iff {x y z : P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
h : Wbtw R (f x) (f y) (f z)
⊢ Wbtw R x y z

Tactic:
rwa [Wbtw, ← affineSegment_image, hf.mem_set_image] at h

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
refine ⟨fun h => ?_, fun h => h.map _⟩

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
h : Wbtw R (f x) (f y) (f z)
⊢ Wbtw R x y z
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma _root_.MeasurableEquiv.gaussianReal_map_symm_apply (hv : v ≠ 0) (f : ℝ ≃ᵐ ℝ) {f' : ℝ → ℝ}
    (h_deriv : ∀ x, HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) :
    (gaussianReal μ v).map f.symm s
      = ENNReal.ofReal (∫ x in s, |f' x| * gaussianPDFReal μ v (f x))

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
exact f.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' hs h_deriv
  (ae_of_all _ (gaussianPDFReal_nonneg _ _)) (integrable_gaussianPDFReal _ _)

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, gaussianPDF_def]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
f : ℝ ≃ᵐ ℝ
f' : ℝ → ℝ
h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
s : Set ℝ
hs : MeasurableSet s
⊢ (Measure.map (⇑f.symm) (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))