harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/CondVar.lean
@[simp] lemma condVar_neg (X : Ω → ℝ) : Var[-X; μ | m] =ᵐ[μ] Var[X; μ | m]

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ Var[-X; μ | m] =ᶠ[ae μ] Var[X; μ | m]

Tactic:
refine condExp_congr_ae ?_

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ (-X - μ[-X|m]) ^ 2 =ᶠ[ae μ] (X - μ[X|m]) ^ 2

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : (μ[-X|m]) ω = (-μ[X|m]) ω
⊢ ((-X - μ[-X|m]) ^ 2) ω = ((X - μ[X|m]) ^ 2) ω

Tactic:
simp [condVar, hω]

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : (μ[-X|m]) ω = (-μ[X|m]) ω
⊢ (-X ω + (μ[X|m]) ω) ^ 2 = (X ω - (μ[X|m]) ω) ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ (-X - μ[-X|m]) ^ 2 =ᶠ[ae μ] (X - μ[X|m]) ^ 2

Tactic:
filter_upwards [condExp_neg (m := m) X] with ω hω

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : (μ[-X|m]) ω = (-μ[X|m]) ω
⊢ ((-X - μ[-X|m]) ^ 2) ω = ((X - μ[X|m]) ^ 2) ω

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : (μ[-X|m]) ω = (-μ[X|m]) ω
⊢ (-X ω + (μ[X|m]) ω) ^ 2 = (X ω - (μ[X|m]) ω) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem head_cyclicPermutations (l : List α) :
    (cyclicPermutations l).head (cyclicPermutations_ne_nil l) = l

Proof state:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.cyclicPermutations.head ⋯ = l

Tactic:
rw [← get_mk_zero h, get_cyclicPermutations, Fin.val_mk, rotate_zero]

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ l.cyclicPermutations.head ⋯ = l

Tactic:
have h : 0 < length (cyclicPermutations l) := length_pos_of_ne_nil (cyclicPermutations_ne_nil _)

Result:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.cyclicPermutations.head ⋯ = l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_filter {l : Array α} (p : α → Bool) :
    (l.filter p).attach = l.attach.filterMap
      fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) { toList := toList✝ }.attach

Tactic:
rw [attach_congr (List.filter_toArray p _)]

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (List.filter p toList✝).toArray.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) { toList := toList✝ }.attach

Proof state:
α : Type u_1
l : Array α
p : α → Bool
⊢ (filter p l).attach = filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ }).attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (List.filter p toList✝).toArray.attach =
    filterMap (fun x => if w : p x.val = true then some ⟨x.val, ⋯⟩ else none) { toList := toList✝ }.attach

Tactic:
simp [List.attach_filter, List.map_filterMap, Function.comp_def]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma one_add_I_mul_ne_one_or {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) :
    1 + I * y ≠ 1 ∨ χ ≠ 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ 1 + I * ↑y ≠ 1 ∨ χ ≠ 1

Tactic:
simpa only [ne_eq, add_right_eq_self, _root_.mul_eq_zero, I_ne_zero, ofReal_eq_zero, false_or]
  using hy

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem eqOn_adjoin_iff {φ ψ : A →ₐ[R] B} {s : Set A}  :
    Set.EqOn φ ψ (adjoin R s) ↔ Set.EqOn φ ψ s

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Tactic:
have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl

Result:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
this : ∀ (S : Set A), S ≤ ↑(equalizer φ ψ) ↔ Set.EqOn (⇑φ) (⇑ψ) S
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
this : ∀ (S : Set A), S ≤ ↑(equalizer φ ψ) ↔ Set.EqOn (⇑φ) (⇑ψ) S
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Tactic:
simp only [← this, Set.le_eq_subset, SetLike.coe_subset_coe, adjoin_le_iff]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem join_cons_cons (a b : α) (s S) :
    join (cons (a, cons b s) S) = cons a (join (cons (b, s) S)) :=
  destruct_eq_cons <| by simp [join]

Proof state:
α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (cons (a, cons b s) S).join.destruct = some (a, (cons (b, s) S).join)

