harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem AffineEquiv.pointReflection_midpoint_right (x y : P) :
    pointReflection R (midpoint R x y) y = x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection R (midpoint R x y)) y = x

Tactic:
rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem riemannZeta_four : riemannZeta 4 = π ^ 4 / 90

Proof state:
case h.e'_2

⊢ riemannZeta 4 = ↑(∑' (b : ℕ), 1 / ↑b ^ 4)

Tactic:
rw [← Nat.cast_one, show (4 : ℂ) = (4 : ℕ) by norm_num,
  zeta_nat_eq_tsum_of_gt_one (by norm_num : 1 < 4)]

Result:
case h.e'_2

⊢ ∑' (n : ℕ), 1 / ↑n ^ 4 = ↑(∑' (b : ℕ), ↑1 / ↑b ^ 4)

Proof state:
⊢ 4 = ↑4

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 1 < 4

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ riemannZeta 4 = ↑π ^ 4 / 90

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

Result:
case h.e'_2

⊢ riemannZeta 4 = ↑(∑' (b : ℕ), 1 / ↑b ^ 4)

case h.e'_3

⊢ ↑π ^ 4 / 90 = ↑(π ^ 4 / 90)

Proof state:
case h.e'_2

⊢ ∑' (n : ℕ), 1 / ↑n ^ 4 = ↑(∑' (b : ℕ), ↑1 / ↑b ^ 4)

Tactic:
simp only [push_cast]

Result:
no goals

Proof state:
case h.e'_3

⊢ ↑π ^ 4 / 90 = ↑(π ^ 4 / 90)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
/-- The eigenvalues of a positive definite matrix are positive -/
lemma eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜}
    (hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosDef
i : n
⊢ 0 < ⋯.eigenvalues i

Tactic:
simp only [hA.1.eigenvalues_eq]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosDef
i : n
⊢ 0 <
    RCLike.re
      (star ((WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i)) ⬝ᵥ A *ᵥ (WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i))

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosDef
i : n
⊢ 0 <
    RCLike.re
      (star ((WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i)) ⬝ᵥ A *ᵥ (WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i))

Tactic:
exact hA.re_dotProduct_pos <| hA.1.eigenvectorBasis.orthonormal.ne_zero i

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_preAleph_succ {o : Ordinal} (h : ω ≤ o) : IsRegular (preAleph (succ o))

Proof state:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (preAleph o)).IsRegular

Tactic:
exact isRegular_succ (aleph0_le_preAleph.2 h)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (preAleph (succ o)).IsRegular

Tactic:
rw [preAleph_succ]

Result:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (preAleph o)).IsRegular
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem PartialHomeomorph.univUnitBall_apply_zero : univUnitBall (0 : E) = 0

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall 0 = 0

Tactic:
simp [PartialHomeomorph.univUnitBall_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp]
lemma isSemisimple_zero [IsSemisimpleModule R M] : IsSemisimple (0 : Module.End R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ IsSemisimple 0

Tactic:
simpa [isSemisimple_iff] using exists_isCompl

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma cauchy_iff_tendsto (𝓕 : Filter G) :
    Cauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Proof state:
G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (fun p => p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [Cauchy, uniformity_eq_comap_nhds_one_swapped, ← tendsto_iff_comap]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem filter_ne_fill [DecidableEq α] (a : α) (m : Σi : Fin (n + 1), Sym α (n - i)) (h : a ∉ m.2) :
    (m.2.fill a m.1).filterNe a = m :=
  sigma_sub_ext
    (by
      rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
      rw [filter_add, filter_eq_self.2, add_right_eq_self, eq_zero_iff_forall_not_mem]
      · intro b hb
        rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
        exact hb.2 hb.1.2.symm
      · exact fun a ha ha' => h <| ha'.symm ▸ ha)

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False

Tactic:
exact hb.2 hb.1.2.symm

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
exact fun a ha ha' => h <| ha'.symm ▸ ha

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ filter (fun x => a ≠ x) ↑(replicate (↑m.fst) a)
⊢ False

Tactic:
rw [mem_filter, Sym.mem_coe, mem_replicate] at hb

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x => a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd

Tactic:
rw [filter_add, filter_eq_self.2, add_right_eq_self, eq_zero_iff_forall_not_mem]

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x => a ≠ x) ↑(replicate (↑m.fst) a)

α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x => a ≠ x) ↑(replicate (↑m.fst) a)

Tactic:
intro b hb

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ filter (fun x => a ≠ x) ↑(replicate (↑m.fst) a)
⊢ False

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd

Tactic:
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x => a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_map_equiv_to_embedding {α β : Type*} [Fintype α] [Fintype β] (e : α ≃ β) :
    univ.map e.toEmbedding = univ :=
  eq_univ_iff_forall.mpr fun b => mem_map.mpr ⟨e.symm b, mem_univ _, by simp⟩

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ e.toEmbedding (e.symm b) = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem _root_.biSup_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) :
    ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun _ ↦ ⟨by simp_all, by simp_all⟩

