harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma completedLFunction_eq (Φ : ZMod N → ℂ) (s : ℂ) :
    completedLFunction Φ s =
      completedLFunction₀ Φ s - N ^ (-s) * Φ 0 / s - N ^ (-s) * (∑ j, Φ j) / (1 - s)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
⊢ ↑N ^ (-s) * ∑ x : ZMod N, Φ x * completedHurwitzZetaEven₀ (toAddCircle x) s - ↑N ^ (-s) * (Φ 0 * s⁻¹) -
        ↑N ^ (-s) * ((∑ i : ZMod N, Φ i) * (1 - s)⁻¹) +
      ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s +
          ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s -
        ↑N ^ (-s) * (Φ 0 * s⁻¹) -
      ↑N ^ (-s) * ((∑ i : ZMod N, Φ i) * (1 - s)⁻¹)

Tactic:
abel

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
⊢ completedLFunction Φ s = completedLFunction₀ Φ s - ↑N ^ (-s) * Φ 0 / s - (↑N ^ (-s) * ∑ j : ZMod N, Φ j) / (1 - s)

Tactic:
simp only [completedLFunction, completedHurwitzZetaEven_eq, toAddCircle_eq_zero, div_eq_mul_inv,
  ite_mul, one_mul, zero_mul, mul_sub, mul_ite, mul_zero, sum_sub_distrib, Fintype.sum_ite_eq',
  ← sum_mul, completedLFunction₀, mul_assoc]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
⊢ ↑N ^ (-s) * ∑ x : ZMod N, Φ x * completedHurwitzZetaEven₀ (toAddCircle x) s - ↑N ^ (-s) * (Φ 0 * s⁻¹) -
        ↑N ^ (-s) * ((∑ i : ZMod N, Φ i) * (1 - s)⁻¹) +
      ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s +
          ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s -
        ↑N ^ (-s) * (Φ 0 * s⁻¹) -
      ↑N ^ (-s) * ((∑ i : ZMod N, Φ i) * (1 - s)⁻¹)
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Basis.ofZLatticeComap_repr_apply (e : F ≃ₗ[K] E) {ι : Type*} (b : Basis ι ℤ L) (x : L)
    (i : ι) :
    (b.ofZLatticeComap K L e).repr (ZLattice.comap_equiv K L e x) i = b.repr x i

Proof state:
K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
ι : Type u_4
b : Basis ι ℤ ↥L
x : ↥L
i : ι
⊢ ((ofZLatticeComap K L e b).repr ((ZLattice.comap_equiv K L e) x)) i = (b.repr x) i

Tactic:
simp [Basis.ofZLatticeComap]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_infty : ContDiffOn 𝕜 ∞ f s ↔ ∀ n : ℕ, ContDiffOn 𝕜 n f s :=
  contDiffOn_iff_forall_nat_le.trans <| by simp only [le_top, forall_prop_of_true]

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
⊢ (∀ (m : ℕ), ↑m ≤ ⊤ → ContDiffOn 𝕜 (↑m) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s

Tactic:
simp only [le_top, forall_prop_of_true]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive (attr := gcongr)]
lemma index_strictAnti (h : H < K) [H.FiniteIndex] : K.index < H.index

Proof state:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H

Tactic:
exact h.not_le

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
⊢ K.index < H.index

Tactic:
have h0 : K.index ≠ 0 := (finiteIndex_of_le h.le).finiteIndex

Result:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index < H.index

Proof state:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index < H.index

Tactic:
apply lt_of_le_of_ne (index_antitone h.le)

Result:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.index

Proof state:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ K.index ≠ H.index

Tactic:
rw [← relindex_mul_index h.le, Ne, eq_comm, mul_eq_right₀ h0, relindex_eq_one]

Result:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K ≤ H
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common vertices will agree with those of the original path `f`. In particular,
a vertex `i` with `i < j` can be identified with the same vertex in `f`. -/
lemma spine_δ_vertex_lt (f : Path X (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)}
    (h : i.castSucc < j) :
    (X.spine n (X.δ j (spineToSimplex f))).vertex i = f.vertex i.castSucc

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (X.spine n (SimplicialObject.δ X j (spineToSimplex f))).vertex i = f.vertex i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_vertex]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ X.map (⦋0⦌.const ⦋n⦌ i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.vertex i.castSucc

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ X.map (⦋0⦌.const ⦋n⦌ i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.vertex i.castSucc

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
  spineToSimplex_vertex]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.castSucc

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc

Tactic:
rw [Fin.succAbove_of_castSucc_lt j i h]

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex ((Hom.toOrderHom (SimplexCategory.δ j)) i) = f.vertex i.castSucc

Tactic:
simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
  OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ f.vertex (j.succAbove i) = f.vertex i.castSucc
-- Mathlib/Analysis/RCLike/Basic.lean
lemma nonneg_iff_exists_ofReal : 0 ≤ z ↔ ∃ x ≥ (0 : ℝ), x = z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z

Tactic:
simp_rw [nonneg_iff (K := K), ext_iff (K := K)]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ re z ∧ im z = 0 ↔ ∃ x ≥ 0, re ↑x = re z ∧ im ↑x = im z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ re z ∧ im z = 0 ↔ ∃ x ≥ 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem toFunLinear_mul_tmul_mul_aux_2 (k : ℕ) (a₁ a₂ : A) (p₁ p₂ : R[X]) :
    a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) =
      (Finset.antidiagonal k).sum fun x =>
        a₁ * (algebraMap R A) (coeff p₁ x.1) * (a₂ * (algebraMap R A) (coeff p₂ x.2))

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * (algebraMap R A) ((p₁ * p₂).coeff k)) =
    a₁ * (a₂ * ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1))

