harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousOn_primitive_interval' (h_int : IntervalIntegrable f μ b₁ b₂)
    (ha : a ∈ [[b₁, b₂]]) : ContinuousOn (fun b => ∫ x in a..b, f x ∂μ) [[b₁, b₂]] := fun _ _ ↦ by
  refine continuousWithinAt_primitive (measure_singleton _) ?_
  rw [min_eq_right ha.1, max_eq_right ha.2]
  simpa [intervalIntegrable_iff, uIoc] using h_int

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (b₁ ⊓ b₂) (b₁ ⊔ b₂)

Tactic:
simpa [intervalIntegrable_iff, uIoc] using h_int

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (a ⊓ (b₁ ⊓ b₂)) (a ⊔ (b₁ ⊔ b₂))

Tactic:
rw [min_eq_right ha.1, max_eq_right ha.2]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (b₁ ⊓ b₂) (b₁ ⊔ b₂)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) [[b₁, b₂]] x✝¹

Tactic:
refine continuousWithinAt_primitive (measure_singleton _) ?_

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (a ⊓ (b₁ ⊓ b₂)) (a ⊔ (b₁ ⊔ b₂))
-- Mathlib/Data/Finsupp/Single.lean
theorem support_update [DecidableEq α] [DecidableEq M] :
    support (f.update a b) = if b = 0 then f.support.erase a else insert a f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Zero M
f : α →₀ M
a : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (if b = 0 then f.support.erase a else insert a f.support) = if b = 0 then f.support.erase a else insert a f.support

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Zero M
f : α →₀ M
a : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

Tactic:
dsimp only [update]

Result:
α : Type u_1
M : Type u_5
inst✝² : Zero M
f : α →₀ M
a : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (if b = 0 then f.support.erase a else insert a f.support) = if b = 0 then f.support.erase a else insert a f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Zero M
f : α →₀ M
a : α
b : M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
⊢ (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support

Tactic:
classical
dsimp only [update]
congr!

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem Code.Ok.zero {c} (h : Code.Ok c) {v} :
    Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> Code.eval c v

Proof state:
c : Code
h : c.Ok
v : List ℕ
⊢ Turing.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
rw [h, ← bind_pure_comp]

Result:
c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      Turing.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← c.eval v
    pure (Cfg.halt a)

Proof state:
c : Code
h : c.Ok
v : List ℕ
⊢ (do
      let v ← c.eval v
      Turing.eval step (Cfg.ret Cont.halt v)) =
    do
    let a ← c.eval v
    pure (Cfg.halt a)

Tactic:
congr

Result:
case e_a
c : Code
h : c.Ok
v : List ℕ
⊢ (fun v => Turing.eval step (Cfg.ret Cont.halt v)) = fun a => pure (Cfg.halt a)

Proof state:
case e_a.h
c : Code
h : c.Ok
v✝ v : List ℕ
⊢ Turing.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)

Tactic:
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

Result:
no goals

Proof state:
case e_a
c : Code
h : c.Ok
v : List ℕ
⊢ (fun v => Turing.eval step (Cfg.ret Cont.halt v)) = fun a => pure (Cfg.halt a)

Tactic:
funext v

Result:
case e_a.h
c : Code
h : c.Ok
v✝ v : List ℕ
⊢ Turing.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_algebraMap (p : K[X]) : denom (algebraMap _ (RatFunc K) p) = 1

Proof state:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ((algebraMap K[X] (RatFunc K)) p).denom = 1

Tactic:
convert denom_div p one_ne_zero <;> simp

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a ∉ Set.range f) :
    mapDomain f x a = 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ (mapDomain f x) a = 0

Tactic:
rw [mapDomain, sum_apply, sum]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ ∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) a = 0

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
x : α →₀ M
a : β
h : a ∉ Set.range f
⊢ ∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) a = 0

Tactic:
exact Finset.sum_eq_zero fun a' _ => single_eq_of_ne fun eq => h <| eq ▸ Set.mem_range_self _

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem dom_inv : r.inv.dom = r.codom

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : β
⊢ x ∈ r.inv.dom ↔ x ∈ r.codom

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.inv.dom = r.codom

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : β
⊢ x ∈ r.inv.dom ↔ x ∈ r.codom
-- Mathlib/Order/KonigLemma.lean
theorem exists_orderEmbedding_covby_of_forall_covby_finite (hfin : ∀ (a : α), {x | a ⋖ x}.Finite)
    (hb : (Ici b).Infinite) : ∃ f : ℕ ↪o α, f 0 = b ∧ ∀ i, f i ⋖ f (i+1)