Proof state:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst✝ : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x✝ : β
⊢ ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩ ≤ x✝ → ⨆ ij ∈ s.sigma t, f ij ≤ x✝

Tactic:
simp_all

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
β : Type u_4
inst✝ : CompleteLattice β
s : Set ι
t : (i : ι) → Set (α i)
f : Sigma α → β
x✝ : β
⊢ ⨆ ij ∈ s.sigma t, f ij ≤ x✝ → ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩ ≤ x✝

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_iff_comp_left (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i]
    [L.HasHomology i] [M.HasHomology i]
    [hφ : QuasiIsoAt φ i] :
    QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i

Tactic:
constructor

Result:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i

case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i

Tactic:
intro

Result:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i

Tactic:
intro

Result:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Tactic:
exact quasiIsoAt_of_comp_left φ φ' i

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_const [NeBot f] {c : β} : (f.map fun _ => c) = pure c

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
⊢ map (fun x => c) f = pure c

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
⊢ s ∈ map (fun x => c) f ↔ s ∈ pure c

Proof state:
case h
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
⊢ s ∈ map (fun x => c) f ↔ s ∈ pure c

Tactic:
by_cases h : c ∈ s <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_eq_fourierIntegral_comp_neg (f : V → E) :
    𝓕⁻ f = 𝓕 (fun x ↦ f (-x))

Proof state:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f (-y) = 𝓕 (fun x => f (-x)) y

Tactic:
change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y

Result:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f ((LinearIsometryEquiv.neg ℝ) y) = 𝓕 (f ∘ ⇑(LinearIsometryEquiv.neg ℝ)) y

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕⁻ f = 𝓕 fun x => f (-x)

Tactic:
ext y

Result:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕⁻ f y = 𝓕 (fun x => f (-x)) y

Proof state:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f ((LinearIsometryEquiv.neg ℝ) y) = 𝓕 (f ∘ ⇑(LinearIsometryEquiv.neg ℝ)) y

Tactic:
exact (fourierIntegral_comp_linearIsometry _ _ _).symm

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕⁻ f y = 𝓕 (fun x => f (-x)) y

Tactic:
rw [fourierIntegralInv_eq_fourierIntegral_neg]

Result:
case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
y : V
⊢ 𝓕 f (-y) = 𝓕 (fun x => f (-x)) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_filterMap {l : List α} {f : α → Option β} {p : β → Bool} :
    (filterMap f l).any p = l.any fun a => match f a with | some b => p b | none => false

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).any p =
    t.any fun a =>
      match f a with
      | some b => p b
      | none => false
⊢ (filterMap f (h :: t)).any p =
    (h :: t).any fun a =>
      match f a with
      | some b => p b
      | none => false

Tactic:
simp only [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).any p =
    t.any fun a =>
      match f a with
      | some b => p b
      | none => false
⊢ (match f h with
        | none => filterMap f t
        | some b => b :: filterMap f t).any
      p =
    (h :: t).any fun a =>
      match f a with
      | some b => p b
      | none => false

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → Option β
p : β → Bool
⊢ (filterMap f l).any p =
    l.any fun a =>
      match f a with
      | some b => p b
      | none => false

