harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/DomMulAct.lean
theorem stabilizer_ncard [Finite α] [Fintype ι] :
    Set.ncard {g : Perm α | f ∘ g = f} = ∏ i, (Set.ncard {a | f a = i})!

Proof state:
case intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
val✝ : Fintype α
⊢ {g | f ∘ ⇑g = f}.ncard = ∏ i : ι, {a | f a = i}.ncard !

Tactic:
simp only [← Set.Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]

Result:
case intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
val✝ : Fintype α
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ x : ι, (Fintype.card { a // f a = x })!

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
⊢ {g | f ∘ ⇑g = f}.ncard = ∏ i : ι, {a | f a = i}.ncard !

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
val✝ : Fintype α
⊢ {g | f ∘ ⇑g = f}.ncard = ∏ i : ι, {a | f a = i}.ncard !

Proof state:
case intro
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
val✝ : Fintype α
⊢ Fintype.card { g // f ∘ ⇑g = f } = ∏ x : ι, (Fintype.card { a // f a = x })!

Tactic:
exact stabilizer_card f

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝¹ : Finite α
inst✝ : Fintype ι
⊢ {g | f ∘ ⇑g = f}.ncard = ∏ i : ι, {a | f a = i}.ncard !

Tactic:
classical
cases nonempty_fintype α
simp only [← Set.Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
exact stabilizer_card f

Result:
no goals
-- Mathlib/RingTheory/EssentialFiniteness.lean
lemma EssFiniteType.algHom_ext [EssFiniteType R S]
    (f g : S →ₐ[R] T) (H : ∀ s ∈ finset R S, f s = g s) : f = g

Proof state:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S) = g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)

Tactic:
apply AlgHom.ext_of_adjoin_eq_top (s := { x | x.1 ∈ finset R S })

Result:
case h.h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ adjoin R {x | ↑x ∈ finset R S} = ⊤

case h.hs
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ Set.EqOn ⇑(f.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S))
    ⇑(g.comp (IsScalarTower.toAlgHom R (↥(subalgebra R S)) S)) {x | ↑x ∈ finset R S}
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t_fst_fst (i j : 𝒰.J) : t 𝒰 f g i j ≫ pullback.fst _ _ ≫ pullback.fst _ _ =
    pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j : 𝒰.J
⊢ t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.fst (𝒰.map j ≫ f) g =
    pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_fst,
  pullback.lift_fst_assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_inv_fst_fst,
  pullbackSymmetry_hom_comp_fst]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem norm_sub_le_of_mem_A {r x : ℝ} (hr : 0 < r) (ε : ℝ) {L₁ L₂ : F} (h₁ : x ∈ A f L₁ r ε)
    (h₂ : x ∈ A f L₂ r ε) : ‖L₁ - L₂‖ ≤ 4 * ε

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r

Tactic:
apply add_le_add

Result:
case h₁
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r

case h₂
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r

Proof state:
case h₂
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r

Tactic:
apply le_of_mem_A h₁ <;> simp [(half_pos hr).le]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ε * r + ε * r = r / 2 * (4 * ε)

Tactic:
ring

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖(r / 2) • (L₁ - L₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖

Tactic:
simp [smul_sub]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 4 * ε

Tactic:
rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_left (half_pos hr)] at H

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ε

Tactic:
suffices H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε) by
  rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_left (half_pos hr)] at H

Result:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)

Proof state:
case h₁
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r

Tactic:
apply le_of_mem_A h₂ <;> simp [(half_pos hr).le]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_def' :
    ∀ {b : ℕ} (_ : 1 < b) {n : ℕ} (_ : 0 < n), digits b n = (n % b) :: digits b (n / b)
  | 0, h => absurd h (by decide)
  | 1, h => absurd h (by decide)
  | b + 2, _ => digitsAux_def _ (by simp) _

Proof state:
n✝ : ℕ
h : 1 < 1
⊢ ¬1 < 1

Tactic:
decide

Result:
no goals

Proof state:
n✝ : ℕ
h : 1 < 0
⊢ ¬1 < 0

Tactic:
decide

Result:
no goals

Proof state:
n✝ b : ℕ
x✝ : 1 < b + 2
⊢ 2 ≤ b + 2

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_vsub_const_eq_affineCombination_vsub (w : ι → k) (p₁ : ι → P) (p₂ : P)
    (h : ∑ i ∈ s, w i = 1) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.affineCombination k p₁ w -ᵥ p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i ∈ s, w i = 1
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁) w -ᵥ p₂

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem equivPair_head {i : ι} {w : Word M} :
    (equivPair i w).head =
      if h : ∃ (h : w.toList ≠ []), (w.toList.head h).1 = i
      then h.snd ▸ (w.toList.head h.1).2
      else 1

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ ((equivPair i) w).head = if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1

