harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ)
    (l : Array α) (init : γ) (w : start = (l.filterMap f).size) :
    (l.filterMap f).foldrM g init start 0 =
      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
init : γ
toList✝ : List α
⊢ List.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init toList✝ =
    List.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init toList✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
l : Array α
init : γ
w : start = (filterMap f l).size
⊢ foldrM g init (filterMap f l) start =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
l : Array α
init : γ
⊢ foldrM g init (filterMap f l) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
l : Array α
init : γ
⊢ foldrM g init (filterMap f l) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
init : γ
toList✝ : List α
⊢ foldrM g init (filterMap f { toList := toList✝ }) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init { toList := toList✝ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
init : γ
toList✝ : List α
⊢ foldrM g init (filterMap f { toList := toList✝ }) =
    foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init { toList := toList✝ }

Tactic:
simp [List.foldrM_filterMap]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : β → γ → m γ
init : γ
toList✝ : List α
⊢ List.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init toList✝ =
    List.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init toList✝
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
@[simp, norm_cast]
lemma val_sum {ι : Type*} (s : Finset ι) (f : ι → AdicCompletion I M) :
    (∑ i ∈ s, f i).val = ∑ i ∈ s, (f i).val

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
⊢ ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

Tactic:
simp_rw [← funext (incl_apply _ _ _), map_sum]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Abelian.lean
lemma kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage :
    (kernel.ι S.g ≫ cokernel.π S.f) ≫ S.cokernelToAbelianCoimage = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (kernel.ι S.g ≫ cokernel.π S.f) ≫ S.cokernelToAbelianCoimage = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a

Proof state:
a b : Int
⊢ a % b + a / b * b = a

Tactic:
rw [Int.mul_comm]

Result:
a b : Int
⊢ a % b + b * (a / b) = a

Proof state:
a b : Int
⊢ a % b + b * (a / b) = a

Tactic:
exact emod_add_ediv ..

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem mulHead_head {i j : ι} (w : NeWord M i j) (x : M i) (hnotone : x * w.head ≠ 1) :
    (mulHead w x hnotone).head = x * w.head

Proof state:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (_w₁✝.mulHead x hnotone).head = x * _w₁✝.head
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (_w₂✝.mulHead x hnotone).head = x * _w₂✝.head
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ ((_w₁✝.append _hne✝ _w₂✝).mulHead x hnotone).head = x * (_w₁✝.append _hne✝ _w₂✝).head

Tactic:
simp [*, mulHead]

Result:
no goals

Proof state:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ ((singleton x✝ a✝).mulHead x hnotone).head = x * (singleton x✝ a✝).head

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head ≠ 1
⊢ (w.mulHead x hnotone).head = x * w.head

Tactic:
induction w

Result:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ ((singleton x✝ a✝).mulHead x hnotone).head = x * (singleton x✝ a✝).head

case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (_w₁✝.mulHead x hnotone).head = x * _w₁✝.head
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (_w₂✝.mulHead x hnotone).head = x * _w₂✝.head
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ ((_w₁✝.append _hne✝ _w₂✝).mulHead x hnotone).head = x * (_w₁✝.append _hne✝ _w₂✝).head
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_eq_zero_iff_forall : exponent G = 0 ↔ ∀ n > 0, ∃ g : G, g ^ n ≠ 1

Proof state:
G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
rw [exponent_eq_zero_iff, ExponentExists]

Result:
G : Type u
inst✝ : Monoid G
⊢ (¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Proof state:
G : Type u
inst✝ : Monoid G
⊢ (∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
⊢ (¬∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
push_neg

Result:
G : Type u
inst✝ : Monoid G
⊢ (∀ (n : ℕ), 0 < n → ∃ g, g ^ n ≠ 1) ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
-- Mathlib/Order/FixedPoints.lean
theorem lfp_eq_sSup_iterate (h : ωScottContinuous f) :
    f.lfp = ⨆ n, f^[n] ⊥

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f = ⨆ n, (⇑f)^[n] ⊥

Tactic:
apply le_antisymm

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

Tactic:
apply lfp_le_fixed

Result:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ f (⨆ n, (⇑f)^[n] ⊥) = ⨆ n, (⇑f)^[n] ⊥

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Tactic:
apply le_lfp

Result:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ∀ (b : α), f b ≤ b → ⨆ n, (⇑f)^[n] ⊥ ≤ b

Proof state:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ f (⨆ n, (⇑f)^[n] ⊥) = ⨆ n, (⇑f)^[n] ⊥

Tactic:
exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
  ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)

Result:
no goals

Proof state:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ∀ (b : α), f b ≤ b → ⨆ n, (⇑f)^[n] ⊥ ≤ b

Tactic:
intro a h_a

Result:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
h_a : f a ≤ a
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ a

Proof state:
case a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
h_a : f a ≤ a
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem natDegree_nodal [Nontrivial R] : (nodal s v).natDegree = #s

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ (nodal s v).natDegree = #s

Tactic:
simp_rw [nodal, natDegree_prod_of_monic (h := fun i _ => monic_X_sub_C (v i)),
  natDegree_X_sub_C, sum_const, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length) :
    (l.drop n).take 1 = [l.get ⟨n, h⟩]

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get ⟨n, h⟩]

Tactic:
rw [drop_eq_getElem_cons h, take, take]

Result:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get ⟨n, h⟩]

Tactic:
rw [drop_eq_getElem_cons h, take, take]

Result:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ [l[n]] = [l.get ⟨n, h⟩]

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_at_apply {S : Type*} [Semiring S] (f : R →+* S) (r : R) :
    p.eval₂ f (f r) = f (p.eval r)

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = ∑ x ∈ p.support, f (p.coeff x * r ^ x)

Tactic:
simp only [f.map_mul, f.map_pow]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ eval₂ f (f r) p = f (eval r p)

Tactic:
rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]

