harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
@[to_additive (attr := simp)]
lemma finprod_apply {α ι : Type*} {f : ι → α → N} (hf : (mulSupport f).Finite) (a : α) :
    (∏ᶠ i, f i) a = ∏ᶠ i, f i a

Proof state:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
⊢ (mulSupport fun i => f i a) ⊆ mulSupport f

Tactic:
aesop

Result:
no goals

Proof state:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
hf' : (mulSupport fun i => f i a).Finite
⊢ ∏ c ∈ ⋯.toFinset, f c a = ∏ c ∈ ⋯.toFinset, f c a

Tactic:
apply Finset.prod_subset <;> aesop

Result:
no goals

Proof state:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
have hf' : (mulSupport fun i ↦ f i a).Finite := hf.subset (by aesop)

Result:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
hf' : (mulSupport fun i => f i a).Finite
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Proof state:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
classical
have hf' : (mulSupport fun i ↦ f i a).Finite := hf.subset (by aesop)
simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
symm
apply Finset.prod_subset <;> aesop

Result:
no goals

Proof state:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
hf' : (mulSupport fun i => f i a).Finite
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]

Result:
N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : (mulSupport f).Finite
a : α
hf' : (mulSupport fun i => f i a).Finite
⊢ ∏ c ∈ ⋯.toFinset, f c a = ∏ c ∈ ⋯.toFinset, f c a
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSum_ground_eq {h} : (M.disjointSum N h).E = M.E ∪ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ (M.disjointSum N h).E = M.E ∪ N.E

Tactic:
simp [disjointSum, restrictSubtype, mapEmbedding]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem ext {φ ψ : R⟦X⟧} (h : ∀ n, coeff R n φ = coeff R n ψ) : φ = ψ :=
  MvPowerSeries.ext fun n => by
    rw [← coeff_def]
    · apply h
    rfl

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ

Tactic:
rw [← coeff_def]

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ (coeff R ?m.6979) φ = (coeff R ?m.6979) ψ

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.6979

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ ℕ

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.6979

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ ℕ

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) φ = (coeff R n) ψ
n : Unit →₀ ℕ
⊢ (coeff R ?m.6979) φ = (coeff R ?m.6979) ψ

Tactic:
apply h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem MetricSpace.replaceUniformity_eq {γ} [U : UniformSpace γ] (m : MetricSpace γ)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m

Proof state:
case h.dist.h.h
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals

Proof state:
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
⊢ m.replaceUniformity H = m

Tactic:
ext

Result:
case h.dist.h.h
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
-- Mathlib/ModelTheory/Syntax.lean
theorem relabelAux_sumInl (k : ℕ) :
    relabelAux (Sum.inl : α → α ⊕ (Fin n)) k = Sum.map id (natAdd n)

Proof state:
case h.inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)

Tactic:
simp [relabelAux]

Result:
no goals

Proof state:
α : Type u'
n k : ℕ
⊢ relabelAux Sum.inl k = Sum.map id (natAdd n)

Tactic:
ext x

Result:
case h
α : Type u'
n k : ℕ
x : α ⊕ Fin k
⊢ relabelAux Sum.inl k x = Sum.map id (natAdd n) x
-- Mathlib/Topology/Sheaves/Presheaf.lean
@[ext]
lemma ext {X : TopCat} {P Q : Presheaf C X} {f g : P ⟶ Q}
    (w : ∀ U : Opens X, f.app (op U) = g.app (op U)) :
    f = g

Proof state:
case app.h.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : Opens ↑X
⊢ f.app (op U) = g.app (op U)

Tactic:
apply w

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
⊢ f = g

Tactic:
apply NatTrans.ext

Result:
case app
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
⊢ f.app = g.app

Proof state:
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : (Opens ↑X)ᵒᵖ
⊢ f.app U = g.app U

Tactic:
induction U with | _ U => ?_

Result:
case app.h.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : Opens ↑X
⊢ f.app (op U) = g.app (op U)

Proof state:
case app
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
⊢ f.app = g.app

Tactic:
ext U

Result:
case app.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : (Opens ↑X)ᵒᵖ
⊢ f.app U = g.app U
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_midpoint_left (p₁ p₂ : P) : dist (midpoint 𝕜 p₁ p₂) p₁ = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_left_midpoint]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem inf_principal {s t : Set α} : 𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t) :=
  le_antisymm
    (by simp only [le_principal_iff, mem_inf_iff]; exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩)
    (by simp [le_inf_iff, inter_subset_left, inter_subset_right])

