harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sublists.lean
theorem sublists'_map (f : α → β) : ∀ (l : List α),
    sublists' (map f l) = map (map f) (sublists' l)
  | [] => by simp
  | a::l => by simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]

Proof state:
α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists' = map (map f) [].sublists'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists' = map (map f) (a :: l).sublists'

Tactic:
simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem card_le_card_image₂_right {t : Finset β} (ht : t.Nonempty)
    (hf : ∀ b, Injective fun a => f a b) : #s ≤ #(image₂ f s t)

Proof state:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ #(image₂ f s {b}) ≤ #(image₂ f s t)

Tactic:
exact card_le_card (image₂_subset_left <| singleton_subset_iff.2 hb)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
ht : t.Nonempty
hf : ∀ (b : β), Injective fun a => f a b
⊢ #s ≤ #(image₂ f s t)

Tactic:
obtain ⟨b, hb⟩ := ht

Result:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ #s ≤ #(image₂ f s t)

Proof state:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ #s ≤ #(image₂ f s t)

Tactic:
rw [← card_image₂_singleton_right _ (hf b)]

Result:
case intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ (b : β), Injective fun a => f a b
b : β
hb : b ∈ t
⊢ #(image₂ f s {b}) ≤ #(image₂ f s t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_take_le (n) (l : List α) : length (take n l) ≤ n

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (take n l).length ≤ n

Tactic:
simp [Nat.min_le_left]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_sub_sub_self (x y : F) : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
simp only [inner_sub_left, inner_sub_right]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
ring

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem ofInt_eq_intCast (n : ℤ) : (ofInt n : ℤ√d) = n

Proof state:
d n : ℤ
⊢ ofInt n = ↑n