Tactic:
simp [join]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem isPerfectMatching_iff : M.IsPerfectMatching ↔ ∀ v, ∃! w, M.Adj v w

Proof state:
case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts

Tactic:
obtain ⟨w, hw, -⟩ := hm v

Result:
case refine_2.intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v w : V
hw : M.Adj v w
⊢ v ∈ M.verts

Proof state:
case refine_1.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : M.IsMatching
hs : M.IsSpanning
v : V
⊢ ∃! w, M.Adj v w

Tactic:
exact hm (hs v)

Result:
no goals

Proof state:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w

Tactic:
rintro ⟨hm, hs⟩ v

Result:
case refine_1.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : M.IsMatching
hs : M.IsSpanning
v : V
⊢ ∃! w, M.Adj v w

Proof state:
case refine_2.intro.intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v w : V
hw : M.Adj v w
⊢ v ∈ M.verts

Tactic:
exact M.edge_vert hw

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w, M.Adj v w

Tactic:
refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩

Result:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching → ∀ (v : V), ∃! w, M.Adj v w

case refine_2
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w, M.Adj v w
v : V
⊢ v ∈ M.verts
-- Mathlib/Combinatorics/HalesJewett.lean
theorem prod_apply {α ι ι'} (l : Line α ι) (l' : Line α ι') (x : α) :
    l.prod l' x = Sum.elim (l x) (l' x)

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
⊢ ↑(l.prod l') x = Sum.elim (↑l x) (↑l' x)

Tactic:
funext i

Result:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(l.prod l') x i = Sum.elim (↑l x) (↑l' x) i

Proof state:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
l' : Line α ι'
x : α
i : ι ⊕ ι'
⊢ ↑(l.prod l') x i = Sum.elim (↑l x) (↑l' x) i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_mem_range (hp : p ≠ 0) : p.supDegree D ∈ Set.range D

Proof state:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
a : A
he : supDegree D p = D a
⊢ supDegree D p ∈ Set.range D

Tactic:
exact ⟨a, he.symm⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
⊢ supDegree D p ∈ Set.range D

Tactic:
obtain ⟨a, -, he⟩ := exists_supDegree_mem_support D hp

Result:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
a : A
he : supDegree D p = D a
⊢ supDegree D p ∈ Set.range D
-- Mathlib/GroupTheory/PresentedGroup.lean
theorem closure_range_of (rels : Set (FreeGroup α)) :
    Subgroup.closure (Set.range (PresentedGroup.of : α → PresentedGroup rels)) = ⊤

Proof state:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ (QuotientGroup.mk' (Subgroup.normalClosure rels)).range = ⊤

Tactic:
exact MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)

Result:
no goals

Proof state:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _),
  FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]