Proof state:
α : Type u
s t : Set α
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)

Tactic:
simp only [le_principal_iff, mem_inf_iff]

Result:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Proof state:
α : Type u
s t : Set α
⊢ 𝓟 (s ∩ t) ≤ 𝓟 s ⊓ 𝓟 t

Tactic:
simp [le_inf_iff, inter_subset_left, inter_subset_right]

Result:
no goals

Proof state:
α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Tactic:
exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
lemma isNilpotent_C_mul_pow_X_of_isNilpotent (n : ℕ) (hnil : IsNilpotent r) :
    IsNilpotent ((C r) * X ^ n)

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r)

Tactic:
obtain ⟨m, hm⟩ := hnil

Result:
case intro
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (C r)

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r * X ^ n)

Tactic:
refine Commute.isNilpotent_mul_left (commute_X_pow _ _).symm ?_

Result:
R : Type u_1
r : R
inst✝ : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (C r)

Proof state:
case intro
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (C r)

Tactic:
refine ⟨m, ?_⟩

Result:
case intro
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ C r ^ m = 0

Proof state:
case intro
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ C r ^ m = 0

Tactic:
rw [← C_pow, hm, C_0]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@[reassoc]
lemma map₂_inv_hom_isIso {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] :
    F.map₂ (inv η) ≫ F.map₂ η = 𝟙 (F.map g)

Proof state:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) ≫ F.map₂ η = 𝟙 (F.map g)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {B : Set (Set X)}
    (hB : IsTopologicalBasis B) (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ s ∈ B) closure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
⊢ (𝓝 x).HasBasis (fun s => x ∈ s ∧ s ∈ B) closure

Tactic:
simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem continuous_iff_lower_upperSemicontinuous {f : α → γ} :
    Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f

Tactic:
simp_rw [continuous_iff_continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn,
  lowerSemicontinuousOn_univ_iff, upperSemicontinuousOn_univ_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b

Proof state:
case inl
a : Int
k : Nat
x✝ : a.natAbs ∣ (a * ↑k).natAbs
⊢ a ∣ a * ↑k

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
case inr
a : Int
k : Nat
x✝ : a.natAbs ∣ (-(a * ↑k)).natAbs
⊢ a ∣ -(a * ↑k)

Tactic:
rw [← Int.mul_neg]

Result:
case inr
a : Int
k : Nat
x✝ : a.natAbs ∣ (-(a * ↑k)).natAbs
⊢ a ∣ a * -↑k

Proof state:
a b : Int
x✝ : a.natAbs ∣ b.natAbs
k : Nat
hk : b.natAbs = a.natAbs * k
⊢ a ∣ b

Tactic:
rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk

Result:
a b : Int
x✝ : a.natAbs ∣ b.natAbs
k : Nat
hk : b = a * ↑k ∨ b = -(a * ↑k)
⊢ a ∣ b

Proof state:
a b : Int
x✝ : a.natAbs ∣ b.natAbs
k : Nat
hk : b = a * ↑k ∨ b = -(a * ↑k)
⊢ a ∣ b

Tactic:
cases hk <;> subst b

Result:
case inl
a : Int
k : Nat
x✝ : a.natAbs ∣ (a * ↑k).natAbs
⊢ a ∣ a * ↑k

case inr
a : Int
k : Nat
x✝ : a.natAbs ∣ (-(a * ↑k)).natAbs
⊢ a ∣ -(a * ↑k)

Proof state:
case inr
a : Int
k : Nat
x✝ : a.natAbs ∣ (-(a * ↑k)).natAbs
⊢ a ∣ a * -↑k

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
a b : Int
⊢ a.natAbs ∣ b.natAbs ↔ a ∣ b

Tactic:
refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩

Result:
a b : Int
x✝ : a.natAbs ∣ b.natAbs
k : Nat
hk : b.natAbs = a.natAbs * k
⊢ a ∣ b
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem mult_log_place_eq_zero {x : (𝓞 K)ˣ} {w : InfinitePlace K} :
    mult w * Real.log (w x) = 0 ↔ w x = 1

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ 0 < ↑w.mult

Tactic:
rw [mult]

Result:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ 0 < ↑(if w.IsReal then 1 else 2)

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = -1

Tactic:
linarith [(apply_nonneg _ _ : 0 ≤ w x)]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0

Tactic:
refine (ne_of_gt ?_)

Result:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ 0 < ↑w.mult

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ 0 < ↑(if w.IsReal then 1 else 2)

Tactic:
split_ifs <;> norm_num

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]