Proof state:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
f : ℕ → α
hf : f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ ∃ f, f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)

Tactic:
exact ⟨OrderEmbedding.ofStrictMono f (strictMono_nat_of_lt_succ (fun i ↦ (hf.2 i).lt)), hf⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
⊢ ∃ f, f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)

Tactic:
obtain ⟨f, hf⟩ := exists_seq_covby_of_forall_covby_finite hfin hb

Result:
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : IsStronglyAtomic α
b : α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
hb : (Ici b).Infinite
f : ℕ → α
hf : f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
⊢ ∃ f, f 0 = b ∧ ∀ (i : ℕ), f i ⋖ f (i + 1)
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonneg' [SMulPosMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem unbotD_eq_self_iff {d : α} {x : WithBot α} : unbotD d x = d ↔ x = d ∨ x = ⊥

Proof state:
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = d ↔ x = ↑d ∨ x = ⊥

Tactic:
simp [unbotD_eq_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma diam_eq_one [Nontrivial α] : G.diam = 1 ↔ G = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Nontrivial α
⊢ G.diam = 1 ↔ G = ⊤

Tactic:
rw [diam, ENat.toNat_eq_iff one_ne_zero, Nat.cast_one, ediam_eq_one]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem apply_update {ι : Sort*} [DecidableEq ι] {α β : ι → Sort*} (f : ∀ i, α i → β i)
    (g : ∀ i, α i) (i : ι) (v : α i) (j : ι) :
    f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j

Proof state:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
⊢ f i (update g i v i) = update (fun k => f k (g k)) i (f i v) i

Tactic:
simp

Result:
no goals

Proof state:
case neg
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : ¬j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j

Tactic:
subst j

Result:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
⊢ f i (update g i v i) = update (fun k => f k (g k)) i (f i v) i

Proof state:
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j

Tactic:
by_cases h : j = i

Result:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j

case neg
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
h : ¬j = i
⊢ f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
-- Mathlib/Order/LiminfLimsup.lean
theorem sdiff_liminf (a : α) : a \ liminf u f = limsup (fun b => a \ u b) f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b => a \ u b) f

Tactic:
rw [← compl_inj_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b => a \ u b) f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b => a \ u b) f)ᶜ

Tactic:
simp only [sdiff_eq, limsup_compl, comp_def, compl_inf, compl_compl, sup_liminf]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma card_eq_card_isUnramifiedIn [NumberField k] [IsGalois k K] :
    Fintype.card (InfinitePlace K) =
      #{w : InfinitePlace k | w.IsUnramifiedIn K} * finrank k K +
      #({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ * (finrank k K / 2)

Proof state:
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
⊢ card (InfinitePlace K) =
    #(Finset.filter (fun w => IsUnramifiedIn K w) Finset.univ) * finrank k K +
      #(Finset.filter (fun w => IsUnramifiedIn K w) Finset.univ)ᶜ * (finrank k K / 2)

Tactic:
rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eraseLead' {c : ℕ} (fc : #f.support = c + 1) :
    #f.eraseLead.support = c

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c

Tactic:
rw [card_support_eraseLead, fc, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_eq_iff (h : IsUnit b) : a / b = c ↔ a = c * b

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a / b = c ↔ a = c * b

Tactic:
rw [div_eq_mul_inv, h.mul_inv_eq_iff_eq_mul]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma Monotone.frequently_le_map_of_frequently_le {f : R → S} (f_incr : Monotone f)
    {u : R} (freq_le : ∃ᶠ x in F, x ≤ u) :
    ∃ᶠ y in F.map f, y ≤ f u

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
⊢ ∀ᶠ (x : R) in F, u < x

Tactic:
filter_upwards [ev] with z hz

Result:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x | f u < x}
⊢ u < z

Proof state:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x | f u < x}
con : ¬u < z
⊢ False

Tactic:
apply lt_irrefl (f u) <| lt_of_lt_of_le hz <| f_incr (not_lt.mp con)

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, ¬(fun y => y ≤ f u) x
⊢ ∀ᶠ (x : R) in F, ¬(fun x => x ≤ u) x