Tactic:
simp only [equivPair, equivPairAux]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ ({
          toFun := fun w =>
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x =>
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w).head =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1

Proof state:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i head : ι
m✝ : M head
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some head
h2✝ : m✝ ≠ 1
a✝ :
  ({
          toFun := fun w =>
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x =>
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w✝).head =
    if h : ∃ (h : w✝.toList ≠ []), (w✝.toList.head h).fst = i then ⋯ ▸ (w✝.toList.head ⋯).snd else 1
hi : ¬i = head
⊢ ({
          toFun := fun w =>
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x =>
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        (cons m✝ w✝ h1✝ h2✝)).head =
    if h : ∃ (h : (cons m✝ w✝ h1✝ h2✝).toList ≠ []), ((cons m✝ w✝ h1✝ h2✝).toList.head h).fst = i then
      ⋯ ▸ ((cons m✝ w✝ h1✝ h2✝).toList.head ⋯).snd
    else 1

Tactic:
simp [hi, Ne.symm hi]

Result:
no goals

Proof state:
case h_empty
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
⊢ ({
          toFun := fun w =>
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x =>
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        empty).head =
    if h : ∃ (h : empty.toList ≠ []), (empty.toList.head h).fst = i then ⋯ ▸ (empty.toList.head ⋯).snd else 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem set_drop {l : List α} {n m : Nat} {a : α} :
    (l.drop n).set m a = (l.set (n + m) a).drop n

Proof state:
α : Type u_1
l : List α
n m : Nat
a : α
⊢ (drop n l).set m a = drop n (l.set (n + m) a)

Tactic:
rw [drop_set, if_neg, add_sub_self_left n m]

Result:
case hnc
α : Type u_1
l : List α
n m : Nat
a : α
⊢ ¬n + m < n

Proof state:
case hnc
α : Type u_1
l : List α
n m : Nat
a : α
⊢ ¬n + m < n

Tactic:
exact (Nat.not_lt).2 (le_add_right n m)

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictMono.mem_lowerBounds_image (hf : StrictMono f) :
    f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s :=  by simp [lowerBounds, hf.le_iff_le]

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ lowerBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [lowerBounds, hf.le_iff_le]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem hasSum_zeta_nat {k : ℕ} (hk : k ≠ 0) :
    HasSum (fun n : ℕ => 1 / (n : ℝ) ^ (2 * k))
      ((-1 : ℝ) ^ (k + 1) * (2 : ℝ) ^ (2 * k - 1) * π ^ (2 * k) *
        bernoulli (2 * k) / (2 * k)!)

Proof state:
case h.e'_5
k : ℕ
hk : k ≠ 0
⊢ (fun n => 1 / ↑n ^ (2 * k)) = fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

Tactic:
ext1 n

Result:
case h.e'_5.h
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

Proof state:
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 ^ 1 = 2 ^ (2 * k)

Tactic:
rw [← pow_add, Nat.sub_add_cancel]

Result:
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k

Proof state:
k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k

Tactic:
omega

Result:
no goals

Proof state:
k : ℕ
hk : k ≠ 0
⊢ HasSum (fun n => 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)

Tactic:
convert hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one) using 1

Result:
case h.e'_5
k : ℕ
hk : k ≠ 0
⊢ (fun n => 1 / ↑n ^ (2 * k)) = fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))

Proof state:
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2

Tactic:
rw [eq_div_iff (two_ne_zero' ℝ)]

Result:
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 = 2 ^ (2 * k)

Proof state:
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * (2 ^ (2 * k) / 2) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 ^ (2 * k) * π ^ (2 * k)) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_5.h
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

Tactic:
rw [mul_zero, Real.cos_zero, mul_one]

Result:
no goals

Proof state:
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))

Tactic:
rw [this, mul_pow]

Result:
case h.e'_6
k : ℕ
hk : k ≠ 0
this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2
⊢ (-1) ^ (k + 1) * (2 ^ (2 * k) / 2) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 ^ (2 * k) * π ^ (2 * k)) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))

Proof state:
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]

Result:
case h.e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
lemma prod_nonneg {s : Multiset R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 0 ≤ a
⊢ 0 ≤ prod ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, prod_coe] at *

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ a✝, 0 ≤ a
⊢ 0 ≤ a✝.prod

Proof state:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : Multiset R
h : ∀ a ∈ s, 0 ≤ a
⊢ 0 ≤ s.prod

Tactic:
cases s using Quotient.ind

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 0 ≤ a
⊢ 0 ≤ prod ⟦a✝⟧

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ a✝, 0 ≤ a
⊢ 0 ≤ a✝.prod

Tactic:
apply List.prod_nonneg h

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem map_id_apply (x : FreeAbelianGroup α) : map id x = x