Result:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = -1

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬↑w.mult = 0

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬w ((algebraMap (𝓞 K) K) ↑x) = 0

Tactic:
simp only [ne_eq, map_eq_zero, coe_ne_zero x, not_false_eq_true]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem toReal_le_add' (hle : a ≤ b + c) (hb : b = ∞ → a = ∞) (hc : c = ∞ → a = ∞) :
    a.toReal ≤ b.toReal + c.toReal

Proof state:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ a.toReal ≤ b.toReal + c.toReal

Tactic:
refine le_trans (toReal_mono' hle ?_) toReal_add_le

Result:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ b + c = ⊤ → a = ⊤

Proof state:
a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ⊤ → a = ⊤
hc : c = ⊤ → a = ⊤
⊢ b + c = ⊤ → a = ⊤

Tactic:
simpa only [add_eq_top, or_imp] using And.intro hb hc

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
@[to_additive] lemma ThreeGPFree.eq_right (hs : ThreeGPFree s) :
    ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a * c = b * b → b = c

Proof state:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c

Tactic:
rintro a ha b hb c hc habc

Result:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : a * c = b * b
⊢ b = c

Proof state:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
c : α
hc : c ∈ s
hb : a ∈ s
habc : a * c = a * a
⊢ a = c

Tactic:
simpa using habc.symm

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : a * c = b * b
⊢ b = c

Tactic:
obtain rfl := hs ha hb hc habc

Result:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
hs : ThreeGPFree s
a : α
ha : a ∈ s
c : α
hc : c ∈ s
hb : a ∈ s
habc : a * c = a * a
⊢ a = c
-- Mathlib/NumberTheory/AbelSummation.lean
theorem sum_mul_eq_sub_integral_mul' (m : ℕ)
    (hf_diff : ∀ t ∈ Set.Icc (0 : ℝ) m, DifferentiableAt ℝ f t)
    (hf_int : IntegrableOn (deriv f) (Set.Icc (0 : ℝ) m)) :
    ∑ k ∈ Icc 0 m, f k * c k =
      f m * (∑ k ∈ Icc 0 m, c k) -
        ∫ t in Set.Ioc (0 : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Proof state:
case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ m = ⌊↑m⌋₊

Tactic:
rw [Nat.floor_natCast]

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ m = ⌊↑m⌋₊

Tactic:
all_goals rw [Nat.floor_natCast]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ ∑ k ∈ Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int

Result:
case h.e'_2.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ m = ⌊↑m⌋₊

case h.e'_3.h.e'_5.h.e'_6.h.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 0 ↑m) volume
⊢ m = ⌊↑m⌋₊
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (image2 f s t).image g = image2 f' (s.image g') t :=
  (image_image2_distrib h_distrib).trans <| by rw [image_id']

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ image2 f' (g' '' s) ((fun b => b) '' t) = image2 f' (g' '' s) t

Tactic:
rw [image_id']

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The cardinality of the fiber of a not-initial object is non-zero. -/
lemma non_zero_card_fiber_of_not_initial (X : C) (h : IsInitial X → False) :
    Nat.card (F.obj X) ≠ 0

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
⊢ Nat.card (F.obj X).carrier ≠ 0

Tactic:
intro hzero

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ False

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ IsEmpty (F.obj X).carrier

Tactic:
exact Finite.card_eq_zero_iff.mp hzero

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ Nonempty (IsInitial X)

Tactic:
rw [initial_iff_fiber_empty F]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ IsEmpty (F.obj X).carrier

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ False

Tactic:
refine Nonempty.elim ?_ h

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
hzero : Nat.card (F.obj X).carrier = 0
⊢ Nonempty (IsInitial X)
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem nnnorm_changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) :
    ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖p.changeOriginSeriesTerm k l s hs‖₊ = ‖p (k + l)‖₊

