harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
    x.slt y = !x.ult y

Proof state:
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ x.slt y = !x.ult y

Tactic:
simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]

Result:
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ decide
      ((if (!y.msb) = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat) <
        if y.msb = true then ↑y.toNat - ↑(2 ^ w) else ↑y.toNat) =
    !y.msb

Proof state:
case true
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ decide
      ((if (!true) = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat) <
        if true = true then ↑y.toNat - ↑(2 ^ w) else ↑y.toNat) =
    !true

Tactic:
simp

Result:
case true
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ ¬↑x.toNat < ↑y.toNat - ↑(2 ^ w)

Proof state:
case true
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ ¬↑x.toNat < ↑y.toNat - ↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x.msb ≠ y.msb
⊢ decide
      ((if (!y.msb) = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat) <
        if y.msb = true then ↑y.toNat - ↑(2 ^ w) else ↑y.toNat) =
    !y.msb

Tactic:
cases y.msb <;> (simp; omega)

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem map_comp (f : α → β) (g : β → γ) : ∀ s : Computation α, map (g ∘ f) s = map g (map f s)
  | ⟨s, al⟩ => by
    apply Subtype.eq; dsimp [map]
    apply congr_arg fun f : _ → Option γ => Stream'.map f s
    ext ⟨⟩ <;> rfl

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o => Option.rec none (fun val => some (g (f val))) o) =
    (fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o

Tactic:
ext ⟨⟩ <;> rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ map (g ∘ f) ⟨s, al⟩ = map g (map f ⟨s, al⟩)

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (g (f val))) o) s =
    Stream'.map
      ((fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o) s

Tactic:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o => Option.rec none (fun val => some (g (f val))) o) =
    (fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))

Tactic:
dsimp [map]

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some (g (f val))) o) s =
    Stream'.map
      ((fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o) s
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
    X.σ j ≫ X.δ i =
      X.δ (i.pred fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) ≫
        X.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le)))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
hi : i = 0
⊢ False

Tactic:
simp only [Fin.not_lt_zero, hi] at H

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (SimplexCategory.σ (j.castLT ⋯)).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.σ j ≫ X.δ i = X.δ (i.pred ⋯) ≫ X.σ (j.castLT ⋯)

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (i.pred ⋯)).op ≫ X.map (SimplexCategory.σ (j.castLT ⋯)).op
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem _root_.Set.mulIndicator_ae_eq_one {M : Type*} [One M] {f : α → M} {s : Set α} :
    s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ f.mulSupport) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ s.mulIndicator f =ᶠ[ae μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0

Tactic:
simp [EventuallyEq, eventually_iff, ae, compl_setOf]

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ μ {a | a ∈ s ∧ ¬f a = 1} = 0 ↔ μ (s ∩ Function.mulSupport f) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
M : Type u_4
inst✝ : One M
f : α → M
s : Set α
⊢ μ {a | a ∈ s ∧ ¬f a = 1} = 0 ↔ μ (s ∩ Function.mulSupport f) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_overlap_pf (x : R) (e) (pq_pf : a + b = c) :
    x ^ e * a + x ^ e * b = x ^ e * c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
⊢ x ^ e * a + x ^ e * b = x ^ e * c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)

Tactic:
simp [mul_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = ↑(m - n)

Proof state:
m n : Nat
h : n - m = 0
⊢ subNatNat m n = ↑(m - n)

Tactic:
rw [subNatNat, h, ofNat_eq_coe]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem map_inv (a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A)

Proof state:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ (σ ↑a)⁻¹
⊢ k ∈ σ ↑a⁻¹

Tactic:
rw [Set.mem_inv] at hk

Result:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ∈ σ ↑a⁻¹

Proof state:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ≠ 0

Tactic:
simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)

Result:
no goals

Proof state:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
⊢ (σ ↑a)⁻¹ = σ ↑a⁻¹

Tactic:
refine Set.eq_of_subset_of_subset (fun k hk => ?_) fun k hk => ?_

Result:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ (σ ↑a)⁻¹
⊢ k ∈ σ ↑a⁻¹

case refine_2
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ σ ↑a⁻¹
⊢ k ∈ (σ ↑a)⁻¹

Proof state:
case refine_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : (↑k)⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹

Tactic:
rw [← Units.val_inv_eq_inv_val k] at hk

Result:
case refine_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹

Proof state:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
⊢ k ∈ σ ↑a⁻¹

Tactic:
have : k ≠ 0 := by simpa only [inv_inv] using inv_ne_zero (ne_zero_of_mem_of_unit hk)

Result:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
this : k ≠ 0
⊢ k ∈ σ ↑a⁻¹

Proof state:
case refine_1
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k⁻¹ ∈ σ ↑a
this : k ≠ 0
⊢ k ∈ σ ↑a⁻¹

Tactic:
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr this