Tactic:
induction l with
| nil => rfl
| cons h t ih =>
  simp only [filterMap_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
⊢ (filterMap f []).any p =
    [].any fun a =>
      match f a with
      | some b => p b
      | none => false

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
h : α
t : List α
ih :
  (filterMap f t).any p =
    t.any fun a =>
      match f a with
      | some b => p b
      | none => false
⊢ (match f h with
        | none => filterMap f t
        | some b => b :: filterMap f t).any
      p =
    (h :: t).any fun a =>
      match f a with
      | some b => p b
      | none => false

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_toFinsupp (p : R[X]) : p.toFinsupp.support = p.support

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.toFinsupp.support = p.support

Tactic:
rw [support]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_prod {α : Type*} [TopologicalSpace α] {β : Type*} [TopologicalSpace β]
    {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ 𝓝[s] a) (hv : v ∈ 𝓝[t] b) :
    u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Proof state:
α : Type u_5
inst✝¹ : TopologicalSpace α
β : Type u_6
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b

Tactic:
exact prod_mem_prod hu hv

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : TopologicalSpace α
β : Type u_6
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Tactic:
rw [nhdsWithin_prod_eq]

Result:
α : Type u_5
inst✝¹ : TopologicalSpace α
β : Type u_6
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem drop_nil : ([] : List α).drop i = []

Proof state:
α : Type u
i : Nat
⊢ drop i nil = nil

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_left_distrib_sub (x y z : PGame) : (⟦x * (y - z)⟧ : Game) = ⟦x * y⟧ - ⟦x * z⟧

Proof state:
x y z : PGame
⊢ ⟦x * (y - z)⟧ = ⟦x * y⟧ - ⟦x * z⟧

Tactic:
change (⟦x * (y + -z)⟧ : Game) = ⟦x * y⟧ + -⟦x * z⟧

Result:
x y z : PGame
⊢ ⟦x * (y + -z)⟧ = ⟦x * y⟧ + -⟦x * z⟧

Proof state:
x y z : PGame
⊢ ⟦x * (y + -z)⟧ = ⟦x * y⟧ + -⟦x * z⟧

Tactic:
rw [quot_left_distrib, quot_mul_neg]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_false (h : f n = false) : cantorFunctionAux c f n = 0

Proof state:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0

Tactic:
simp [cantorFunctionAux, h]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem norm_fourierIntegral_le_integral_norm (e : AddChar 𝕜 𝕊) (μ : Measure V)
    (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) :
    ‖fourierIntegral e μ L f w‖ ≤ ∫ v : V, ‖f v‖ ∂μ

Proof state:
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

Tactic:
refine (norm_integral_le_integral_norm _).trans (le_of_eq ?_)

Result:
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ∫ (a : V), ‖e (-(L a) w) • f a‖ ∂μ = ∫ (v : V), ‖f v‖ ∂μ

Proof state:
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ∫ (a : V), ‖e (-(L a) w) • f a‖ ∂μ = ∫ (v : V), ‖f v‖ ∂μ

Tactic:
simp_rw [Circle.norm_smul]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
/-- See also `bot_eq_zero` and `bot_eq_zero'` for canonically ordered monoids. -/
lemma bot_eq_zero'' : (⊥ : α) = 0 := eq_of_forall_ge_iff fun _ ↦ by simp

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoidWithZero α
x✝ : α
⊢ ⊥ ≤ x✝ ↔ 0 ≤ x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0

Proof state:
b a : Nat
h : b < a
⊢ a ≠ 0

Tactic:
cases a

Result:
case zero
b : Nat
h : b < 0
⊢ 0 ≠ 0

case succ
b n✝ : Nat
h : b < n✝ + 1
⊢ n✝ + 1 ≠ 0

Proof state:
case zero
b : Nat
h : b < 0
⊢ 0 ≠ 0

case succ
b n✝ : Nat
h : b < n✝ + 1
⊢ n✝ + 1 ≠ 0

Tactic:
exact absurd h (Nat.not_lt_zero _)

Result:
case succ
b n✝ : Nat
h : b < n✝ + 1
⊢ n✝ + 1 ≠ 0

Proof state:
case succ
b n✝ : Nat
h : b < n✝ + 1
⊢ n✝ + 1 ≠ 0

Tactic:
apply Nat.noConfusion

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem co_support_zero [OrderedCancelAddCommMonoid Γ] [Semiring R] (g : Γ) :
    {a | ¬((0 : HahnSeries Γ R) ^ a).coeff g = 0} ⊆ {0}

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
hn : ¬(0 ^ n).coeff g = 0
h' : ¬n = 0
⊢ False

Tactic:
simp_all only [ne_eq, not_false_eq_true, zero_pow, coeff_zero, not_true_eq_false]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ ∀ (y : ℕ), ¬(0 ^ y).coeff g = 0 → y = 0

Tactic:
intro n hn

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
hn : ¬(0 ^ n).coeff g = 0
⊢ n = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
hn : ¬(0 ^ n).coeff g = 0
⊢ n = 0

Tactic:
by_contra h'

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
hn : ¬(0 ^ n).coeff g = 0
h' : ¬n = 0
⊢ False

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ {a | ¬(0 ^ a).coeff g = 0} ⊆ {0}

Tactic:
simp only [Set.subset_singleton_iff, Set.mem_setOf_eq]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
g : Γ
⊢ ∀ (y : ℕ), ¬(0 ^ y).coeff g = 0 → y = 0
-- Mathlib/Algebra/Group/EvenFunction.lean
/-- The sum of the values of an odd function is 0. -/
lemma Odd.sum_eq_zero [Fintype α] [InvolutiveNeg α] {f : α → β} (hf : f.Odd) : ∑ a, f a = 0

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : AddCommGroup β
inst✝² : NoZeroSMulDivisors ℕ β
inst✝¹ : Fintype α
inst✝ : InvolutiveNeg α
f : α → β
hf : Function.Odd f
⊢ ∑ a : α, f a = 0

Tactic:
simpa only [neg_eq_self ℕ, Finset.sum_neg_distrib, funext hf, Equiv.neg_apply] using
  Equiv.sum_comp (.neg α) f

Result:
no goals