Tactic:
simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
lemma neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
  | 0 => Or.inl (pow_zero _)
  | n + 1 => (neg_one_pow_eq_or n).symm.imp
    (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
    (fun h ↦ by rw [pow_succ, h, one_mul])

Proof state:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1

Tactic:
rw [pow_succ, h, neg_one_mul, neg_neg]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1

Tactic:
rw [pow_succ, h, one_mul]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem SlashAction.neg_slash {β G α γ : Type*} [Group G] [AddGroup α] [SMul γ α]
    [SlashAction β G α γ] (k : β) (g : G) (a : α) : (-a) ∣[k;γ] g = -a ∣[k;γ] g :=
  eq_neg_of_add_eq_zero_left <| by
    rw [← SlashAction.add_slash, neg_add_cancel, SlashAction.zero_slash]

Proof state:
β : Type u_1
G : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup α
inst✝¹ : SMul γ α
inst✝ : SlashAction β G α γ
k : β
g : G
a : α
⊢ (-a) ∣[k;γ] g + a ∣[k;γ] g = 0

Tactic:
rw [← SlashAction.add_slash, neg_add_cancel, SlashAction.zero_slash]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_atTop_zpow_iff_pow [DivInvMonoid G] [TopologicalSpace G] {x y : G} :
    MapClusterPt x atTop (y ^ · : ℤ → G) ↔ MapClusterPt x atTop (y ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝¹ : DivInvMonoid G
inst✝ : TopologicalSpace G
x y : G
⊢ (MapClusterPt x atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x

Tactic:
simp_rw [MapClusterPt, ← Nat.map_cast_int_atTop, map_map, comp_def, zpow_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem regionBetween_subset (f g : α → ℝ) (s : Set α) : regionBetween f g s ⊆ s ×ˢ univ

Proof state:
α : Type u_1
f g : α → ℝ
s : Set α
⊢ regionBetween f g s ⊆ s ×ˢ univ

Tactic:
simpa only [prod_univ, regionBetween, Set.preimage, setOf_subset_setOf] using fun a => And.left

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Choose.lean
theorem isEquivalent_choose (k : ℕ) :
    (fun (n : ℕ) ↦ (n.choose k : ℝ)) ~[atTop] (fun (n : ℕ) ↦ (n^k / k.factorial : ℝ))

Proof state:
k : ℕ
⊢ (fun n => ↑(n.choose k)) ~[atTop] fun n => ↑n ^ k / ↑k !

Tactic:
conv_lhs =>
  intro n
  rw [choose_eq_descFactorial_div_factorial,
    cast_div (n.factorial_dvd_descFactorial k) (mod_cast k.factorial_ne_zero)]

Result:
k : ℕ
⊢ (fun n => ↑(n.descFactorial k) / ↑k !) ~[atTop] fun n => ↑n ^ k / ↑k !

Proof state:
k : ℕ
⊢ (fun n => ↑(n.descFactorial k) / ↑k !) ~[atTop] fun n => ↑n ^ k / ↑k !

Tactic:
exact (isEquivalent_descFactorial k).div IsEquivalent.refl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_one_add_col_mul_row {ι : Type*} [Unique ι] (u v : m → α) :
    det (1 + col ι u * row ι v) = 1 + v ⬝ᵥ u

Proof state:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 + col ι u * row ι v).det = 1 + v ⬝ᵥ u

Tactic:
rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
  Matrix.row_mul_col_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_neg : ∫ x in a..b, -f x ∂μ = -∫ x in a..b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ -∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ =
    -(∫ (x : ℝ) in Ioc a b, f x ∂μ - ∫ (x : ℝ) in Ioc b a, f x ∂μ)

Tactic:
abel

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ ∫ (x : ℝ) in a..b, -f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
simp only [intervalIntegral, integral_neg]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ -∫ (a : ℝ) in Ioc a b, f a ∂μ - -∫ (a : ℝ) in Ioc b a, f a ∂μ =
    -(∫ (x : ℝ) in Ioc a b, f x ∂μ - ∫ (x : ℝ) in Ioc b a, f x ∂μ)
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem spectral_theorem :
    A = (eigenvectorUnitary hA : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues)
      * (star (eigenvectorUnitary hA : Matrix n n 𝕜))

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary

Tactic:
rw [← star_mul_self_mul_eq_diagonal, mul_assoc, mul_assoc,
  (Matrix.mem_unitaryGroup_iff).mp (eigenvectorUnitary hA).2, mul_one,
  ← mul_assoc, (Matrix.mem_unitaryGroup_iff).mp (eigenvectorUnitary hA).2, one_mul]

Result:
no goals