harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem support_normalize : (normalize f hf0 hf).support = Function.support f :=
  Set.ext fun a => by simp [hf, mem_support_iff]

Proof state:
α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ (normalize f hf0 hf).support ↔ a ∈ Function.support f

Tactic:
simp [hf, mem_support_iff]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2_separation_compact_nhds [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
    ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
x y : X
h : x ≠ y
⊢ ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

Tactic:
simpa only [exists_prop, ← exists_and_left, and_comm, and_assoc, and_left_comm] using
  ((compact_basis_nhds x).disjoint_iff (compact_basis_nhds y)).1 (disjoint_nhds_nhds.2 h)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_neg : (∫ x in a..b, f (-x)) = ∫ x in -b..-a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, f (-x) = ∫ (x : ℝ) in -b..-a, f x

Tactic:
simpa only [zero_sub] using integral_comp_sub_left f 0

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem mem_adjoin_iff (x : E) :
    x ∈ adjoin F S ↔ ∃ r s : MvPolynomial S F,
      x = MvPolynomial.aeval Subtype.val r / MvPolynomial.aeval Subtype.val s

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
x : E
⊢ x ∈ adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s

Tactic:
rw [← mem_adjoin_range_iff, Subtype.range_coe]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_self_sub_left : neLocus (f - g) f = g.support

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f - g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_sub_right]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem abs_one_div (a : α) : |1 / a| = 1 / |a|

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ |1 / a| = 1 / |a|

Tactic:
rw [abs_div, abs_one]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
theorem rootsOfUnity.integer_power_of_ringEquiv' (g : L ≃+* L) :
    ∃ m : ℤ, ∀ t ∈ rootsOfUnity n L, g (t : Lˣ) = (t ^ m : Lˣ)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)

Tactic:
simpa using rootsOfUnity.integer_power_of_ringEquiv n g

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp] lemma alternatingMapLinearEquiv_symm_map (f : M →ₗ[R] N) :
    alternatingMapLinearEquiv.symm (map n f) = (ιMulti R n).compLinearMap f

Proof state:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ alternatingMapLinearEquiv.symm (map n f) = (ιMulti R n).compLinearMap f

Tactic:
simp only [map, LinearEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false)
    {h} :
    getKey k (insertListConst l toInsert) h =
      getKey k l (containsKey_of_containsKey_insertListConst h not_contains)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
h : containsKey k (insertListConst l toInsert) = true
⊢ getKey k (insertListConst l toInsert) h = getKey k l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
  getKey?_insertListConst_of_contains_eq_false not_contains, getKey?_eq_some_getKey]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem gcd_one {a : Int} : gcd a 1 = 1

Proof state:
a : Int
⊢ a.gcd 1 = 1

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_add_emod_self (a b : Int) : (-a + b) % a = b % a

Proof state:
a b : Int
⊢ (-a + b) % a = b % a