Result:
case refine_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : (↑k)⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹

Proof state:
case refine_2.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k ∈ σ ↑a⁻¹
⊢ ↑k ∈ (σ ↑a)⁻¹

Tactic:
simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk

Result:
no goals

Proof state:
case refine_1.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k⁻¹ ∈ σ ↑a
this : ↑k ≠ 0
⊢ ↑k ∈ σ ↑a⁻¹

Tactic:
exact inv_mem_iff.mp hk

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜
hk : k ∈ σ ↑a⁻¹
⊢ k ∈ (σ ↑a)⁻¹

Tactic:
lift k to 𝕜ˣ using isUnit_iff_ne_zero.mpr (ne_zero_of_mem_of_unit hk)

Result:
case refine_2.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : Aˣ
k : 𝕜ˣ
hk : ↑k ∈ σ ↑a⁻¹
⊢ ↑k ∈ (σ ↑a)⁻¹
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
lemma _root_.integrable_cexp_quadratic (hb : 0 < b.re) (c d : ℂ) :
    Integrable (fun (x : ℝ) ↦ cexp (-b * x ^ 2 + c * x + d))

Proof state:
b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ Integrable (fun x => cexp (-b * ↑x ^ 2 + c * ↑x + d)) volume

Tactic:
have : (-b).re < 0 := by simpa using hb

Result:
b : ℂ
hb : 0 < b.re
c d : ℂ
this : (-b).re < 0
⊢ Integrable (fun x => cexp (-b * ↑x ^ 2 + c * ↑x + d)) volume

Proof state:
b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ (-b).re < 0

Tactic:
simpa using hb

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
c d : ℂ
this : (-b).re < 0
⊢ Integrable (fun x => cexp (-b * ↑x ^ 2 + c * ↑x + d)) volume