Result:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = ∑ x ∈ p.support, f (p.coeff x * r ^ x)
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.apply_ne (hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a ∈ s) :
    f a ≠ a

Proof state:
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
⊢ f a ≠ a

Tactic:
obtain ⟨b, hb, hba⟩ := hs.exists_ne a

Result:
case intro.intro
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ f a ≠ a

Proof state:
case intro.intro
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ f a ≠ a

Tactic:
obtain ⟨n, rfl⟩ := hf.2 ha hb

Result:
case intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
hba : (f ^ n) a ≠ a
⊢ f a ≠ a

Proof state:
case intro.intro.intro
α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
hba : (f ^ n) a ≠ a
⊢ f a ≠ a

Tactic:
exact fun h => hba (IsFixedPt.perm_zpow h n)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Defs.lean
theorem one_le_mul_self_iff : 1 ≤ a * a ↔ 1 ≤ a :=
  ⟨(fun h ↦ by push_neg at h ⊢; exact mul_lt_one' h h).mtr, fun h ↦ one_le_mul h h⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : ¬1 ≤ a
⊢ ¬1 ≤ a * a

Tactic:
push_neg at h ⊢

Result:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : a < 1
⊢ a * a < 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
h : a < 1
⊢ a * a < 1

Tactic:
exact mul_lt_one' h h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
@[simp] lemma mk_setProd {α β : Type u} (s : Set α) (t : Set β) : #(s ×ˢ t) = #s * #t

Proof state:
α β : Type u
s : Set α
t : Set β
⊢ #↑(s ×ˢ t) = #↑s * #↑t

Tactic:
rw [mul_def, mk_congr (Equiv.Set.prod ..)]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem ae_null_of_comp_null (h : (η ∘ₖ κ) a s = 0) : (η · s) =ᵐ[κ a] 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
⊢ (fun x => (η x) s) =ᶠ[ae (κ a)] 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : ((η ∘ₖ κ) a) t = 0
⊢ (fun x => (η x) s) =ᶠ[ae (κ a)] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : ((η ∘ₖ κ) a) t = 0
⊢ (fun x => (η x) s) =ᶠ[ae (κ a)] 0

Tactic:
simp_rw [comp_null a mt] at ht

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y => (η y) t) =ᶠ[ae (κ a)] 0
⊢ (fun x => (η x) s) =ᶠ[ae (κ a)] 0

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y => (η y) t) =ᶠ[ae (κ a)] 0
⊢ (fun x => (η x) s) =ᶠ[ae (κ a)] 0

Tactic:
rw [Filter.eventuallyLE_antisymm_iff]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y => (η y) t) =ᶠ[ae (κ a)] 0
⊢ (fun x => (η x) s) ≤ᶠ[ae (κ a)] 0 ∧ 0 ≤ᶠ[ae (κ a)] fun x => (η x) s

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
s : Set γ
h : ((η ∘ₖ κ) a) s = 0
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht : (fun y => (η y) t) =ᶠ[ae (κ a)] 0
⊢ (fun x => (η x) s) ≤ᶠ[ae (κ a)] 0 ∧ 0 ≤ᶠ[ae (κ a)] fun x => (η x) s

Tactic:
exact ⟨Filter.EventuallyLE.trans_eq (ae_of_all _ fun _ ↦ measure_mono hst) ht,
  ae_of_all _ fun _ ↦ zero_le _⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_one (R : Type*) [Ring R] : cyclotomic 1 R = X - 1

Proof state:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)

Tactic:
simp only [map_X, Polynomial.map_one, Polynomial.map_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 1 R = X - 1

Tactic:
have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
  simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]

Result:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ

Tactic:
simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1

Tactic:
symm

Result:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R

Proof state:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R

Tactic:
rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]

Result:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_sub_of_lt {x y : BitVec w} (h : x < y) :
    (x - y).toNat = 2^w - (y.toNat - x.toNat)