Tactic:
rw [Int.add_comm, add_neg_emod_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem parent_push {m : UnionFind} : m.push.parent a = m.parent a

Proof state:
a : Nat
m : UnionFind
⊢ m.push.parent a = m.parent a

Tactic:
simp [parent]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.insert_isBasis_iff_mem_closure (hI : M.Indep I) :
    M.IsBasis I (insert e I) ↔ e ∈ M.closure I

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (insert e I) ↔ e ∈ M.closure I

Tactic:
rw [hI.closure_eq_setOf_isBasis_insert, mem_setOf]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem map_apply : (map f p) b = ∑' a, if b = f a then p a else 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ (map f p) b = ∑' (a : α), if b = f a then p a else 0

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_neg (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
    integralSum (-f) vol π = -integralSum f vol π

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (-f) vol π = -integralSum f vol π

Tactic:
simp only [integralSum, Pi.neg_apply, (vol _).map_neg, Finset.sum_neg_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem take_mk (a : Array α) (h : a.size = n) (m) :
    (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl

Proof state:
α : Type ?u.17462
n : Nat
a : Array α
h : a.size = n
m : Nat
⊢ (a.take m).size = min m n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma preimage_iSup {ι} (U : ι → Opens Y) : f ⁻¹ᵁ iSup U = ⨆ i, f ⁻¹ᵁ U i :=
  Opens.ext (by simp)

Proof state:
X Y : Scheme
f : X.Hom Y
ι : Sort u_1
U : ι → Y.Opens
⊢ ↑(f ⁻¹ᵁ iSup U) = ↑(⨆ i, f ⁻¹ᵁ U i)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α}
    {v : β} :
    get! (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then v else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
k a : α
v : β
⊢ get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else get! m a

Tactic:
simp_to_model [insertIfNew] using List.getValue!_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem BitVec.bne_to_beq (a b : BitVec w) : (a != b) = (!(a == b))

Proof state:
w : Nat
a b : BitVec w
⊢ (a != b) = !a == b

Tactic:
simp [bne]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Order.lean
theorem order_ne_top_of_isPreconnected {x y : 𝕜} (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U)
    (h₂x : (hf x h₁x).order ≠ ⊤) :
    (hf y hy).order ≠ ⊤ :=
  (hf.exists_order_ne_top_iff_forall ⟨nonempty_of_mem h₁x, hU⟩).1 (by use ⟨x, h₁x⟩) ⟨y, hy⟩

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x y : 𝕜
hU : IsPreconnected U
h₁x : x ∈ U
hy : y ∈ U
h₂x : ⋯.order ≠ ⊤
⊢ ∃ u, ⋯.order ≠ ⊤

Tactic:
use ⟨x, h₁x⟩

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem splitWrtComposition_flatten (L : List (List α)) (c : Composition L.flatten.length)
    (h : map length L = c.blocks) : splitWrtComposition (flatten L) c = L

Proof state:
α : Type u_1
L : List (List α)
c : Composition L.flatten.length
h : map length L = c.blocks
⊢ L.flatten.splitWrtComposition c = L

Tactic:
simp only [eq_self_iff_true, and_self_iff, eq_iff_flatten_eq, flatten_splitWrtComposition,
  map_length_splitWrtComposition, h]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem map_roots [IsDomain S] : (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Proof state:
R : Type u_1
S : Type u_2
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Tactic:
rw [roots, map_toPoly]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_zero : content (0 : R[X]) = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ content 0 = 0

Tactic:
rw [← C_0, content_C, normalize_zero]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem pair {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β} {g : α → γ}
    (hf : Primrec f) (hg : Primrec g) : Primrec fun a => (f a, g a) :=
  ((casesOn1 0
            (Nat.Primrec.succ.comp <|
              .pair (Nat.Primrec.pred.comp hf) (Nat.Primrec.pred.comp hg))).comp
        (@Primcodable.prim α _)).of_eq
    fun n => by cases @decode α _ n <;> simp [encodek]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n =>
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a => (f a, g a)) (decode n))

Tactic:
cases @decode α _ n <;> simp [encodek]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a) = f a

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), F (of a) = f a

Tactic:
simpa only [funext_iff] using lift.symm.bijective.existsUnique f

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_natCast' (n : ℕ) {_ : Decidable (n : PartENat).Dom} :
    toWithTop (n : PartENat) = n

Proof state:
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ (↑n).toWithTop = ↑n

Tactic:
rw [toWithTop_natCast n]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_add : u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
u v w : m → α
⊢ u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

Tactic:
simp [dotProduct, mul_add, Finset.sum_add_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_zero : (0#w).getLsbD i = false

Proof state:
w i : Nat
⊢ (0#w).getLsbD i = false

Tactic:
simp [getLsbD]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.exists_smul_eq_mul
    (a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ nonZeroDivisors S) :
    ∃ᵉ (c : S) (d ≠ (0 : R)), d • a = b * c :=
  have ⟨r, hr, s, h⟩ := hRb.exists_nonzero_dvd hb
  ⟨s * a, r, hr, by rw [Algebra.smul_def, h, mul_assoc]⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : b ∈ nonZeroDivisors S
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ r • a = b * (s * a)

Tactic:
rw [Algebra.smul_def, h, mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_const : eval assign (.const val) = val

Proof state:
assign : Assignment
w✝ : Nat
val : BitVec w✝
⊢ eval assign (const val) = val

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_ball_one_iff : a ∈ ball (1 : E) r ↔ ‖a‖ < r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ ball 1 r ↔ ‖a‖ < r

Tactic:
rw [mem_ball, dist_one_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_mul_const {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0):
    logDeriv (fun z => f z * a) x = logDeriv f x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
a : 𝕜'
ha : a ≠ 0
⊢ logDeriv (fun z => f z * a) x = logDeriv f x

Tactic:
simp only [logDeriv_apply, deriv_mul_const_field, mul_div_mul_right _ _ ha]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
lemma biprod.ext_to_iff {f g : Z ⟶ X ⊞ Y} :
    f = g ↔ f ≫ biprod.fst = g ≫ biprod.fst ∧ f ≫ biprod.snd = g ≫ biprod.snd

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
Z : C
f g : Z ⟶ X ⊞ Y
⊢ f = g ↔ f ≫ fst = g ≫ fst ∧ f ≫ snd = g ≫ snd

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Order/LeftRight.lean
theorem nhdsLE_sup_nhdsGE (a : α) : 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive three_nsmul]
lemma pow_three (a : M) : a ^ 3 = a * (a * a)

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * (a * a)

Tactic:
rw [pow_succ', pow_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_some_getValue! [BEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α}
    (h : containsKey a l = true) : getValue? a l = some (getValue! a l)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
a : α
h : containsKey a l = true
⊢ getValue? a l = some (getValue! a l)

Tactic:
rw [getValue?_eq_some_getValue h, getValue_eq_getValue!]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem roots_C_mul_X_sub_C (b : R) (ha : a ≠ 0) : (C a * X - C b).roots = {a⁻¹ * b}

Proof state:
R : Type u
a : R
inst✝ : Field R
b : R
ha : a ≠ 0
⊢ (C a * X - C b).roots = {a⁻¹ * b}

Tactic:
simp [roots_C_mul_X_sub_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonneg_iff (hx : 0 < x) : 0 ≤ logb b x ↔ 1 ≤ x

Proof state:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 ≤ logb b x ↔ 1 ≤ x

Tactic:
rw [← not_lt, logb_neg_iff hb hx, not_lt]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem closedBall_eq_univ_of_half_period_le (hp : p ≠ 0) (x : AddCircle p) {ε : ℝ}
    (hε : |p| / 2 ≤ ε) : closedBall x ε = univ :=
  eq_univ_iff_forall.mpr fun x => by
    simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

Proof state:
p : ℝ
hp : p ≠ 0
x✝ : AddCircle p
ε : ℝ
hε : |p| / 2 ≤ ε
x : AddCircle p
⊢ x ∈ closedBall x✝ ε

Tactic:
simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma neg_of_Z_eq_zero' {P : Fin 3 → R} (hPz : P z = 0) : W'.neg P = ![P x, -P y, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.neg P = ![P x, -P y, 0]

Tactic:
rw [neg, negY_of_Z_eq_zero hPz, hPz]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type*} [AddCommGroup V] [Module ℝ V]
    [MeasurableSpace V] {W : Type*} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ)
    (μ : Measure V) (f : V → E) (w : W) :
    VectorFourier.fourierIntegral fourierChar μ L f w =
      ∫ v : V, Complex.exp (↑(-2 * π * L v w) * Complex.I) • f v ∂μ

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_3
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ VectorFourier.fourierIntegral 𝐞 μ L f w = ∫ (v : V), Complex.exp (↑(-2 * π * (L v) w) * Complex.I) • f v ∂μ

Tactic:
simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, Real.fourierChar_apply, mul_neg,
  neg_mul]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_uIcc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    update f i '' uIcc (f i) b = uIcc f (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' uIcc (f i) b = uIcc f (update f i b)

Tactic:
simpa using image_update_uIcc f i (f i) b

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem X_pow_mem_lifts (f : R →+* S) (n : ℕ) : (X ^ n : S[X]) ∈ lifts f :=
  ⟨X ^ n, by
    simp only [coe_mapRingHom, map_pow, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
      map_X, and_self_iff]⟩

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (mapRingHom f) (X ^ n) = X ^ n

Tactic:
simp only [coe_mapRingHom, map_pow, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  map_X, and_self_iff]

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem strictMono_map_iff {f : α → β} : StrictMono (WithTop.map f) ↔ StrictMono f :=
  strictMono_iff.trans <| by simp [StrictMono, coe_lt_top]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x < map f ⊤) ↔ StrictMono f

Tactic:
simp [StrictMono, coe_lt_top]

Result:
no goals
-- Mathlib/Data/List/Scan.lean
theorem scanl_cons : scanl f b (a :: l) = [b] ++ scanl f (f b a) l

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
a : α
l : List α
⊢ scanl f b (a :: l) = [b] ++ scanl f (f b a) l

Tactic:
simp only [scanl, eq_self_iff_true, singleton_append, and_self_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem left_mem_Ico : a ∈ Ico a b ↔ a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
simp only [mem_Ico, true_and, le_refl]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem one_mul : (1 : MvPowerSeries σ R) * φ = φ :=
  ext fun n => by simpa using coeff_add_monomial_mul 0 n φ 1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (1 * φ) = (coeff R n) φ

Tactic:
simpa using coeff_add_monomial_mul 0 n φ 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_none [LawfulBEq α] (h : m.WF) {a : α} : ¬a ∈ m → m.get? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
⊢ ¬a ∈ m → m.get? a = none

Tactic:
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_map_of_map_ne_zero_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]}
    (f : A →+* B) (h : p.map f ≠ 0) (hroots : p.roots.card = p.natDegree) :
    p.roots.map f = (p.map f).roots :=
  eq_of_le_of_card_le (map_roots_le h) <| by
    simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans natDegree_map_le

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
hroots : p.roots.card = p.natDegree
⊢ (map f p).roots.card ≤ (Multiset.map (⇑f) p.roots).card

Tactic:
simpa only [Multiset.card_map, hroots] using (p.map f).card_roots'.trans natDegree_map_le

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem t_pow_smul_eq_unitsSMul (u : ℤˣ) (w : NormalWord d) :
    (t ^ (u : ℤ) : HNNExtension G A B φ) • w = unitsSMul φ u w

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ t ^ ↑u • w = unitsSMul φ u w

Tactic:
rcases Int.units_eq_one_or u with (rfl | rfl) <;>
  simp [instHSMul, SMul.smul, MulAction.toEndHom, Equiv.Perm.inv_def]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_reverse' :
    haveI := prim H
    Primrec (@List.reverse β) :=
  letI := prim H
  (list_foldl' H .id (const []) <| to₂ <| ((list_cons' H).comp snd fst).comp snd).of_eq
    (suffices ∀ l r, List.foldl (fun (s : List β) (b : β) => b :: s) r l = List.reverseAux l r from
      fun l => this l []
    fun l => by induction l <;> simp [*, List.reverseAux])

Proof state:
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n => encode (decode n)
this : Primcodable (List β) := prim H
l : List β
⊢ ∀ (r : List β), List.foldl (fun s b => b :: s) r l = l.reverseAux r

Tactic:
induction l <;> simp [*, List.reverseAux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

Proof state:
a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)

Tactic:
cases a <;> cases b <;> decide

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_prod_singleton (s : Set α) (b : β) : Nat.card (s ×ˢ {b}) = Nat.card s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ Nat.card ↑(s ×ˢ {b}) = Nat.card ↑s

Tactic:
rw [prod_singleton, Nat.card_image_of_injective (Prod.mk.inj_right b)]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem smulRight_one_eq_iff {f f' : M₂} :
    smulRight (1 : R₁ →L[R₁] R₁) f = smulRight (1 : R₁ →L[R₁] R₁) f' ↔ f = f'

Proof state:
R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
f f' : M₂
⊢ smulRight 1 f = smulRight 1 f' ↔ f = f'

Tactic:
simp only [ContinuousLinearMap.ext_ring_iff, smulRight_apply, one_apply, one_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_comp_mul_right_Ioi (g : ℝ → E) (a : ℝ) {b : ℝ} (hb : 0 < b) :
    (∫ x in Ioi a, g (x * b)) = b⁻¹ • ∫ x in Ioi (a * b), g x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi a, g (x * b) = b⁻¹ • ∫ (x : ℝ) in Ioi (a * b), g x

Tactic:
simpa only [mul_comm] using integral_comp_mul_left_Ioi g a hb

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem toTensor_ι (m : M) : FreeAlgebra.toTensor (FreeAlgebra.ι R m) = TensorAlgebra.ι R m

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ toTensor (ι R m) = (TensorAlgebra.ι R) m

Tactic:
simp [toTensor]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma monotoneOn_of_sub_one_le (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) ≤ f a) → MonotoneOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using monotoneOn_of_pred_le hs (f := f)

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_right_comm (s t u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t

Tactic:
simp_rw [convexJoin_assoc, convexJoin_comm]

Result:
no goals