Tactic:
exact integrable_cexp_quadratic' this c d

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem hasBasis_uniformity_of_basis (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖)
    {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
    (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
      UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
simp only [iInf_uniformity]

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
exact
  hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
    (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
    (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem transfer_append {w : V} (q : G.Walk v w) (hpq) :
    (p.append q).transfer H hpq =
      (p.transfer H fun e he => hpq _ (by simp [he])).append
        (q.transfer H fun e he => hpq _ (by simp [he]))

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝ u' v' : V
p✝ : G.Walk u✝ v✝
u v : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ q.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u✝ : V
q : G.Walk u✝ w
hpq : ∀ e ∈ (nil.append q).edges, e ∈ H.edgeSet
⊢ (nil.append q).transfer H hpq = (nil.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝ u' v' : V
p✝ : G.Walk u✝ v✝
u v : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
induction p with
| nil => simp
| cons _ _ ih => simp only [Walk.transfer, cons_append, cons.injEq, heq_eq_eq, true_and, ih]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih :
  ∀ (q : G.Walk w✝ w) (hpq : ∀ e ∈ (p✝.append q).edges, e ∈ H.edgeSet),
    (p✝.append q).transfer H hpq = (p✝.transfer H ⋯).append (q.transfer H ⋯)
q : G.Walk w✝ w
hpq : ∀ e ∈ ((cons h✝ p✝).append q).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).append q).transfer H hpq = ((cons h✝ p✝).transfer H ⋯).append (q.transfer H ⋯)

Tactic:
simp only [Walk.transfer, cons_append, cons.injEq, heq_eq_eq, true_and, ih]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_pow_boole [DecidableEq α] (s : Finset α) (f : α → β) (a : α) :
    (∏ x ∈ s, f x ^ ite (a = x) 1 0) = ite (a ∈ s) (f a) 1

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
⊢ (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_const (c : ε) (h0 : p ≠ 0) (hμ : μ ≠ 0) :
    eLpNorm (fun _ : α => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / ENNReal.toReal p)

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : p = ⊤
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Proof state:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : p = ⊤
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
simp [h_top, eLpNormEssSup_const c hμ]

Result:
no goals

Proof state:
case neg
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem map_sub_rev (x y : V) : e (x - y) = e (y - x)

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (y - x)

Tactic:
rw [← neg_sub, e.map_neg]

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux

Proof state:
case refine_3

⊢ Continuous fun x => ↑x.1 * 2 * ↑x.2

Tactic:
continuity

Result:
no goals

Proof state:
case refine_5

⊢ ∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
intro x hx

Result:
case refine_5
x : ↑I × ↑I
hx : ↑x.2 = 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Proof state:
case refine_1

⊢ Continuous fun x => ↑x.2

Tactic:
continuity

Result:
no goals

Proof state:
case refine_5
x : ↑I × ↑I
hx : ↑x.2 = 1 / 2
⊢ ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
norm_num [hx, mul_assoc]

Result:
no goals

Proof state:
case refine_2

⊢ Continuous fun x => 1 / 2

Tactic:
continuity

Result:
no goals

Proof state:
⊢ Continuous reflTransSymmAux

Tactic:
refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_

Result:
case refine_1

⊢ Continuous fun x => ↑x.2

case refine_2

⊢ Continuous fun x => 1 / 2

case refine_3

⊢ Continuous fun x => ↑x.1 * 2 * ↑x.2

case refine_4

⊢ Continuous fun x => ↑x.1 * (2 - 2 * ↑x.2)

case refine_5

⊢ ∀ (x : ↑I × ↑I), ↑x.2 = 1 / 2 → ↑x.1 * 2 * ↑x.2 = ↑x.1 * (2 - 2 * ↑x.2)

Proof state:
case refine_4

⊢ Continuous fun x => ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
continuity

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
lemma jacobiTheta_eq_jacobiTheta₂ (τ : ℂ) : jacobiTheta τ = jacobiTheta₂ 0 τ :=
  tsum_congr (by simp [jacobiTheta₂_term])

Proof state:
τ : ℂ
⊢ ∀ (b : ℤ), cexp (↑π * I * ↑b ^ 2 * τ) = jacobiTheta₂_term b 0 τ

Tactic:
simp [jacobiTheta₂_term]

Result:
no goals
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem isCountablyGenerated_pure (a : α) : IsCountablyGenerated (pure a)

Proof state:
α : Type u_1
a : α
⊢ (𝓟 {a}).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_principal _

Result:
no goals

Proof state:
α : Type u_1
a : α
⊢ (pure a).IsCountablyGenerated

Tactic:
rw [← principal_singleton]

Result:
α : Type u_1
a : α
⊢ (𝓟 {a}).IsCountablyGenerated
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem spectralRadius_zero : spectralRadius 𝕜 (0 : A) = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ spectralRadius 𝕜 0 = 0

Tactic:
nontriviality A

Result:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a✝ : Nontrivial A
⊢ spectralRadius 𝕜 0 = 0

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a✝ : Nontrivial A
⊢ spectralRadius 𝕜 0 = 0

Tactic:
simp [spectralRadius]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_true' {p : α → Bool} {xs : Vector α n} :
    xs.all p = true ↔ ∀ x, x ∈ xs → p x

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Tactic:
simp only [all_mk, Array.all_eq_true']

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = true ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → p x = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_append {l₁ l₂ : List α} : (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p)

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : find? p (xs ++ l₂) = (find? p xs).or (find? p l₂)
⊢ (match p x with
    | true => some x
    | false => find? p (xs ++ l₂)) =
    (match p x with
        | true => some x
        | false => find? p xs).or
      (find? p l₂)

Tactic:
by_cases h : p x <;> simp [h, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
l₂ : List α
⊢ find? p ([] ++ l₂) = (find? p []).or (find? p l₂)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : find? p (xs ++ l₂) = (find? p xs).or (find? p l₂)
⊢ find? p (x :: xs ++ l₂) = (find? p (x :: xs)).or (find? p l₂)

Tactic:
simp only [cons_append, find?]

Result:
case cons
α : Type u_1
p : α → Bool
l₂ : List α
x : α
xs : List α
ih : find? p (xs ++ l₂) = (find? p xs).or (find? p l₂)
⊢ (match p x with
    | true => some x
    | false => find? p (xs ++ l₂)) =
    (match p x with
        | true => some x
        | false => find? p xs).or
      (find? p l₂)

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ find? p (l₁ ++ l₂) = (find? p l₁).or (find? p l₂)

Tactic:
induction l₁ with
| nil => simp
| cons x xs ih =>
  simp only [cons_append, find?]
  by_cases h : p x <;> simp [h, ih]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem injective_codRestrict {f : ι → α} {s : Set α} (h : ∀ x, f x ∈ s) :
    Injective (codRestrict f s h) ↔ Injective f

Proof state:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f

Tactic:
simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_five [CommMonoid β] (f : Fin 5 → β) :
    ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
rw [prod_univ_castSucc, prod_univ_four]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 5 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.nil {u : V} : (nil : G.Walk u u).IsTrail :=
  ⟨by simp [edges]⟩

Proof state:
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.edges.Nodup

Tactic:
simp [edges]

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
lemma Cotangent.mk_eq_zero_iff {P : Extension R S} (x : P.ker) :
    Cotangent.mk x = 0 ↔ x.val ∈ P.ker ^ 2

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
⊢ mk x = 0 ↔ ↑x ∈ P.ker ^ 2

Tactic:
simp [Cotangent.ext_iff, Ideal.toCotangent_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_ite' {p : Prop} [Decidable p] :
    (if p then none else some b).isSome = true ↔ ¬ p

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
⊢ (if p then none else some b).isSome = true ↔ ¬p

Tactic:
split <;> simpa

Result:
no goals