Tactic:
ext <;> simp [ofInt_re, ofInt_im]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : List α
⊢ (∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ↔ ¬a ∈ l

Tactic:
simp [forall_mem_ne']

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : List α
⊢ l.erase a = l ↔ ¬a ∈ l

Tactic:
rw [erase_eq_eraseP', eraseP_eq_self_iff]

Result:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l : List α
⊢ (∀ (a_1 : α), a_1 ∈ l → ¬(a_1 == a) = true) ↔ ¬a ∈ l
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformly.prod_map {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'}
    {f' : α' → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') :
    TendstoUniformly (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)

Tactic:
exact h.prod_map h'

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Tactic:
rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformlyOn F f p univ
h' : TendstoUniformlyOn F' f' p' univ
⊢ TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (univ ×ˢ univ)
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_bisim_tail {f₁ : α → σ₁ → σ₁ × β} {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂}
    (h : ∃ R : σ₁ → σ₂ → Prop, R s₁ s₂ ∧
      ∀ {s q} a, R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) :
    (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd

Proof state:
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
rcases h with ⟨R, h₀, hR⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2
⊢ (mapAccumr f₁ xs s₁).2 = (mapAccumr f₂ xs s₂).2

Tactic:
exact (mapAccumr_bisim R h₀ hR).2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_flatMap {l : List α} {f : α → List β} :
    (l.flatMap f).head? = l.findSome? fun a => (f a).head?

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : (flatMap f tail✝).head? = findSome? (fun a => (f a).head?) tail✝
⊢ (flatMap f (head✝ :: tail✝)).head? =
    match (f head✝).head? with
    | some b => some b
    | none => findSome? (fun a => (f a).head?) tail✝

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → List β
⊢ (flatMap f []).head? = findSome? (fun a => (f a).head?) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : (flatMap f tail✝).head? = findSome? (fun a => (f a).head?) tail✝
⊢ (flatMap f (head✝ :: tail✝)).head? = findSome? (fun a => (f a).head?) (head✝ :: tail✝)

Tactic:
simp only [findSome?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : (flatMap f tail✝).head? = findSome? (fun a => (f a).head?) tail✝
⊢ (flatMap f (head✝ :: tail✝)).head? =
    match (f head✝).head? with
    | some b => some b
    | none => findSome? (fun a => (f a).head?) tail✝

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (flatMap f l).head? = findSome? (fun a => (f a).head?) l

Tactic:
induction l with
| nil => rfl
| cons =>
  simp only [findSome?_cons]
  split <;> simp_all

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

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 ≠ 1
⊢ (replaceHead x hnotone (singleton x✝ a✝)).head = x

Tactic:
rfl

Result:
no goals

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 ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x

Tactic:
simp [*, replaceHead]

Result:
no goals

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

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 ≠ 1
⊢ (replaceHead x hnotone (singleton x✝ a✝)).head = x

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 ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem coe_of_apply {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
    [AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : A i) :
    (of (fun i ↦ {x // x ∈ A i}) i x j : M) = if i = j then x else 0

Proof state:
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
⊢ ↑(((of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
obtain rfl | h := Decidable.eq_or_ne i j

Result:
case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : ↥(A i)
⊢ ↑(((of (fun i => ↥(A i)) i) x) i) = ↑(if i = i then x else 0)

case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : i ≠ j
⊢ ↑(((of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Proof state:
case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : i ≠ j
⊢ ↑(((of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

Result:
no goals

Proof state:
case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : ↥(A i)
⊢ ↑(((of (fun i => ↥(A i)) i) x) i) = ↑(if i = i then x else 0)

Tactic:
rw [DirectSum.of_eq_same, if_pos rfl]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem Integrable.hasIntegral (h : Integrable I l f vol) :
    HasIntegral I l f vol (integral I l f vol)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
⊢ HasIntegral I l f vol (Exists.choose h)

Tactic:
exact Classical.choose_spec h

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
⊢ HasIntegral I l f vol (integral I l f vol)

Tactic:
rw [integral, dif_pos h]

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
⊢ HasIntegral I l f vol (Exists.choose h)
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D]
    (H : C ⥤ D) :/- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
             H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
          colimit.post
          F H ≫
        H.map (colim.map α) =
      colim.map (whiskerRight α H) ≫ colimit.post G H

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι G j✝)

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι G j✝)
-- Mathlib/Data/String/Lemmas.lean
@[simp] lemma length_replicate (n : ℕ) (c : Char) : (replicate n c).length = n

Proof state:
n : ℕ
c : Char
⊢ (replicate n c).length = n

Tactic:
simp only [String.length, String.replicate, List.length_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/RawLemmas.lean
theorem getD_insertManyIfNewUnit_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit m l) k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α Unit
l : List α
k : α
fallback : Unit
⊢ (m.insertManyIfNewUnit l).getD k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_sub_left {x y z : E} : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x y z : E
⊢ inner (x - y) z = inner x z - inner y z

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/List.lean
lemma list_sum_right (a : R) (l : List R) (h : ∀ b ∈ l, Commute a b) : Commute a l.sum

Proof state:
case nil
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
h : ∀ (b : R), b ∈ [] → Commute a b
⊢ Commute a [].sum

Tactic:
exact Commute.zero_right _

Result:
no goals

Proof state:
case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Tactic:
exact (h _ <| mem_cons_self _ _).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Result:
no goals

Proof state:
case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x :: xs).sum

Tactic:
rw [List.sum_cons]

Result:
case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Proof state:
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a l.sum

Tactic:
induction l with
| nil => exact Commute.zero_right _
| cons x xs ih =>
  rw [List.sum_cons]
  exact (h _ <| mem_cons_self _ _).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem cmpLE_swap {α} [LE α] [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)] (x y : α) :
    (cmpLE x y).swap = cmpLE y x

Proof state:
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x y : α
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, *, Ordering.swap]

Result:
case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Proof state:
case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ False

Tactic:
cases not_or_intro xy yx (total_of _ _ _)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_iff_edist_tendsto_0 {l : Filter β} {f : β → α} {y : α} :
    Tendsto f l (𝓝 y) ↔ Tendsto (fun x => edist (f x) y) l (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
l : Filter β
f : β → α
y : α
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (fun x => edist (f x) y) l (𝓝 0)

Tactic:
simp only [EMetric.nhds_basis_eball.tendsto_right_iff, EMetric.mem_ball,
  @tendsto_order ℝ≥0∞ β _ _, forall_prop_of_false ENNReal.not_lt_zero, forall_const, true_and]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_exp_Iic (c : ℝ) : IntegrableOn exp (Iic c)

Proof state:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ rexp (id y)

Tactic:
exact (exp_pos _).le

Result:
no goals

Proof state:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c

Tactic:
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]

Result:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ rexp (id y)

Proof state:
c : ℝ
⊢ IntegrableOn rexp (Iic c) volume

Tactic:
refine
  integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
    (fun y => intervalIntegrable_exp.1) tendsto_id
    (eventually_of_mem (Iic_mem_atBot 0) fun y _ => ?_)

Result:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
@[simp]
lemma Iso.isMatching_map {G' : SimpleGraph W} {M : Subgraph G} (f : G ≃g G') :
    (M.map f.toHom).IsMatching ↔ M.IsMatching where
   mp h

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G ≃g G'
h : (Subgraph.map f.toHom M).IsMatching
⊢ M.IsMatching

Tactic:
simpa [← map_comp] using h.map f.symm.toHom f.symm.injective

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometric_radius_top_of_neg_nat₂ {k : ℕ} :
    (ordinaryHypergeometricSeries 𝔸 a (-(k : 𝕂)) c).radius = ⊤

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 (-↑k) a c).radius = ⊤

Tactic:
exact ordinaryHypergeometric_radius_top_of_neg_nat₁ 𝔸 a c

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 a (-↑k) c).radius = ⊤

Tactic:
rw [ordinaryHypergeometricSeries_symm]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 (-↑k) a c).radius = ⊤
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma ae_smul_measure_iff (hc : c ≠ 0) {μ : Measure α} : (∀ᵐ x ∂c • μ, p x) ↔ ∀ᵐ x ∂μ, p x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
p : α → Prop
hc : c ≠ 0
μ : Measure α
⊢ (∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x

Tactic:
simp [ae_iff, hc]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
lemma summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) :
    Summable fun n : ℕ ↦ n ^ k * exp (-r * n)

Proof state:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n => ↑n ^ k * rexp (-r) ^ n

Tactic:
apply summable_pow_mul_geometric_of_norm_lt_one

Result:
case hr
k : ℕ
r : ℝ
hr : 0 < r
⊢ ‖rexp (-r)‖ < 1

Proof state:
case hr
k : ℕ
r : ℝ
hr : 0 < r
⊢ ‖rexp (-r)‖ < 1

Tactic:
rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]

Result:
no goals

Proof state:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n => ↑n ^ k * rexp (-r * ↑n)

Tactic:
simp_rw [mul_comm (-r), exp_nat_mul]

Result:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n => ↑n ^ k * rexp (-r) ^ n
-- Mathlib/CategoryTheory/GlueData.lean
theorem t'_jii (i j : D.J) : D.t' j i i = pullback.fst _ _ ≫ D.t j i ≫ inv (pullback.snd _ _)

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Result:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_uncurry (f : α → β → γ) (x : Option (α × β)) :
    x.map (uncurry f) = map₂ f (x.map Prod.fst) (x.map Prod.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)

Tactic:
cases x <;> rfl

Result:
no goals