Result:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ (QuotientGroup.mk' (Subgroup.normalClosure rels)).range = ⊤

Proof state:
α : Type u_1
rels : Set (FreeGroup α)
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl

Result:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (Set.range of) = ⊤
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_eq_Ioc_same_iff : Ioo a b = Ioc a b ↔ ¬a < b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ioc a b

Tactic:
rw [Ioo_eq_empty h, Ioc_eq_empty h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Ioo a b = Ioc a b
⊢ ¬a < b

Tactic:
simpa using Set.ext_iff.mp h b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
@[simp] lemma induceHomOfLE_toHom :
    (G.induceHomOfLE h).toHom = induceHom (.id : G →g G) ((Set.mapsTo_id s).mono_right h)

Proof state:
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
⊢ (G.induceHomOfLE h).toHom = induceHom Hom.id ⋯

Tactic:
ext

Result:
case h.a
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
x✝ : ↑s
⊢ ↑((G.induceHomOfLE h).toHom x✝) = ↑((induceHom Hom.id ⋯) x✝)

Proof state:
case h.a
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
x✝ : ↑s
⊢ ↑((G.induceHomOfLE h).toHom x✝) = ↑((induceHom Hom.id ⋯) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem sub_mem_orthogonal_of_inner_left {x y : E} (h : ∀ v : K, ⟪x, v⟫ = ⟪y, v⟫) : x - y ∈ Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
⊢ ∀ u ∈ K, inner (x - y) u = 0

Tactic:
intro u hu

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u

Tactic:
exact h ⟨u, hu⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
⊢ x - y ∈ Kᗮ

Tactic:
rw [mem_orthogonal']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
⊢ ∀ u ∈ K, inner (x - y) u = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0

Tactic:
rw [inner_sub_left, sub_eq_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma app_eq_appLE {U : Y.Opens} :
    f.app U = f.appLE U _ le_rfl

Proof state:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
⊢ f.app U = f.appLE U (f ⁻¹ᵁ U) ⋯

Tactic:
simp [Hom.appLE]

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.inter {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) : IsGδ (s ∩ t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ b, bif b then s else t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ b, bif b then s else t)

Tactic:
exact .iInter (Bool.forall_bool.2 ⟨ht, hs⟩)

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

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = false
⊢ replaceEntry k v (l ++ l') = l ++ replaceEntry k v l'

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k [] = false
⊢ replaceEntry k v ([] ++ l') = [] ++ replaceEntry k v l'

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = false → replaceEntry k v (tail✝ ++ l') = tail✝ ++ replaceEntry k v l'
h : containsKey k (⟨k✝, v✝⟩ :: tail✝) = false
⊢ replaceEntry k v (⟨k✝, v✝⟩ :: tail✝ ++ l') = ⟨k✝, v✝⟩ :: tail✝ ++ replaceEntry k v l'

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

Tactic:
simp only [containsKey_cons, Bool.or_eq_false_iff] at h

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = false → replaceEntry k v (t ++ l') = t ++ replaceEntry k v l'
h : (k' == k) = false ∧ containsKey k t = false
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = ⟨k', v'⟩ :: t ++ replaceEntry k v l'

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k [] = false
⊢ replaceEntry k v ([] ++ l') = [] ++ replaceEntry k v l'

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = false → replaceEntry k v (tail✝ ++ l') = tail✝ ++ replaceEntry k v l'
h : containsKey k (⟨k✝, v✝⟩ :: tail✝) = false
⊢ replaceEntry k v (⟨k✝, v✝⟩ :: tail✝ ++ l') = ⟨k✝, v✝⟩ :: tail✝ ++ replaceEntry k v l'

Tactic:
next k' v' t ih =>
simp only [containsKey_cons, Bool.or_eq_false_iff] at h
simpa [replaceEntry_cons, h.1] using ih h.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = false → replaceEntry k v (t ++ l') = t ++ replaceEntry k v l'
h : (k' == k) = false ∧ containsKey k t = false
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = ⟨k', v'⟩ :: t ++ replaceEntry k v l'

Tactic:
simpa [replaceEntry_cons, h.1] using ih h.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_singleton_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
    l.mapFinIdx f = [b] ↔ ∃ (a : α) (w : l = [a]), f 0 a (by simp [w]) = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ l.mapFinIdx f = [b] ↔ ∃ a w, f 0 a ⋯ = b

Tactic:
simp [mapFinIdx_eq_cons_iff]

Result:
no goals

Proof state:
α : Type ?u.48036
β : Type ?u.48060
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
a : α
w : l = [a]
⊢ 0 < l.length

Tactic:
simp [w]

Result:
no goals
-- Mathlib/Topology/Bornology/BoundedOperation.lean
lemma SeminormedAddCommGroup.lipschitzWith_sub :
    LipschitzWith 2 (fun (p : R × R) ↦ p.1 - p.2)

Proof state:
case h.e'_5
R : Type u_1
inst✝ : SeminormedAddCommGroup R
⊢ 2 = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
⊢ LipschitzWith 2 fun p => p.1 - p.2

Tactic:
convert LipschitzWith.prod_fst.sub LipschitzWith.prod_snd

Result:
case h.e'_5
R : Type u_1
inst✝ : SeminormedAddCommGroup R
⊢ 2 = 1 + 1
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_eq' [TopologicalSpace ι] [OrderTopology ι]
    [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω = i}

Tactic:
exact hτ.measurableSet_eq i

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_taylor {R} [CommSemiring R] (f : R[X]) (r s : R) :
    taylor r (taylor s f) = taylor (r + s) f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
f : R[X]
r s : R
⊢ (taylor r) ((taylor s) f) = (taylor (r + s)) f

Tactic:
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, C_add, add_assoc]

Result:
no goals
-- Mathlib/Data/Finset/Slice.lean
theorem sum_card_slice : ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜

Proof state:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ x ∈ Iic (Fintype.card α), ∀ y ∈ Iic (Fintype.card α), x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)

Tactic:
exact Finset.pairwiseDisjoint_slice.subset (Set.subset_univ _)

Result:
no goals

Proof state:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜

Tactic:
letI := Classical.decEq α

Result:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜

Proof state:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜

Tactic:
rw [← card_biUnion, biUnion_slice]

Result:
α : Type u_1
𝒜 : Finset (Finset α)
inst✝ : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∀ x ∈ Iic (Fintype.card α), ∀ y ∈ Iic (Fintype.card α), x ≠ y → Disjoint (𝒜 # x) (𝒜 # y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_tail (l : List α) (i : Nat) :
    (tail l)[i]? = l[i + 1]?

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.tail[i]? = l[i + 1]?

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem rprod_le_transGen_gameAdd : RProd rα rβ ≤ Relation.TransGen (GameAdd rα rβ)
  | _, _, h => h.rec (by
      intro _ _ _ _ hα hβ
      exact Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ))

Proof state:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
⊢ ∀ {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, rα a₁ a₂ → rβ b₁ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
intro _ _ _ _ hα hβ

Result:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
hα : rα a₁✝ a₂✝
hβ : rβ b₁✝ b₂✝
⊢ Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)

Proof state:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
a₁✝ : α
b₁✝ : β
a₂✝ : α
b₂✝ : β
hα : rα a₁✝ a₂✝
hβ : rβ b₁✝ b₂✝
⊢ Relation.TransGen (GameAdd rα rβ) (a₁✝, b₁✝) (a₂✝, b₂✝)

Tactic:
exact Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem pred_toNat : ∀ i : Int, (i - 1).toNat = i.toNat - 1
  | 0 => rfl
  | (_+1:Nat) => by simp [ofNat_add]
  | -[_+1] => rfl

Proof state:
n✝ : Nat
⊢ (↑(n✝ + 1) - 1).toNat = (↑(n✝ + 1)).toNat - 1

Tactic:
simp [ofNat_add]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem dropWhile (p : Char → Bool) : ∀ {s}, ValidFor l m r s →
    ValidFor (l ++ m.takeWhile p) (m.dropWhile p) r (s.dropWhile p)
  | _, ⟨⟩ => by
    simp only [Substring.dropWhile, takeWhileAux_of_valid]
    apply ValidFor.of_eq <;> simp
    rw [Nat.add_assoc, ← utf8Len_append (m.takeWhile p), List.takeWhile_append_dropWhile]

Proof state:
l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }

Tactic:
apply ValidFor.of_eq <;> simp

Result:
case a
l m r : List Char
p : Char → Bool
⊢ utf8Len l + utf8Len m = utf8Len l + utf8Len (List.takeWhile p m) + utf8Len (List.dropWhile p m)

Proof state:
l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    ({ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.dropWhile
      p)

Tactic:
simp only [Substring.dropWhile, takeWhileAux_of_valid]

Result:
l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }

Proof state:
case a
l m r : List Char
p : Char → Bool
⊢ utf8Len l + utf8Len m = utf8Len l + utf8Len (List.takeWhile p m) + utf8Len (List.dropWhile p m)

Tactic:
rw [Nat.add_assoc, ← utf8Len_append (m.takeWhile p), List.takeWhile_append_dropWhile]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_add' [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α]
    (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (x + c)) = ∏ x ∈ Ico (a + c) (b + c), f x

Proof state:
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
rw [← map_add_right_Ico, prod_map]

Result:
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)