harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_set' {l : List α} {i j : Nat} {a : α} :
    (set l i a)[j]? = if i = j then Function.const _ a <$> l[j]? else l[j]?

Proof state:
case pos
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : i = j
⊢ (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

Tactic:
simp only [getElem?_set_self', Option.map_eq_map, ↓reduceIte, *]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
⊢ (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

Tactic:
by_cases i = j

Result:
case pos
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : i = j
⊢ (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

case neg
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : ¬i = j
⊢ (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

Proof state:
case neg
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : ¬i = j
⊢ (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

Tactic:
simp only [ne_eq, not_false_eq_true, getElem?_set_ne, ↓reduceIte, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.idxOf a = l.length

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : ¬a ∈ []
⊢ idxOf a [] = [].length

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : ¬a ∈ xs → idxOf a xs = xs.length
h : ¬a = x ∧ ¬a ∈ xs
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) = (x :: xs).length

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : ¬a ∈ xs → idxOf a xs = xs.length
h : ¬a ∈ x :: xs
⊢ idxOf a (x :: xs) = (x :: xs).length

Tactic:
simp only [mem_cons, not_or] at h

Result:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : ¬a ∈ xs → idxOf a xs = xs.length
h : ¬a = x ∧ ¬a ∈ xs
⊢ idxOf a (x :: xs) = (x :: xs).length

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
h : ¬a ∈ l
⊢ idxOf a l = l.length

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [mem_cons, not_or] at h
  simp only [idxOf_cons, cond_eq_if, beq_iff_eq]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : ¬a ∈ xs → idxOf a xs = xs.length
h : ¬a = x ∧ ¬a ∈ xs
⊢ idxOf a (x :: xs) = (x :: xs).length

Tactic:
simp only [idxOf_cons, cond_eq_if, beq_iff_eq]

Result:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : ¬a ∈ xs → idxOf a xs = xs.length
h : ¬a = x ∧ ¬a ∈ xs
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) = (x :: xs).length
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_norm_one : Tendsto (fun a : E => ‖a‖) (𝓝 1) (𝓝 0)

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ Tendsto (fun a => ‖a‖) (𝓝 1) (𝓝 0)

Tactic:
simpa using tendsto_norm_div_self (1 : E)

Result:
no goals
-- Mathlib/Data/Set/List.lean
theorem range_list_getI [Inhabited α] (l : List α) :
    range l.getI = insert default { x | x ∈ l }

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ range l.getI = insert default {x | x ∈ l}

Tactic:
unfold List.getI

Result:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ (range fun n => l.getD n default) = insert default {x | x ∈ l}

Proof state:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ (range fun n => l.getD n default) = insert default {x | x ∈ l}

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem tail_drop (n : ℕ) (s : Stream' α) : tail (drop n s) = drop n (tail s)

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ (drop n s).tail = drop n s.tail

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Array α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : γ → β → γ
x : γ
⊢ foldl g x (pmap f l H) = foldl (fun acc a => g acc (f a.val ⋯)) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldl_map]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_assoc {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} :
    (s.bind f).bind g = s.bind fun a => (f a).bind g :=
  Multiset.induction_on s (by simp) (by simp +contextual)

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind f).bind g = s.bind fun a => (f a).bind g) →
      ((a ::ₘ s).bind f).bind g = (a ::ₘ s).bind fun a => (f a).bind g

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ (bind 0 f).bind g = bind 0 fun a => (f a).bind g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_add (p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).coeff n =
    { toFinsupp := toFinsupp✝¹ }.coeff n + { toFinsupp := toFinsupp✝ }.coeff n

Tactic:
simp_rw [← ofFinsupp_add, coeff]

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ (toFinsupp✝¹ + toFinsupp✝) n = toFinsupp✝¹ n + toFinsupp✝ n

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p + q).coeff n = p.coeff n + q.coeff n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } + q).coeff n = { toFinsupp := toFinsupp✝ }.coeff n + q.coeff n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } + q).coeff n = { toFinsupp := toFinsupp✝ }.coeff n + q.coeff n

