harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_prod (f : α → M) (hf : (mulSupport f).Finite) :
    ∏ᶠ i : α, f i = ∏ i ∈ hf.toFinset, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ hf.toFinset, f i

Tactic:
rw [finprod_def, dif_pos hf]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ hf.toFinset, f i

Tactic:
classical rw [finprod_def, dif_pos hf]

Result:
no goals
-- Mathlib/Analysis/Convex/AmpleSet.lean
theorem image {s : Set E} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) :
    AmpleSet (L '' s) := forall_mem_image.mpr fun x hx ↦
  calc (convexHull ℝ) (connectedComponentIn (L '' s) (L x))
    _ = (convexHull ℝ) (L '' (connectedComponentIn s x)) :=
          .symm <| congrArg _ <| L.toHomeomorph.image_connectedComponentIn hx
    _ = L '' (convexHull ℝ (connectedComponentIn s x)) :=
          .symm <| L.toAffineMap.image_convexHull _
    _ = univ

Proof state:
F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᵃL[ℝ] F
x : E
hx : x ∈ s
⊢ ⇑L '' (convexHull ℝ) (connectedComponentIn s x) = univ

Tactic:
rw [h x hx, image_univ, L.surjective.range_eq]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem riemannZeta_two_mul_nat {k : ℕ} (hk : k ≠ 0) :
    riemannZeta (2 * k) = (-1) ^ (k + 1) * (2 : ℂ) ^ (2 * k - 1)
      * (π : ℂ) ^ (2 * k) * bernoulli (2 * k) / (2 * k)!

Proof state:
case h.e'_2
k : ℕ
hk : k ≠ 0
⊢ ∑' (n : ℕ), 1 / ↑n ^ (2 * k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))

Tactic:
simp [push_cast]

Result:
no goals

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

Tactic:
convert congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq

Result:
case h.e'_2
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
norm_cast

Result:
no goals

Proof state:
case h.e'_2
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))

Tactic:
rw [← Nat.cast_two, ← Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one (by omega)]

Result:
case h.e'_2
k : ℕ
hk : k ≠ 0
⊢ ∑' (n : ℕ), 1 / ↑n ^ (2 * k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))
-- Mathlib/SetTheory/Surreal/Basic.lean
/-- A small set of surreals is bounded below. -/
lemma bddBelow_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddBelow s

Proof state:
s : Set Surreal
inst✝ : Small.{u, u + 1} ↑s
⊢ BddBelow s

Tactic:
simpa using bddBelow_range_of_small (Subtype.val : s → Surreal.{u})

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
lemma WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n < m

Proof state:
n : ℕ
m : WithBot ℕ∞
⊢ ↑n + 1 ≤ m ↔ ↑n < m

Tactic:
rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]

Result:
n : ℕ
m : WithBot ℕ∞
⊢ ↑↑(n + 1) ≤ m ↔ ↑n < m

Proof state:
case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

Tactic:
simp

Result:
no goals

Proof state:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝

Tactic:
rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
  ← WithBot.coe_lt_coe, WithBot.coe_natCast]

Result:
no goals

Proof state:
n : ℕ
m : WithBot ℕ∞
⊢ ↑↑(n + 1) ≤ m ↔ ↑n < m

Tactic:
cases m

Result:
case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem mem_prod_list_ofFn {a : α} {s : Fin n → Finset α} :
    a ∈ (List.ofFn s).prod ↔ ∃ f : ∀ i : Fin n, s i, (List.ofFn fun i => (f i : α)).prod = a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
rw [← mem_coe, coe_list_prod, List.map_ofFn, Set.mem_prod_list_ofFn]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, (List.ofFn fun i => ↑(f i)).prod = a) ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Finset α
⊢ (∃ f, (List.ofFn fun i => ↑(f i)).prod = a) ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem map_natCast_nonneg [AddMonoidWithOne α] [PartialOrder α]
    [AddLeftMono α] [ZeroLEOneClass α] : 0 ≤ n.map (Nat.cast : ℕ → α)

