harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the arithmetic function `ζ` and of the Möbius function are inverses. -/
lemma LSeries_zeta_mul_Lseries_moebius {s : ℂ} (hs : 1 < s.re) : L ↗ζ s * L ↗μ s = 1

Proof state:
s : ℂ
hs : 1 < s.re
⊢ L ((fun x => ↑(ζ x)) ⍟ fun n => ↑(μ n)) s = 1

Tactic:
simp [← natCoe_apply, ← intCoe_apply, coe_mul, one_eq_delta, LSeries_delta, -zeta_apply]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(ζ n)) s * L (fun n => ↑(μ n)) s = 1

Tactic:
rw [← LSeries_convolution' (LSeriesSummable_zeta_iff.mpr hs)
  (LSeriesSummable_moebius_iff.mpr hs)]

Result:
s : ℂ
hs : 1 < s.re
⊢ L ((fun x => ↑(ζ x)) ⍟ fun n => ↑(μ n)) s = 1
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem disjoint_powers_iff_not_mem (y : R) (hI : I.IsRadical) :
    Disjoint (Submonoid.powers y : Set R) ↑I ↔ y ∉ I.1

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I.toAddSubmonoid
⊢ ↑(Submonoid.powers y) ⊓ ↑I ≤ ⊥

Tactic:
rintro x ⟨⟨n, rfl⟩, hx'⟩

Result:
case intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I.toAddSubmonoid
n : ℕ
hx' : (fun x => y ^ x) n ∈ ↑I
⊢ (fun x => y ^ x) n ∈ ⊥

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
⊢ Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid

Tactic:
refine ⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _),
    fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I.toAddSubmonoid
⊢ ↑(Submonoid.powers y) ⊓ ↑I ≤ ⊥

Proof state:
case intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I.toAddSubmonoid
n : ℕ
hx' : (fun x => y ^ x) n ∈ ↑I
⊢ (fun x => y ^ x) n ∈ ⊥

Tactic:
exact h (hI <| mem_radical_of_pow_mem <| le_radical hx')

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciInf_lt_iff [Nonempty ι] {f : ι → α} (hb : BddBelow (range f)) :
    iInf f < a ↔ ∃ i, f i < a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddBelow (range f)
⊢ iInf f < a ↔ ∃ i, f i < a

Tactic:
simpa only [mem_range, exists_exists_eq_and] using csInf_lt_iff hb (range_nonempty _)

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k ! * (n - k)! ∣ n !

Proof state:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Result:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Proof state:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
exact Nat.dvd_mul_left _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem sinh_log {x : ℝ} (hx : 0 < x) : sinh (log x) = (x - x⁻¹) / 2

Proof state:
x : ℝ
hx : 0 < x
⊢ sinh (log x) = (x - x⁻¹) / 2

Tactic:
rw [sinh_eq, exp_neg, exp_log hx]

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem pos_of_div_pos {n : ℕ+} {a : ℕ} (h : a ∣ n) : 0 < a

Proof state:
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a

Tactic:
apply pos_iff_ne_zero.2

Result:
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0

Proof state:
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False

Tactic:
exact PNat.ne_zero n (eq_zero_of_zero_dvd h)

Result:
no goals

Proof state:
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0

Tactic:
intro hzero

Result:
n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False

Proof state:
n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False

Tactic:
rw [hzero] at h

Result:
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
-- Mathlib/Analysis/Quaternion.lean
theorem continuous_normSq : Continuous (normSq : ℍ → ℝ)

Proof state:
⊢ Continuous ⇑normSq

Tactic:
simpa [← normSq_eq_norm_mul_self] using
  (continuous_norm.mul continuous_norm : Continuous fun q : ℍ => ‖q‖ * ‖q‖)

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparating_proj_preimage {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) :
    IsSeparating ((proj S T).obj ⁻¹' 𝒢)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left

Tactic:
exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsSeparating ((proj S T).obj ⁻¹' 𝒢)

Tactic:
refine fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => ?_)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_mul_of_isRegular_right {f g : MvPolynomial σ R}
    (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) :
    m.degree (f * g) = m.degree f + m.degree g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_iff_forall_lintegral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ≥0,
        Tendsto (fun i ↦ ∫⁻ x, f x ∂(μs i : Measure Ω)) F (𝓝 (∫⁻ x, f x ∂(μ : Measure Ω)))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))

Tactic:
simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
  ENNReal.toNNReal_coe]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))

Tactic:
rw [tendsto_iff_forall_toWeakDualBCNN_tendsto]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem fst_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (fst R B C).comp (prod f g) = f

Proof state:
R : Type u
inst✝⁶ : Monoid R
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableOn_finCons :
    DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x)) s ↔
      DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) s ∧
      ∀ (i : Fin n), DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) s) ↔
    DifferentiableOn 𝕜 φ s ∧ ∀ (i : Fin n), DifferentiableOn 𝕜 (fun x => φs x i) s

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s