Tactic:
rcases q with ⟨⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).coeff n =
    { toFinsupp := toFinsupp✝¹ }.coeff n + { toFinsupp := toFinsupp✝ }.coeff n

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ (toFinsupp✝¹ + toFinsupp✝) n = toFinsupp✝¹ n + toFinsupp✝ n

Tactic:
exact Finsupp.add_apply _ _ _

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem IsHausdorff.eq_iff_smodEq [IsHausdorff I M] {x y : M} :
    x = y ↔ ∀ n, x ≡ y [SMOD (I ^ n • ⊤ : Submodule R M)]

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), x - y ≡ 0 [SMOD I ^ n • ⊤]

Tactic:
simpa [SModEq.sub_mem] using h

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ x - y = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
⊢ x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]

Tactic:
refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ x = y

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ x - y = 0

Tactic:
apply IsHausdorff.haus' (I := I) (x - y)

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsHausdorff I M
x y : M
h : ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), x - y ≡ 0 [SMOD I ^ n • ⊤]
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem nnnorm_equiv_symm_fst (x : α) :
    ‖(WithLp.equiv p (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Proof state:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Tactic:
have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'

Result:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Proof state:
case top
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
hp : Fact (1 ≤ ⊤)
⊢ ‖(WithLp.equiv ⊤ (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Tactic:
simp [prod_nnnorm_eq_sup]

Result:
no goals

Proof state:
case coe
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖(WithLp.equiv (↑p) (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Tactic:
simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : α
⊢ ‖(WithLp.equiv p (α × β)).symm (x, 0)‖₊ = ‖x‖₊

Tactic:
induction p generalizing hp with
| top =>
  simp [prod_nnnorm_eq_sup]
| coe p =>
  have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
  simp [prod_nnnorm_eq_add, NNReal.zero_rpow hp0, ← NNReal.rpow_mul, mul_inv_cancel₀ hp0]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_univ [Fintype α] (inst : Fintype (Sym2 α) := Sym2.instFintype) :
    (univ : Finset α).sym2 = univ

Proof state:
case h
α : Type u_1
inst✝ : Fintype α
inst : optParam (Fintype (Sym2 α)) Sym2.instFintype
a✝ : Sym2 α
⊢ a✝ ∈ univ.sym2 ↔ a✝ ∈ univ

Tactic:
simp only [mem_sym2_iff, mem_univ, implies_true]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
inst : optParam (Fintype (Sym2 α)) Sym2.instFintype
⊢ univ.sym2 = univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Fintype α
inst : optParam (Fintype (Sym2 α)) Sym2.instFintype
a✝ : Sym2 α
⊢ a✝ ∈ univ.sym2 ↔ a✝ ∈ univ
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem C_mul_comp : (C a * p).comp r = C a * p.comp r

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p r : R[X]
⊢ (C a * p).comp r = C a * p.comp r

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp [hp, hq, mul_add]
| h_monomial n b =>
  simp [mul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u
a : R
inst✝ : Semiring R
p✝ r p q : R[X]
hp : (C a * p).comp r = C a * p.comp r
hq : (C a * q).comp r = C a * q.comp r
⊢ (C a * (p + q)).comp r = C a * (p + q).comp r

Tactic:
simp [hp, hq, mul_add]

Result:
no goals

Proof state:
case h_monomial
R : Type u
a : R
inst✝ : Semiring R
p r : R[X]
n : ℕ
b : R
⊢ (C a * (monomial n) b).comp r = C a * ((monomial n) b).comp r

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem finrank_real_of_complex (E : Type*) [AddCommGroup E] [Module ℂ E] :
    Module.finrank ℝ E = 2 * Module.finrank ℂ E

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E

Tactic:
rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem conj_orthogonalProjection {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (U : Submodule 𝕜 E)
    [CompleteSpace U] :
    IsSelfAdjoint
      (U.subtypeL ∘L orthogonalProjection U ∘L T ∘L U.subtypeL ∘L orthogonalProjection U)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ IsSelfAdjoint (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U)))))

Tactic:
rw [← ContinuousLinearMap.comp_assoc]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ IsSelfAdjoint ((U.subtypeL.comp (orthogonalProjection U)).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ IsSelfAdjoint ((U.subtypeL.comp (orthogonalProjection U)).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))

Tactic:
nth_rw 1 [← (orthogonalProjection_isSelfAdjoint U).adjoint_eq]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ IsSelfAdjoint
    ((adjoint (U.subtypeL.comp (orthogonalProjection U))).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ IsSelfAdjoint
    ((adjoint (U.subtypeL.comp (orthogonalProjection U))).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))

Tactic:
exact hT.adjoint_conj _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq' {xs : Vector α n} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x)

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ∀ (x : α), x ∈ xs → ¬p x = true
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simpa using h

Result:
no goals

Proof state:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp_all [any_eq_true']

Result:
no goals

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = false
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = false
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
by_cases h : xs.any p

Result:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = false
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [any_eq_false'] at h

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ∀ (x : α), x ∈ xs → ¬p x = true
⊢ false = decide (∃ x, x ∈ xs ∧ p x = true)

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.any p = true
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.any p = false
⊢ xs.any p = decide (∃ x, x ∈ xs ∧ p x = true)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_ofNat_of_le (h : v ≤ w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

Proof state:
v w : Nat
h : v ≤ w
x : Nat
⊢ setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
v w : Nat
h : v ≤ w
x : Nat
⊢ (setWidth v (BitVec.ofNat w x)).toNat = (BitVec.ofNat v x).toNat

Proof state:
case a
v w : Nat
h : v ≤ w
x : Nat
⊢ (setWidth v (BitVec.ofNat w x)).toNat = (BitVec.ofNat v x).toNat

Tactic:
simp only [toNat_setWidth, toNat_ofNat]

Result:
case a
v w : Nat
h : v ≤ w
x : Nat
⊢ x % 2 ^ w % 2 ^ v = x % 2 ^ v

Proof state:
case a.h
v w : Nat
h : v ≤ w
x : Nat
⊢ 2 ^ v ∣ 2 ^ w

Tactic:
exact Nat.pow_dvd_pow_iff_le_right'.mpr h

Result:
no goals

Proof state:
case a
v w : Nat
h : v ≤ w
x : Nat
⊢ x % 2 ^ w % 2 ^ v = x % 2 ^ v

Tactic:
rw [Nat.mod_mod_of_dvd]

Result:
case a.h
v w : Nat
h : v ≤ w
x : Nat
⊢ 2 ^ v ∣ 2 ^ w
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq_of_ge {u : ι → Ω → β} {τ : Ω → ι} {i : ι} {ω : Ω} (h : τ ω ≤ i) :
    stoppedProcess u τ i ω = u (τ ω) ω

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : LinearOrder ι
u : ι → Ω → β
τ : Ω → ι
i : ι
ω : Ω
h : τ ω ≤ i
⊢ stoppedProcess u τ i ω = u (τ ω) ω

Tactic:
simp [stoppedProcess, min_eq_right h]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma neg {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt (-f) x

Proof state:
case h.e'_6.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
z : 𝕜
⊢ (-f) z = ((fun x => -1) • f) z

Tactic:
simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul]

Result:
no goals

Proof state:
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
⊢ -f = (fun x => -1) • f

Tactic:
ext1 z

Result:
case h.e'_6.h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
z : 𝕜
⊢ (-f) z = ((fun x => -1) • f) z

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
⊢ MeromorphicAt (-f) x

Tactic:
convert (MeromorphicAt.const (-1 : 𝕜) x).smul hf using 1

Result:
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
⊢ -f = (fun x => -1) • f
-- Mathlib/RingTheory/Coprime/Basic.lean
/-- `IsCoprime` is not a useful definition for `Nat`; consider using `Nat.Coprime` instead. -/
@[simp]
lemma Nat.isCoprime_iff {m n : ℕ} : IsCoprime m n ↔ m = 1 ∨ n = 1

Proof state:
case refine_2
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n

Tactic:
obtain rfl | rfl := h

Result:
case refine_2.inl
n : ℕ
⊢ IsCoprime 1 n

case refine_2.inr
m : ℕ
⊢ IsCoprime m 1

Proof state:
m n : ℕ
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1

Tactic:
refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩

Result:
case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

case refine_2
m n : ℕ
h : m = 1 ∨ n = 1
⊢ IsCoprime m n

Proof state:
case refine_2.inl
n : ℕ
⊢ IsCoprime 1 n

Tactic:
exact isCoprime_one_left

Result:
no goals

Proof state:
case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ m = 1 ∨ n = 1

Tactic:
simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H

Result:
case refine_1
m n : ℕ
x✝ : IsCoprime m n
a b : ℕ
H : (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)
⊢ m = 1 ∨ n = 1

Proof state:
case refine_2.inr
m : ℕ
⊢ IsCoprime m 1

Tactic:
exact isCoprime_one_right

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem nhdsSet_le_iff [T1Space X] {s t : Set X} : 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
⊢ x ∈ t

Tactic:
by_contra hxt

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
hxt : x ∉ t
⊢ False

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t

Tactic:
intro h x hx

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
x : X
hx : x ∈ s
⊢ x ∈ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
x : X
hx : x ∈ s
⊢ x ∈ t

Tactic:
specialize h {x}ᶜ

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∈ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Tactic:
refine ⟨?_, fun h => monotone_nhdsSet h⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∈ t

Tactic:
simp_rw [compl_singleton_mem_nhdsSet_iff] at h

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
⊢ x ∈ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t

Tactic:
simp_rw [Filter.le_def]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
hxt : x ∉ t
⊢ False

Tactic:
exact h hxt hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_cons_left : Disjoint (a::l₁) l₂ ↔ (a ∉ l₂) ∧ Disjoint l₁ l₂ :=
  (disjoint_append_left (l₁ := [a])).trans <| by simp [singleton_disjoint]

Proof state:
α✝ : Type u_1
a : α✝
l₁ l₂ : List α✝
⊢ [a].Disjoint l₂ ∧ l₁.Disjoint l₂ ↔ ¬a ∈ l₂ ∧ l₁.Disjoint l₂

Tactic:
simp [singleton_disjoint]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_add (m : ℕ) : ∀ n : ℕ, f^[m + n] = f^[m] ∘ f^[n]
  | 0 => rfl
  | Nat.succ n => by rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]; rfl

Proof state:
α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]

Result:
α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_bot (h : 2 ≤ n) : (⊥ : SimpleGraph α).CliqueFree n

Proof state:
α : Type u_1
n : ℕ
h : 2 ≤ n
⊢ ⊥.CliqueFree n

Tactic:
intro t ht

Result:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
⊢ False

Proof state:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
this : 2 ≤ 1
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
⊢ False

Tactic:
have := le_trans h (isNClique_bot_iff.1 ht).1

Result:
α : Type u_1
n : ℕ
h : 2 ≤ n
t : Finset α
ht : ⊥.IsNClique n t
this : 2 ≤ 1
⊢ False
-- Mathlib/Algebra/Module/Equiv/Basic.lean
theorem toIntLinearEquiv_toAddEquiv : ↑e.toIntLinearEquiv = e

Proof state:
case h
M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑e.toIntLinearEquiv x✝ = e x✝

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
e : M ≃+ M₂
⊢ ↑e.toIntLinearEquiv = e

Tactic:
ext

Result:
case h
M : Type u_5
M₂ : Type u_7
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
e : M ≃+ M₂
x✝ : M
⊢ ↑e.toIntLinearEquiv x✝ = e x✝