Proof state:
n : ℕ∞
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ 0 ≤ map Nat.cast n

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem EqOn.image_eq_self {f : α → α} (h : Set.EqOn f id s) : f '' s = s

Proof state:
α : Type u_1
s : Set α
f : α → α
h : EqOn f id s
⊢ f '' s = s

Tactic:
rw [h.image_eq, image_id]

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem desc {α β : Type*} (f : X → α) (g : α → β) (h : IsLocallyConstant (g ∘ f))
    (inj : Function.Injective g) : IsLocallyConstant f := fun s => by
  rw [← preimage_image_eq s inj, preimage_preimage]
  exact h (g '' s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))

Tactic:
exact h (g '' s)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen (f ⁻¹' s)

Tactic:
rw [← preimage_image_eq s inj, preimage_preimage]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
    (f : α → β → m β) (arr : Array α) (init : β) (i h) :
    (arr.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f arr 0 i h init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : 0 ≤ arr.size
⊢ List.foldlM (fun x y => f y x) init (List.take 0 arr.toList).reverse =
    if (0 == 0) = true then pure init
    else
      match 0, h with
      | 0, x => pure init
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i ⋯ __do_lift

Tactic:
simp [List.foldlM, List.take]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i✝ i : Nat
h : i + 1 ≤ arr.size
⊢ List.foldlM (fun x y => f y x) init (List.take (i + 1) arr.toList).reverse =
    if (i + 1 == 0) = true then pure init
    else
      match i + 1, h with
      | 0, x => pure init
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i ⋯ __do_lift

Tactic:
rw [← List.take_concat_get _ _ h]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i✝ i : Nat
h : i + 1 ≤ arr.size
⊢ List.foldlM (fun x y => f y x) init ((List.take i arr.toList).concat arr.toList[i]).reverse =
    if (i + 1 == 0) = true then pure init
    else
      match i + 1, h with
      | 0, x => pure init
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i ⋯ __do_lift

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : i ≤ arr.size
⊢ List.foldlM (fun x y => f y x) init (List.take i arr.toList).reverse = foldrM.fold f arr 0 i h init

Tactic:
unfold foldrM.fold

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
arr : Array α
init : β
i : Nat
h : i ≤ arr.size
⊢ List.foldlM (fun x y => f y x) init (List.take i arr.toList).reverse =
    if (i == 0) = true then pure init
    else
      match i, h with
      | 0, x => pure init
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f arr[i] init
        foldrM.fold f arr 0 i ⋯ __do_lift
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem mem_skewAdjointMatricesSubmodule :
    A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁

Tactic:
simp [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

Tactic:
erw [mem_pairSelfAdjointMatricesSubmodule]

Result:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ (-J).IsAdjointPair J A₁ A₁ ↔ J.IsSkewAdjoint A₁
-- Mathlib/CategoryTheory/Limits/FullSubcategory.lean
theorem closedUnderColimitsOfShape_of_colimit [P.IsClosedUnderIsomorphisms]
    (h : ∀ {F : J ⥤ C} [HasColimit F], (∀ j, P (F.obj j)) → P (colimit F)) :
    ClosedUnderColimitsOfShape J P

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasColimit F], (∀ (j : J), P (F.obj j)) → P (colimit F)
F : J ⥤ C
c : Cocone F
hc : IsColimit c
hF : ∀ (j : J), P (F.obj j)
this : HasColimit F
⊢ P c.pt

Tactic:
exact P.prop_of_iso ((colimit.isColimit _).coconePointUniqueUpToIso hc) (h hF)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasColimit F], (∀ (j : J), P (F.obj j)) → P (colimit F)
F : J ⥤ C
c : Cocone F
hc : IsColimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt

Tactic:
have : HasColimit F := ⟨_, hc⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasColimit F], (∀ (j : J), P (F.obj j)) → P (colimit F)
F : J ⥤ C
c : Cocone F
hc : IsColimit c
hF : ∀ (j : J), P (F.obj j)
this : HasColimit F
⊢ P c.pt

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasColimit F], (∀ (j : J), P (F.obj j)) → P (colimit F)
⊢ ClosedUnderColimitsOfShape J P