Tactic:
congr

Result:
case e_a.e_a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (algebraMap R A) ((p₁ * p₂).coeff k) =
    ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1)

Proof state:
case e_a.e_a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (algebraMap R A) ((p₁ * p₂).coeff k) =
    ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1)

Tactic:
simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, RingHom.map_mul]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) =
    ∑ x ∈ Finset.antidiagonal k, a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))

Tactic:
simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * (algebraMap R A) ((p₁ * p₂).coeff k)) =
    a₁ * (a₂ * ∑ i ∈ Finset.antidiagonal k, (algebraMap R A) (p₂.coeff i.2) * (algebraMap R A) (p₁.coeff i.1))
-- Mathlib/Data/Matrix/DoublyStochastic.lean
/-- The set of doubly stochastic matrices is convex. -/
lemma convex_doublyStochastic : Convex R (doublyStochastic R n : Set (Matrix n n R))

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
x : Matrix n n R
hx : x ∈ ↑(doublyStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(doublyStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(doublyStochastic R n)

Tactic:
simp only [SetLike.mem_coe, mem_doublyStochastic_iff_sum] at hx hy ⊢

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
x y : Matrix n n R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
hx : (∀ (i j : n), 0 ≤ x i j) ∧ (∀ (i : n), ∑ j : n, x i j = 1) ∧ ∀ (j : n), ∑ i : n, x i j = 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ (∀ (i : n), ∑ j : n, y i j = 1) ∧ ∀ (j : n), ∑ i : n, y i j = 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧
    (∀ (i : n), ∑ j : n, (a • x + b • y) i j = 1) ∧ ∀ (j : n), ∑ i : n, (a • x + b • y) i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
x y : Matrix n n R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
hx : (∀ (i j : n), 0 ≤ x i j) ∧ (∀ (i : n), ∑ j : n, x i j = 1) ∧ ∀ (j : n), ∑ i : n, x i j = 1
hy : (∀ (i j : n), 0 ≤ y i j) ∧ (∀ (i : n), ∑ j : n, y i j = 1) ∧ ∀ (j : n), ∑ i : n, y i j = 1
⊢ (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧
    (∀ (i : n), ∑ j : n, (a • x + b • y) i j = 1) ∧ ∀ (j : n), ∑ i : n, (a • x + b • y) i j = 1

Tactic:
simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
⊢ Convex R ↑(doublyStochastic R n)

Tactic:
intro x hx y hy a b ha hb h

Result:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
x : Matrix n n R
hx : x ∈ ↑(doublyStochastic R n)
y : Matrix n n R
hy : y ∈ ↑(doublyStochastic R n)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ ↑(doublyStochastic R n)
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasStrictFDerivAt_const (c : F) (x : E) :
    HasStrictFDerivAt (fun _ => c) (0 : E →L[𝕜] F) x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun _ => by
    simp only [zero_apply, sub_self, Pi.zero_apply]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
x : E
x✝ : E × E
⊢ 0 x✝ = c - c - 0 (x✝.1 - x✝.2)

Tactic:
simp only [zero_apply, sub_self, Pi.zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_congr {xs ys : List α} (w : xs = ys)
    (f : (i : Nat) → α → (h : i < xs.length) → β) :
    mapFinIdx xs f = mapFinIdx ys (fun i a h => f i a (by simp [w]; omega))

Proof state:
α : Type ?u.5942
β : Type ?u.5971
xs ys : List α
w : xs = ys
f : (i : Nat) → α → i < xs.length → β
i : Nat
a : α
h : i < ys.length
⊢ i < xs.length

Tactic:
simp [w]

Result:
α : Type ?u.5942
β : Type ?u.5971
xs ys : List α
w : xs = ys
f : (i : Nat) → α → i < xs.length → β
i : Nat
a : α
h : i < ys.length
⊢ i < ys.length

Proof state:
α : Type u_1
β : Type u_2
xs ys : List α
w : xs = ys
f : (i : Nat) → α → i < xs.length → β
⊢ xs.mapFinIdx f = ys.mapFinIdx fun i a h => f i a ⋯

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
xs : List α
f : (i : Nat) → α → i < xs.length → β
⊢ xs.mapFinIdx f = xs.mapFinIdx fun i a h => f i a ⋯

Proof state:
α : Type u_1
β : Type u_2
xs : List α
f : (i : Nat) → α → i < xs.length → β
⊢ xs.mapFinIdx f = xs.mapFinIdx fun i a h => f i a ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type ?u.5942
β : Type ?u.5971
xs ys : List α
w : xs = ys
f : (i : Nat) → α → i < xs.length → β
i : Nat
a : α
h : i < ys.length
⊢ i < ys.length

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
/-- The norm of a matrix is the sup of the sup of the nnnorm of the entries -/
lemma norm_eq_sup_sup_nnnorm (A : Matrix m n α) :
    ‖A‖ = Finset.sup Finset.univ fun i ↦ Finset.sup Finset.univ fun j ↦ ‖A i j‖₊

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖A‖ = ↑(Finset.univ.sup fun i => Finset.univ.sup fun j => ‖A i j‖₊)

Tactic:
simp_rw [Matrix.norm_def, Pi.norm_def, Pi.nnnorm_def]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f)
    (s : ι → Subgroup G) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem eq_true_eq (p : Prop) : (p = True) = p

Proof state:
p : Prop
⊢ (p = True) = p

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_getElem {l : Array α} {p : α → Prop} :
    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a

Proof state:
α : Type u_1
l : Array α
p : α → Prop
⊢ (∀ (i : Nat) (h : i < l.size), p l[i]) ↔ ∀ (a : α), a ∈ l → p a

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
⊢ (∀ (i : Nat) (h : i < { toList := toList✝ }.size), p { toList := toList✝ }[i]) ↔
    ∀ (a : α), a ∈ { toList := toList✝ } → p a

Proof state:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
⊢ (∀ (i : Nat) (h : i < { toList := toList✝ }.size), p { toList := toList✝ }[i]) ↔
    ∀ (a : α), a ∈ { toList := toList✝ } → p a

Tactic:
simp [List.forall_getElem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
    (h : containsKey k l = false) : insertEntry k v l = ⟨k, v⟩ :: l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ insertEntry k v l = ⟨k, v⟩ :: l

Tactic:
simp [insertEntry, h]

Result:
no goals
-- Mathlib/Probability/Independence/Integrable.lean
/-- If a nonzero function belongs to `ℒ^p` and is independent of another function, then
the space is a probability space. -/
lemma MemLp.isProbabilityMeasure_of_indepFun
    (f : Ω → E) (g : Ω → F) {p : ℝ≥0∞} (hp : p ≠ 0) (hp' : p ≠ ∞)
    (hℒp : MemLp f p μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : IndepFun f g μ) :
    IsProbabilityMeasure μ

Proof state:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
⊢ IsProbabilityMeasure μ

Tactic:
have := hindep.measure_inter_preimage_eq_mul {x | c ≤ ‖x‖₊} Set.univ
  (isClosed_le continuous_const continuous_nnnorm).measurableSet MeasurableSet.univ

Result:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
this : μ (f ⁻¹' {x | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) = μ (f ⁻¹' {x | c ≤ ‖x‖₊}) * μ (g ⁻¹' Set.univ)
⊢ IsProbabilityMeasure μ

Proof state:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
  ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Result:
case intro.intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Proof state:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
this : μ {a | c ≤ ‖f a‖₊} = μ {a | c ≤ ‖f a‖₊} * μ Set.univ
⊢ IsProbabilityMeasure μ

Tactic:
exact ⟨(ENNReal.mul_eq_left hc.ne' h'c.ne).1 this.symm⟩

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem dom_bool₂ (f : Bool → Bool → α) : Primrec₂ f :=
  (cond fst ((dom_bool (f true)).comp snd) ((dom_bool (f false)).comp snd)).of_eq fun ⟨a, b⟩ => by
    cases a <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : Bool → Bool → α
x✝ : Bool × Bool
a b : Bool
⊢ (bif (a, b).1 then f true (a, b).2 else f false (a, b).2) = f (a, b).1 (a, b).2

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_add_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
exact div_mul_cancel₀ _ hxy

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
by_cases hxy : ‖x + y‖ = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
simp [h'.1]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
rw [hxy, zero_mul, eq_comm,
  add_eq_zero_iff_of_nonneg (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_mul_rat_iff : Irrational (x * q) ↔ q ≠ 0 ∧ Irrational x

Proof state:
q : ℚ
x : ℝ
⊢ Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x

Tactic:
rw [mul_comm, irrational_rat_mul_iff]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.spectrum_algebraMap_eq [Nontrivial A] (r : R) :
    spectrum R (algebraMap R A r) = {r}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
r : R
⊢ spectrum R ((algebraMap R A) r) = {r}

Tactic:
have hp : p 0 := cfc_predicate_zero R

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
r : R
hp : p 0
⊢ spectrum R ((algebraMap R A) r) = {r}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
r : R
hp : p 0
⊢ spectrum R ((algebraMap R A) r) = {r}

Tactic:
rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
r : R
hp : p 0
⊢ (fun x => r) '' spectrum R 0 = {r}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : Nontrivial A
r : R
hp : p 0
⊢ (fun x => r) '' spectrum R 0 = {r}

Tactic:
exact Set.Nonempty.image_const (⟨0, spectrum.zero_mem (R := R) not_isUnit_zero⟩) _

Result:
no goals