Tactic:
simp only [not_le, not_lt] at ev freq_le ⊢

Result:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
⊢ ∀ᶠ (x : R) in F, u < x

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
⊢ ∃ᶠ (y : S) in map f F, y ≤ f u

Tactic:
refine fun ev ↦ freq_le ?_

Result:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, ¬(fun y => y ≤ f u) x
⊢ ∀ᶠ (x : R) in F, ¬(fun x => x ≤ u) x

Proof state:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x | f u < x}
⊢ u < z

Tactic:
by_contra con

Result:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
u : R
freq_le : ∃ᶠ (x : R) in F, x ≤ u
ev : ∀ᶠ (x : S) in map f F, f u < x
z : R
hz : z ∈ f ⁻¹' {x | f u < x}
con : ¬u < z
⊢ False
-- Mathlib/Order/Filter/EventuallyConst.lean
theorem eventuallyConst_pred {p : α → Prop} :
    EventuallyConst p l ↔ (∀ᶠ x in l, p x) ∨ (∀ᶠ x in l, ¬p x)

Proof state:
α : Type u_1
l : Filter α
p : α → Prop
⊢ EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x

Tactic:
simp [eventuallyConst_pred', or_comm, EventuallyEq]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma isGLB_iff_sInf_eq : IsGLB s a ↔ sInf s = a :=
  ⟨(isGLB_sInf s).unique, by rintro rfl; exact isGLB_sInf _⟩

Proof state:
α : Type u_1
inst✝ : CompleteSemilatticeInf α
s : Set α
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteSemilatticeInf α
s : Set α
a : α
⊢ sInf s = a → IsGLB s a

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : CompleteSemilatticeInf α
s : Set α
⊢ IsGLB s (sInf s)
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_eq (f : V → E) (w : V) :
    𝓕⁻ f w = ∫ v, 𝐞 ⟪v, w⟫ • f v

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
w : V
⊢ 𝓕⁻ f w = ∫ (v : V), 𝐞 (inner v w) • f v

Tactic:
simp [fourierIntegralInv, VectorFourier.fourierIntegral]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma div_pow (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c

Proof state:
case inr
a b c : ℕ
h : a ∣ b
hc : c > 0
⊢ (b / a) ^ c = b ^ c / a ^ c

Tactic:
obtain rfl | ha := a.eq_zero_or_pos

Result:
case inr.inl
b c : ℕ
hc : c > 0
h : 0 ∣ b
⊢ (b / 0) ^ c = b ^ c / 0 ^ c

case inr.inr
a b c : ℕ
h : a ∣ b
hc : c > 0
ha : a > 0
⊢ (b / a) ^ c = b ^ c / a ^ c

Proof state:
a b c : ℕ
h : a ∣ b
⊢ (b / a) ^ c = b ^ c / a ^ c

Tactic:
obtain rfl | hc := c.eq_zero_or_pos

Result:
case inl
a b : ℕ
h : a ∣ b
⊢ (b / a) ^ 0 = b ^ 0 / a ^ 0

case inr
a b c : ℕ
h : a ∣ b
hc : c > 0
⊢ (b / a) ^ c = b ^ c / a ^ c

Proof state:
case inr.inr
a b c : ℕ
h : a ∣ b
hc : c > 0
ha : a > 0
⊢ b ^ c = a ^ c * (b / a) ^ c

Tactic:
rw [← Nat.mul_pow, Nat.mul_div_cancel_left' h]

Result:
no goals

Proof state:
case inr.inr
a b c : ℕ
h : a ∣ b
hc : c > 0
ha : a > 0
⊢ (b / a) ^ c = b ^ c / a ^ c

Tactic:
refine (Nat.div_eq_of_eq_mul_right (pos_pow_of_pos c ha) ?_).symm

Result:
case inr.inr
a b c : ℕ
h : a ∣ b
hc : c > 0
ha : a > 0
⊢ b ^ c = a ^ c * (b / a) ^ c

Proof state:
case inr.inl
b c : ℕ
hc : c > 0
h : 0 ∣ b
⊢ (b / 0) ^ c = b ^ c / 0 ^ c

Tactic:
simp [Nat.zero_pow hc]

Result:
no goals

Proof state:
case inl
a b : ℕ
h : a ∣ b
⊢ (b / a) ^ 0 = b ^ 0 / a ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
lemma toENatAux_gc : GaloisConnection (↑) toENatAux := fun n x ↦ by
  cases lt_or_le x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

Proof state:
n : ℕ∞
x : Cardinal.{u_1}
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
cases lt_or_le x ℵ₀ with
| inl hx => lift x to ℕ using hx; simp
| inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

Result:
no goals

Proof state:
case inr
n : ℕ∞
x : Cardinal.{u_1}
hx : ℵ₀ ≤ x
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

Result:
no goals

Proof state:
case inl.intro
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux

Tactic:
simp

Result:
no goals

Proof state:
case inl
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
lift x to ℕ using hx

Result:
case inl.intro
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_erase_attach [DecidableEq ι] {s : Finset ι} (f : ι → α) (i : ↑s) :
    ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Tactic:
rw [← Function.Embedding.coe_subtype, ← prod_map]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x ∈ map (Embedding.subtype fun x => x ∈ s) (s.attach.erase i), f x =
    ∏ j ∈ s.erase ((Embedding.subtype fun x => x ∈ s) i), f j

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x ∈ map (Embedding.subtype fun x => x ∈ s) (s.attach.erase i), f x =
    ∏ j ∈ s.erase ((Embedding.subtype fun x => x ∈ s) i), f j

Tactic:
simp [attach_map_val]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem IsLocalization.mk' (h₁ : Localization.StrictUniversalPropertyFixedTarget L W D)
    (h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization) :
    IsLocalization L W :=
  { inverts := h₁.inverts
    isEquivalence := IsEquivalence.mk' (h₂.lift W.Q W.Q_inverts)
      (eqToIso (Localization.Construction.uniq _ _ (by
        simp only [← Functor.assoc, Localization.Construction.fac, h₂.fac, Functor.comp_id])))
      (eqToIso (h₁.uniq _ _ (by
        simp only [← Functor.assoc, h₂.fac, Localization.Construction.fac, Functor.comp_id]))) }

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ L ⋙ h₂.lift W.Q ⋯ ⋙ Localization.Construction.lift L ⋯ = L ⋙ 𝟭 D

Tactic:
simp only [← Functor.assoc, h₂.fac, Localization.Construction.fac, Functor.comp_id]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
h₁ : Localization.StrictUniversalPropertyFixedTarget L W D
h₂ : Localization.StrictUniversalPropertyFixedTarget L W W.Localization
⊢ W.Q ⋙ 𝟭 W.Localization = W.Q ⋙ Localization.Construction.lift L ⋯ ⋙ h₂.lift W.Q ⋯

Tactic:
simp only [← Functor.assoc, Localization.Construction.fac, h₂.fac, Functor.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_true_not_same  : ∀ (c b : Bool), cond c (!c) b = (!c && b)

Proof state:
⊢ ∀ (c b : Bool), (bif c then !c else b) = (!c && b)

Tactic:
decide

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem atom_pf (a : R) : a = a ^ (nat_lit 1).rawCast * (nat_lit 1).rawCast + 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma iSupIndep_genWeightSpaceOf [NoZeroSMulDivisors R M] (x : L) :
    iSupIndep fun (χ : R) ↦ genWeightSpaceOf M χ x

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
⊢ iSupIndep fun i => ((toEnd R L M) x).maxGenEigenspace i

Tactic:
exact (toEnd R L M x).independent_genEigenspace _

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
⊢ iSupIndep fun χ => genWeightSpaceOf M χ x

Tactic:
rw [LieSubmodule.iSupIndep_iff_toSubmodule]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
⊢ iSupIndep fun i => ↑(genWeightSpaceOf M i x)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
⊢ iSupIndep fun i => ↑(genWeightSpaceOf M i x)

Tactic:
dsimp [genWeightSpaceOf]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
x : L
⊢ iSupIndep fun i => ((toEnd R L M) x).maxGenEigenspace i
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem left_nonuniformWitnesses_subset (h : ¬G.IsUniform ε s t) :
    (G.nonuniformWitnesses ε s t).1 ⊆ s

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (⋯.choose, ⋯.choose).1 ⊆ s

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.1

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (⋯.choose, ⋯.choose).1 ⊆ s