Proof state:
w : Nat
x y : BitVec w
h : x < y
⊢ 2 ^ w - y.toNat + x.toNat = 2 ^ w - (y.toNat - x.toNat)

Tactic:
bv_omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x < y
⊢ (x - y).toNat = 2 ^ w - (y.toNat - x.toNat)

Tactic:
simp only [toNat_sub]

Result:
w : Nat
x y : BitVec w
h : x < y
⊢ (2 ^ w - y.toNat + x.toNat) % 2 ^ w = 2 ^ w - (y.toNat - x.toNat)

Proof state:
w : Nat
x y : BitVec w
h : x < y
⊢ 2 ^ w - y.toNat + x.toNat < 2 ^ w

Tactic:
bv_omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x < y
⊢ (2 ^ w - y.toNat + x.toNat) % 2 ^ w = 2 ^ w - (y.toNat - x.toNat)

Tactic:
rw [Nat.mod_eq_of_lt (by bv_omega)]

Result:
w : Nat
x y : BitVec w
h : x < y
⊢ 2 ^ w - y.toNat + x.toNat = 2 ^ w - (y.toNat - x.toNat)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_zipIdx_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = l.zipIdx.attach.map
      fun ⟨⟨x, i⟩, m⟩ =>
        f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1)

Proof state:
α : Type ?u.31255
β : Type ?u.31277
l : List α
f : (i : Nat) → α → i < l.length → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : (x, i) ∈ l.zipIdx
⊢ i < l.length

Tactic:
rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m

Result:
α : Type ?u.31255
β : Type ?u.31277
l : List α
f : (i : Nat) → α → i < l.length → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : ∃ h, l[i] = x
⊢ i < l.length

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f =
    map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      l.zipIdx.attach

Tactic:
apply ext_getElem <;> simp

Result:
no goals

Proof state:
α : Type ?u.31255
β : Type ?u.31277
l : List α
f : (i : Nat) → α → i < l.length → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : ∃ h, l[i] = x
⊢ i < l.length

Tactic:
exact m.1

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma isPresentation_mk
    (h₁ : Submodule.span A (Set.range solution.var) = ⊤)
    (h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)) :
    solution.IsPresentation

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ solution.IsPresentation

Tactic:
rw [isPresentation_iff]

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧
    LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧
    LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
constructor <;> assumption

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullbackIsoProdSubtype_hom_snd (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd _ _

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g

Tactic:
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_snd]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma isLoop_iff_forall_not_mem_isBase (he : e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Tactic:
simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_diff, and_iff_right he]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem mkArray [BEq α] [Hashable α] {c : Nat} : IsHashSelf
    (mkArray c (AssocList.nil : AssocList α β)) :=
  ⟨by simp⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ ∀ (i : Nat) (h : i < (Array.mkArray c AssocList.nil).size),
    HashesTo (Array.mkArray c AssocList.nil)[i].toList i (Array.mkArray c AssocList.nil).size

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_mul_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    uniformBell m n * n ! ^ m * m ! = (m * n)!

Proof state:
case h.e'_2.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

Tactic:
simp only [toFinset_replicate]

Result:
case h.e'_2.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ x ∈ (if m = 0 then ∅ else {n}).erase 0, (count x (replicate m n))!

Proof state:
case h.e'_3.h.e'_1
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Tactic:
simp

Result:
no goals

Proof state:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ m ! = ∏ x ∈ ∅.erase 0, (count x (replicate m n))!

Tactic:
rw [hm, factorial_zero, eq_comm]

Result:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))! = 1

Proof state:
case h.e'_2.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ x ∈ (if m = 0 then ∅ else {n}).erase 0, (count x (replicate m n))!

Tactic:
split_ifs with hm

Result:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ m ! = ∏ x ∈ ∅.erase 0, (count x (replicate m n))!

case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}.erase 0, (count x (replicate m n))!

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}.erase 0, (count x (replicate m n))!

Tactic:
rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]

Result:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}, (count x (replicate m n))!

Proof state:
m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!

Tactic:
convert bell_mul_eq (replicate m n)

Result:
case h.e'_2.h.e'_5.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = (map (fun j => j !) (replicate m n)).prod

case h.e'_2.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

case h.e'_3.h.e'_1
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Proof state:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}, (count x (replicate m n))!

Tactic:
simp only [Finset.prod_singleton, count_replicate_self]

Result:
no goals

Proof state:
case h.e'_2.h.e'_5.h.e'_6
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = (map (fun j => j !) (replicate m n)).prod

Tactic:
simp only [map_replicate, prod_replicate]

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ {n}.erase 0 = {n}

Tactic:
simp [Ne.symm hn]

Result:
no goals

Proof state:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ ∏ x ∈ ∅.erase 0, (count x (replicate 0 n))! = 1

Tactic:
rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl,  Finset.prod_empty]

Result:
no goals