Proof state:
α : Type u
x : FreeAbelianGroup α
⊢ (map id) x = x

Tactic:
rw [map_id]

Result:
α : Type u
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α)) x = x

Proof state:
α : Type u
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α)) x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem Injective.image_injective (hf : Injective f) : Injective (image f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
intro s t h

Result:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t

Tactic:
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
/-- If `β - qα ... β ... β + rα` is the `α`-chain through `β`, then
  `β (coroot α) = q - r`. In particular, it is an integer. -/
lemma apply_coroot_eq_cast :
    β (coroot α) = (chainBotCoeff α β - chainTopCoeff α β : ℤ)

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) =
    ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))

Tactic:
congr 1

Result:
case e_a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β) =
    ↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)

Proof state:
case e_a
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β) =
    ↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β)

Tactic:
omega

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ β (coroot α) = ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))

Tactic:
rw [apply_coroot_eq_cast', ← chainTopCoeff_add_chainBotCoeff]

Result:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ ↑(↑(chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β) - 2 * ↑(chainTopCoeff (⇑α) β)) =
    ↑(↑(chainBotCoeff (⇑α) β) - ↑(chainTopCoeff (⇑α) β))
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem skewAdjointLieSubalgebraEquiv_apply
    (f : skewAdjointLieSubalgebra (B.compl₁₂ (Qₗ := N) (Qₗ' := N) ↑e ↑e)) :
    ↑(skewAdjointLieSubalgebraEquiv B e f) = e.lieConj f

Proof state:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : BilinForm R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : N ≃ₗ[R] M
f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B ↑e ↑e))
⊢ ↑((skewAdjointLieSubalgebraEquiv B e) f) = e.lieConj ↑f

Tactic:
simp [skewAdjointLieSubalgebraEquiv]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
@[to_additive]
lemma finprod_option {f : Option α → M} (hf : (mulSupport (f ∘ some)).Finite) :
    ∏ᶠ o, f o = f none * ∏ᶠ a, f (some a)

Proof state:
case h.e'_3.h.e'_6
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective some

Tactic:
exact Option.some_injective _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport (f ∘ some)).Finite
⊢ (mulSupport f).Finite

Tactic:
simpa [finite_option]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport (f ∘ some)).Finite
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
replace hf : (mulSupport f).Finite := by simpa [finite_option]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (o : Option α), f o = f none * ∏ᶠ (a : α), f (some a)

Tactic:
convert finprod_mem_insert' f (show none ∉ Set.range Option.some by aesop)
  (hf.subset inter_subset_right)

Result:
case h.e'_2.h.e'_4.h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x✝ : Option α
⊢ f x✝ = ∏ᶠ (_ : x✝ ∈ insert none (range some)), f x✝

case h.e'_3.h.e'_6
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Proof state:
case h.e'_2.h.e'_4.h
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x✝ : Option α
⊢ f x✝ = ∏ᶠ (_ : x✝ ∈ insert none (range some)), f x✝

Tactic:
aesop

Result:
no goals

Proof state:
case h.e'_3.h.e'_6
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
rw [finprod_mem_range]

Result:
case h.e'_3.h.e'_6
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ Injective some

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ none ∉ range some

Tactic:
aesop

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_eval_rev {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ b₂ a₂}
    (aa : tr a₁ a₂) (ab : b₂ ∈ eval f₂ a₂) : ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ eval f₁ a₁

Proof state:
case intro.intro.intro.intro.intro.refl.some
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
this :
  match some d₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
hfc : f₁ c₁ = some d₁
⊢ some d₁ = none

Tactic:
rcases this with ⟨d₂, _, bd⟩

Result:
case intro.intro.intro.intro.intro.refl.some.intro.intro
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
d₁ : σ₁
hfc : f₁ c₁ = some d₁
d₂ : σ₂
left✝ : tr d₁ d₂
bd : Reaches₁ f₂ b₂ d₂
⊢ some d₁ = none

Proof state:
case intro.intro.intro.intro.intro.refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
⊢ f₁ c₁ = none

Tactic:
have := H cc

Result:
case intro.intro.intro.intro.intro.refl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
b₂ a₂ : σ₂
aa : tr a₁ a₂
ab✝ : b₂ ∈ eval f₂ a₂
ab : Reaches f₂ a₂ b₂
b0 : f₂ b₂ = none
c₁ : σ₁
ac : Reaches f₁ a₁ c₁
bc : Reaches f₂ b₂ b₂
cc : tr c₁ b₂
this :
  match f₁ c₁ with
  | some b₁ => ∃ b₂_1, tr b₁ b₂_1 ∧ Reaches₁ f₂ b₂ b₂_1
  | none => f₂ b₂ = none
⊢ f₁ c₁ = none