Tactic:
rw [differentiableOn_pi, Fin.forall_fin_succ, differentiableOn_pi]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) s ∧
      ∀ (i : Fin n), DifferentiableOn 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) s) ↔
    DifferentiableOn 𝕜 φ s ∧ ∀ (i : Fin n), DifferentiableOn 𝕜 (fun x => φs x i) s
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_conj : sin (conj x) = conj (sin x)

Proof state:
x : ℂ
⊢ sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sin x)

Tactic:
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← RingHom.map_mul, ← RingHom.map_mul,
  sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
@[simp] lemma coord_smul (a : G) (b : AffineBasis ι k V) (i : ι) :
    (a • b).coord i = (b.coord i).comp (DistribMulAction.toLinearEquiv _ _ a).symm.toAffineMap

Proof state:
case h
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
v : V
⊢ ((a • b).coord i) v = ((b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap) v

Tactic:
simp [map_sub, coord]

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).coord i = (b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap

Tactic:
ext v

Result:
case h
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
v : V
⊢ ((a • b).coord i) v = ((b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap) v
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) :
    map (MonoidHom.id G) (φ ≫ ψ) n =
      map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ map (MonoidHom.id G) (φ ≫ ψ) n = map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0

Proof state:
⊢ 2 * ↑π * I ≠ 0

Tactic:
norm_num [Real.pi_ne_zero, I_ne_zero]

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem process_zero : process s 0 = 0

Proof state:
Ω : Type u_1
s : ℕ → Set Ω
⊢ process s 0 = 0

Tactic:
rw [process, Finset.range_zero, Finset.sum_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_insert_of_not_mem {l : List α} (h : a ∉ l) :
    length (l.insert a) = length l + 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ (a :: l).length = l.length + 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ (List.insert a l).length = l.length + 1

Tactic:
rw [insert_of_not_mem h]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ (a :: l).length = l.length + 1
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma infs_self : s ⊼ s = s ↔ InfClosed (s : Set α)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeInf α
s : Finset α
⊢ s ⊼ s = s ↔ InfClosed ↑s

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/Algebra/Homology/HasNoLoop.lean
lemma exists_distinct_prev_or :
    (∃ (k : ι), c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬ c.Rel j k

Proof state:
case pos
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ∃ k, c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
obtain ⟨k, hk⟩ := h

Result:
case pos.intro
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j k : ι
hk : c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Proof state:
case neg
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ k, c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
exact Or.inr (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
by_cases h : ∃ (k : ι), c.Rel j k

Result:
case pos
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ∃ k, c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

case neg
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ k, c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Proof state:
case pos.intro
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j k : ι
hk : c.Rel j k
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
exact Or.inl ⟨k, hk, fun hjk ↦ c.not_rel_of_eq hjk hk⟩

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
h : ¬∃ k, c.Rel j k
⊢ ∀ (k : ι), ¬c.Rel j k

Tactic:
simpa using h

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_range_iff_exists_fun :
    x ∈ span R (range v) ↔ ∃ c : α → R, ∑ i, c i • v i = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i : α, Finsupp.equivFunOnFinite x_1 i • v i = x

Tactic:
simp only [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply]

Result:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ (∃ c, (c.sum fun i a => a • v i) = x) ↔ ∃ x_1, ∑ x : α, x_1 x • v x = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ (∃ c, (c.sum fun i a => a • v i) = x) ↔ ∃ x_1, ∑ x : α, x_1 x • v x = x

Tactic:
exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ c, ∑ i : α, c i • v i = x

Tactic:
rw [Finsupp.equivFunOnFinite.surjective.exists]

Result:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i : α, Finsupp.equivFunOnFinite x_1 i • v i = x
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem norm_integral_le_of_le_const {c : ℝ}
    (hc : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ c) (μ : Measure ℝⁿ) [IsLocallyFiniteMeasure μ] :
    ‖(integral I l f μ.toBoxAdditive.toSMul : E)‖ ≤ (μ I).toReal * c

Proof state:
ι : Type u
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
c : ℝ
hc : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ c
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ (μ ↑I).toReal * c

Tactic:
simpa only [integral_const] using norm_integral_le_of_norm_le hc μ (integrable_const c)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_coe_pi : (2 : ℤ) • (π : Angle) = 0

Proof state:
⊢ 2 • ↑π = 0

Tactic:
simp [← intCast_mul_eq_zsmul]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
/-- The group of group homomorphisms from a finite cyclic group `G` of order `n` into another
group `G'` is (noncanonically) isomorphic to the group of `n`th roots of unity in `G'`. -/
lemma monoidHom_mulEquiv_rootsOfUnity (G : Type*) [CommGroup G] [IsCyclic G]
    (G' : Type*) [CommGroup G'] :
    Nonempty <| (G →* G') ≃* rootsOfUnity (Nat.card G) G'

Proof state:
case intro
G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
exact ⟨monoidHomMulEquivRootsOfUnityOfGenerator hg G'⟩

Result:
no goals

Proof state:
G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Result:
case intro
G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_true  : ∀(b : Bool), (b != true)  = !b

Proof state:
⊢ ∀ (b : Bool), (b != true) = !b

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Flat.lean
lemma isCofiltered_of_representablyFlat [IsCofiltered D] [RepresentablyFlat F] :
    IsCofiltered C

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsCofiltered D
inst✝ : RepresentablyFlat F
this : IsFiltered Cᵒᵖ
⊢ IsCofiltered C

Tactic:
exact isCofiltered_of_isFiltered_op C

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsCofiltered D
inst✝ : RepresentablyFlat F
⊢ IsCofiltered C

Tactic:
have := isFiltered_of_representablyCoflat F.op

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsCofiltered D
inst✝ : RepresentablyFlat F
this : IsFiltered Cᵒᵖ
⊢ IsCofiltered C
-- Mathlib/Computability/DFA.lean
theorem eval_reindex (g : σ ≃ σ') (x : List α) : (reindex g M).eval x = g (M.eval x)

Proof state:
α : Type u
σ : Type v
M : DFA α σ
σ' : Type u_2
g : σ ≃ σ'
x : List α
⊢ ((reindex g) M).eval x = g (M.eval x)

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
b : β
⊢ b ∈ pmap f l H ↔ ∃ a h, f a ⋯ = b

Tactic:
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.rotateL_lemma₂ {a b c : ℕ} (H3 : 2 * (b + c) ≤ 9 * a + 3) (h : b < 2 * c) :
    b < 3 * a + 1

Proof state:
a b c : ℕ
H3 : 2 * (b + c) ≤ 9 * a + 3
h : b < 2 * c
⊢ b < 3 * a + 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_append (xs ys : Array α) (k : Nat) :
    zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.size)

Proof state:
case mk.mk
α : Type u_1
k : Nat
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).zipIdx k =
    { toList := toList✝¹ }.zipIdx k ++ { toList := toList✝ }.zipIdx (k + { toList := toList✝¹ }.size)

Tactic:
simp [List.zipIdx_append]

Result:
no goals

Proof state:
α : Type u_1
xs ys : Array α
k : Nat
⊢ (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + xs.size)

Tactic:
cases xs

Result:
case mk
α : Type u_1
ys : Array α
k : Nat
toList✝ : List α
⊢ ({ toList := toList✝ } ++ ys).zipIdx k = { toList := toList✝ }.zipIdx k ++ ys.zipIdx (k + { toList := toList✝ }.size)

Proof state:
case mk
α : Type u_1
ys : Array α
k : Nat
toList✝ : List α
⊢ ({ toList := toList✝ } ++ ys).zipIdx k = { toList := toList✝ }.zipIdx k ++ ys.zipIdx (k + { toList := toList✝ }.size)

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
k : Nat
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ } ++ { toList := toList✝ }).zipIdx k =
    { toList := toList✝¹ }.zipIdx k ++ { toList := toList✝ }.zipIdx (k + { toList := toList✝¹ }.size)
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem mem_rootsOfUnity_prime_pow_mul_iff (p k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} :
    ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ∈ rootsOfUnity (p ^ k * m) R ↔ ζ ∈ rootsOfUnity m R

Tactic:
simp only [mem_rootsOfUnity', ExpChar.pow_prime_pow_mul_eq_one_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pushout.mapLift_comp {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T) (i' : S' ⟶ S)
    [HasPushout f g] [HasPushout (i ≫ f) (i ≫ g)] [HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)]
    [HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)] :
    pushout.mapLift f g (i' ≫ i) =
      (pushout.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom ≫
        pushout.mapLift _ _ i' ≫ pushout.mapLift f g i

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y S T S' : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
i' : S' ⟶ S
inst✝³ : HasPushout f g
inst✝² : HasPushout (i ≫ f) (i ≫ g)
inst✝¹ : HasPushout (i' ≫ i ≫ f) (i' ≫ i ≫ g)
inst✝ : HasPushout ((i' ≫ i) ≫ f) ((i' ≫ i) ≫ g)
⊢ mapLift f g (i' ≫ i) = (congrHom ⋯ ⋯).hom ≫ mapLift (i ≫ f) (i ≫ g) i' ≫ mapLift f g i

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_zero_fun : cgf 0 μ t = log (μ Set.univ).toReal

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
⊢ cgf 0 μ t = log (μ Set.univ).toReal

Tactic:
simp only [cgf, mgf_zero_fun]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_top : a ∆ b = ⊤ ↔ IsCompl a b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ∆ b = ⊤ ↔ IsCompl a b

Tactic:
rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
  codisjoint_iff, and_comm]

Result:
no goals