Tactic:
intros F c hc hF

Result:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{w', w} J
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
h : ∀ {F : J ⥤ C} [inst : HasColimit F], (∀ (j : J), P (F.obj j)) → P (colimit F)
F : J ⥤ C
c : Cocone F
hc : IsColimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem carry_width {x y : BitVec w} :
    carry w x y c = decide (x.toNat + y.toNat + c.toNat ≥ 2^w)

Proof state:
w : Nat
c : Bool
x y : BitVec w
⊢ carry w x y c = decide (x.toNat + y.toNat + c.toNat ≥ 2 ^ w)

Tactic:
simp [carry]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem smul_re (a : ℤ) (b : ℤ√d) : (↑a * b).re = a * b.re

Proof state:
d a : ℤ
b : ℤ√d
⊢ (↑a * b).re = a * b.re

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Functor.lean
theorem coe_subset : (γ : Set α) ⊆ β

Proof state:
α : Type u
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : ⟨val✝, ha⟩ ∈ γ
right✝ : a✝ ∈ (fun h => (fun a => pure ↑a) ⟨val✝, ha⟩) h✝
⊢ a✝ ∈ β

Tactic:
convert ha

Result:
no goals

Proof state:
α : Type u
β : Set α
γ : Set ↑β
⊢ (do
      let a ← γ
      pure ↑a) ⊆
    β

Tactic:
intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩

Result:
α : Type u
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : ⟨val✝, ha⟩ ∈ γ
right✝ : a✝ ∈ (fun h => (fun a => pure ↑a) ⟨val✝, ha⟩) h✝
⊢ a✝ ∈ β
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full. -/
lemma Full.of_comp_faithful_iso {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [Full H] [G.Faithful]
    (h : F ⋙ G ≅ H) : Full F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full

Tactic:
have := Full.of_iso h.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
this : (F ⋙ G).Full
⊢ F.Full

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
this : (F ⋙ G).Full
⊢ F.Full

Tactic:
exact Full.of_comp_faithful F G

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₂_eq' (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.X i₁).d i₂ i₂' ≫
    K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, i₂'⟩ i₁₂)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂

Tactic:
obtain rfl := c₂.next_eq' h

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem biproduct_ι_comp_leftDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
    (X ◁ biproduct.ι _ j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j

Tactic:
classical
simp [leftDistributor_hom, Preadditive.comp_sum, ← MonoidalCategory.whiskerLeft_comp_assoc,
  biproduct.ι_π, whiskerLeft_dite, dite_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j

Tactic:
simp [leftDistributor_hom, Preadditive.comp_sum, ← MonoidalCategory.whiskerLeft_comp_assoc,
  biproduct.ι_π, whiskerLeft_dite, dite_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_unitOfList
    {l : List α} {k : α} {h} :
    get (unitOfList l) k h = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
h : k ∈ unitOfList l
⊢ get (unitOfList l) k h = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_congr_set' (y : 𝕜) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    derivWithin f s x = derivWithin f t x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
y : 𝕜
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ derivWithin f s x = derivWithin f t x

Tactic:
simp only [derivWithin, fderivWithin_congr_set' y h]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma Differentiable.sub_iff_right (hg : Differentiable 𝕜 f) :
    Differentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 g

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
f g : E → F
hg : Differentiable 𝕜 f
⊢ (Differentiable 𝕜 fun y => f y - g y) ↔ Differentiable 𝕜 g

Tactic:
simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_right]

Result:
no goals
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma min_ne (ha : a ≠ c) (hb : b ≠ c) : min a b ≠ c

Proof state:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then a else b) ≠ c

Tactic:
split_ifs <;> assumption

Result:
no goals

Proof state:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ a ⊓ b ≠ c

Tactic:
rw [min_def]

Result:
R : Type u_2
inst✝ : LinearOrder R
a b c : R
ha : a ≠ c
hb : b ≠ c
⊢ (if a ≤ b then a else b) ≠ c
-- Mathlib/GroupTheory/Index.lean
theorem relindex_bot_right : H.relindex ⊥ = 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relindex ⊥ = 1

Tactic:
rw [relindex, subgroupOf_bot_eq_top, index_top]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem squareCylinders_eq_iUnion_image (C : ∀ i, Set (Set (α i))) :
    squareCylinders C = ⋃ s : Finset ι, (fun t ↦ (s : Set ι).pi t) '' univ.pi C

Proof state:
case h
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
f : Set ((i : ι) → α i)
⊢ f ∈ squareCylinders C ↔ f ∈ ⋃ s, (fun t => (↑s).pi t) '' univ.pi C

Tactic:
simp only [squareCylinders, mem_iUnion, mem_image, mem_univ_pi, exists_prop, mem_setOf_eq,
  eq_comm (a := f)]

Result:
no goals

Proof state:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
⊢ squareCylinders C = ⋃ s, (fun t => (↑s).pi t) '' univ.pi C

Tactic:
ext1 f

Result:
case h
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
f : Set ((i : ι) → α i)
⊢ f ∈ squareCylinders C ↔ f ∈ ⋃ s, (fun t => (↑s).pi t) '' univ.pi C
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem bypass_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).bypass = p.bypass.copy hu hv

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).bypass = p.bypass.copy hu hv

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).bypass = p.bypass.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_ncard_iff_ncard_diff_le_ncard_diff (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
  inter_comm, add_le_add_iff_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_xor_distrib_right : ∀ (x y z : Bool), ((x ^^ y) && z) = ((x && z) ^^ (y && z))

Proof state:
⊢ ∀ (x y z : Bool), ((x ^^ y) && z) = (x && z ^^ y && z)

Tactic:
decide

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem ord_card_unbounded : Unbounded (· < ·) { b : Ordinal | b.card.ord = b } :=
  unbounded_lt_iff.2 fun a =>
    ⟨_,
      ⟨by
        dsimp
        rw [card_ord], (lt_ord_succ_card a).le⟩⟩

Proof state:
a : Ordinal.{u_1}
⊢ (succ a.card).ord ∈ {b | b.card.ord = b}

Tactic:
dsimp

Result:
a : Ordinal.{u_1}
⊢ (succ a.card).ord.card.ord = (succ a.card).ord

Proof state:
a : Ordinal.{u_1}
⊢ (succ a.card).ord.card.ord = (succ a.card).ord

Tactic:
rw [card_ord]

Result:
no goals
-- Mathlib/RingTheory/WittVector/IsPoly.lean
theorem bind₁_onePoly_wittPolynomial [hp : Fact p.Prime] (n : ℕ) :
    bind₁ onePoly (wittPolynomial p ℤ n) = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (wittPolynomial p ℤ n) = 1

Tactic:
rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1

case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Proof state:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → (bind₁ onePoly) (C (↑p ^ b) * X b ^ p ^ (n - b)) = 0

Tactic:
intro i _hi hi0

Result:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 1

Tactic:
simp only [onePoly, one_pow, one_mul, map_pow, C_1, pow_zero, bind₁_X_right, if_true,
  eq_self_iff_true]

Result:
no goals

Proof state:
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0

Tactic:
simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
  bind₁_X_right, map_mul]

Result:
no goals

Proof state:
case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → (bind₁ onePoly) (C (↑p ^ 0) * X 0 ^ p ^ (n - 0)) = 0

Tactic:
simp

Result:
no goals