harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma orthogonal_top_eq_ker (hB : B.IsRefl) :
    B.orthogonal ⊤ = LinearMap.ker B

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
hB : B.IsRefl
⊢ B.orthogonal ⊤ = ker B

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
hB : B.IsRefl
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊤ ↔ x✝ ∈ ker B

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
hB : B.IsRefl
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊤ ↔ x✝ ∈ ker B

Tactic:
simp [LinearMap.BilinForm.IsOrtho, LinearMap.ext_iff, hB.eq_iff]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma adj_homEquiv (X : Type u) (M : ModuleCat.{u} R) :
    (adj R).homEquiv X M = freeHomEquiv

Proof state:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
⊢ (adj R).homEquiv X M = freeHomEquiv

Tactic:
simp only [adj, Adjunction.mkOfHomEquiv_homEquiv]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_filter_exists (f : α → β) [Fintype β] [DecidablePred fun y => ∃ x, f x = y]
    [DecidableEq β] : (Finset.univ.filter fun y => ∃ x, f x = y) = Finset.univ.image f

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => ∃ x, f x = y
inst✝ : DecidableEq β
a✝ : β
⊢ a✝ ∈ filter (fun y => ∃ x, f x = y) univ ↔ a✝ ∈ image f univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => ∃ x, f x = y
inst✝ : DecidableEq β
⊢ filter (fun y => ∃ x, f x = y) univ = image f univ

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y => ∃ x, f x = y
inst✝ : DecidableEq β
a✝ : β
⊢ a✝ ∈ filter (fun y => ∃ x, f x = y) univ ↔ a✝ ∈ image f univ
-- Mathlib/Order/Lattice.lean
theorem sup_right_comm (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b

Tactic:
rw [sup_assoc, sup_assoc, sup_comm b]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem chain_ne_nil (r : α → α → Prop) {l : List α} :
    ∀ hl : l ≠ [], Chain r l ↔ List.Chain r (getLast l hl) l :=
  l.reverseRecOn (fun hm => hm.irrefl.elim) (by
    intro m a _H _
    rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton])

Proof state:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ List.Chain r (m.getLast hl) m
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ List.Chain r ((m ++ [a]).getLast hl✝) (m ++ [a])

Tactic:
rw [← coe_cons_eq_coe_append, chain_coe_cons, getLast_append_singleton]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (hl : l ≠ []), Chain r ↑l ↔ List.Chain r (l.getLast hl) l) →
      ∀ (hl : l ++ [a] ≠ []), Chain r ↑(l ++ [a]) ↔ List.Chain r ((l ++ [a]).getLast hl) (l ++ [a])

Tactic:
intro m a _H _

Result:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ List.Chain r (m.getLast hl) m
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ List.Chain r ((m ++ [a]).getLast hl✝) (m ++ [a])
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_one_div (h : (0 : ℝ) ∉ [[a, b]]) : ∫ x : ℝ in a..b, 1 / x = log (b / a)

Proof state:
a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv h]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_comm {n : β → α → γ} (h_comm : ∀ a b, m a b = n b a) : map₂ m f g = map₂ n g f :=
  (map₂_swap _ _ _).trans <| by simp_rw [h_comm]

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun a b => m b a) g f = map₂ n g f

Tactic:
simp_rw [h_comm]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Union.lean
theorem sup'_biUnion [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β}
    (Ht : ∀ b, (t b).Nonempty) :
    (s.biUnion t).sup' (Hs.biUnion fun b _ => Ht b) f = s.sup' Hs (fun b => (t b).sup' (Ht b) f) :=
  eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
f : β → α
inst✝ : DecidableEq β
s : Finset γ
Hs : s.Nonempty
t : γ → Finset β
Ht : ∀ (b : γ), (t b).Nonempty
c : α
⊢ (s.biUnion t).sup' ⋯ f ≤ c ↔ (s.sup' Hs fun b => (t b).sup' ⋯ f) ≤ c

Tactic:
simp [@forall_swap _ β]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x y : ℝ*} :
    ¬Infinitesimal x → 0 < x → InfiniteNeg y → InfiniteNeg (x * y) := fun hx hp hy => by
  rw [mul_comm]; exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp

Proof state:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg

Tactic:
exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp

Result:
no goals

Proof state:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (x * y).InfiniteNeg

Tactic:
rw [mul_comm]

Result:
x y : ℝ*
hx : ¬x.Infinitesimal
hp : 0 < x
hy : y.InfiniteNeg
⊢ (y * x).InfiniteNeg
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem sum_repr_mul_repr_mul (x y : M) :
    ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • B (b i) (b j)) = B x y

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
⊢ ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B x) y

Tactic:
conv_rhs => rw [← b.linearCombination_repr x, ← b.linearCombination_repr y]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
⊢ ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) =
    (B ((Finsupp.linearCombination R ⇑b) (b.repr x))) ((Finsupp.linearCombination R ⇑b) (b.repr y))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
⊢ ((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) =
    (B ((Finsupp.linearCombination R ⇑b) (b.repr x))) ((Finsupp.linearCombination R ⇑b) (b.repr y))

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
  smul_eq_mul]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.map_intNormAux [Algebra.IsSeparable K L] (x : B) :
    algebraMap A K (Algebra.intNormAux A K L B x) = Algebra.norm K (algebraMap B L x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsIntegralClosure B A L
inst✝² : FiniteDimensional K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsSeparable K L
x : B
⊢ (algebraMap A K) ((intNormAux A K L B) x) = (norm K) ((algebraMap B L) x)

Tactic:
dsimp [Algebra.intNormAux]

Result:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsIntegralClosure B A L
inst✝² : FiniteDimensional K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsSeparable K L
x : B
⊢ (algebraMap A K) (IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x)) ⋯) = (norm K) ((algebraMap B L) x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : IsFractionRing A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsIntegralClosure B A L
inst✝² : FiniteDimensional K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : Algebra.IsSeparable K L
x : B
⊢ (algebraMap A K) (IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x)) ⋯) = (norm K) ((algebraMap B L) x)

Tactic:
exact IsIntegralClosure.algebraMap_mk' _ _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_mul_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
B : Matrix m n α
h : IsUnit A.det
⊢ B * A⁻¹ * A = B

Tactic:
simp [Matrix.mul_assoc, nonsing_inv_mul A h]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem sup_prod (f₁ f₂ : Filter α) (g : Filter β) : (f₁ ⊔ f₂) ×ˢ g = (f₁ ×ˢ g) ⊔ (f₂ ×ˢ g)

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF)
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (m.insertMany l).getKey! k' = k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (m.insertMany l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.getKey!_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_eq_cons {u v : V} (p : G.Walk u v) : p.support = u :: p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support = u :: p.support.tail

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_le_iff {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
    i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j ↦ q (i.succAbove j)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_3
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (i.succAbove j)

Tactic:
simp [Pi.le_def, forall_iff_succAbove i]

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
z : 𝕜
⊢ ((p n) fun x => z) = z ^ n • p.coeff n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.symmetry (P Q : C) :
    (biprod.braiding P Q).hom ≫ (biprod.braiding Q P).hom = 𝟙 _

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ (braiding P Q).hom ≫ (braiding Q P).hom = 𝟙 (P ⊞ Q)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_const_smul (c : R) (hf : ContDiffWithinAt 𝕜 n f s x) :
    iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : R
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ ((c • iteratedFDerivWithin 𝕜 n f s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1

Tactic:
simp only [ContinuousMultilinearMap.smul_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : R
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

Tactic:
simp_rw [iteratedDerivWithin]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : R
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ ((iteratedFDerivWithin 𝕜 n (c • f) s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : R
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ ((iteratedFDerivWithin 𝕜 n (c • f) s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1

Tactic:
rw [iteratedFDerivWithin_const_smul_apply hf h hx]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_3
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : R
hf : ContDiffWithinAt 𝕜 (↑n) f s x
⊢ ((c • iteratedFDerivWithin 𝕜 n f s x) fun x => 1) = c • (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem dom_fg_iff_cod_fg {N : Type*} [L.Structure N] (f : M ≃ₚ[L] N) :
    f.dom.FG ↔ f.cod.FG

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
N : Type u_1
inst✝ : L.Structure N
f : M ≃ₚ[L] N
⊢ f.dom.FG ↔ f.cod.FG

Tactic:
rw [Substructure.fg_iff_structure_fg, f.toEquiv.fg_iff, Substructure.fg_iff_structure_fg]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp] lemma univ_inter (s : Finset α) : univ ∩ s = s

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ univ ∩ s = s

Tactic:
ext a

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem smul_eval (x) (p : MvPolynomial σ R) (s) : eval x (s • p) = s * eval x p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x) (s • p) = s * (eval x) p

Tactic:
rw [smul_eq_C_mul, (eval x).map_mul, eval_C]

Result:
no goals
-- Mathlib/Analysis/Fourier/PoissonSummation.lean
theorem SchwartzMap.tsum_eq_tsum_fourierIntegral (f : SchwartzMap ℝ ℂ) (x : ℝ) :
    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, fourierTransformCLM ℝ f n * fourier n (x : UnitAddCircle)

Proof state:
f : 𝓢(ℝ, ℂ)
x : ℝ
⊢ ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), ((fourierTransformCLM ℝ) f) ↑n * (fourier n) ↑x

Tactic:
apply Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay f.continuous one_lt_two
  (f.isBigO_cocompact_rpow (-2)) ((fourierTransformCLM ℝ f).isBigO_cocompact_rpow (-2))

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma whiskerRight_id (X Y : LocalizedMonoidal L W ε) :
    (𝟙 X) ▷ Y = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
⊢ 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_lt_inter_le [LinearOrder α] (a : α) :
    Bounded (· < ·) (s ∩ { b | a ≤ b }) ↔ Bounded (· < ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
convert @bounded_lt_inter_not_lt _ s _ a

Result:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a

Proof state:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a ≤ x✝ ↔ ¬x✝ < a

Tactic:
exact not_lt.symm

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma Icc_chartedSpaceChartAt_of_top_le {z : Set.Icc x y} (h : y ≤ z.val) :
    chartAt _ z = IccRightChart x y

Proof state:
x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
h : y ≤ ↑z
⊢ chartAt (EuclideanHalfSpace 1) z = IccRightChart x y

Tactic:
simp [Icc_chartedSpaceChartAt, reduceIte, not_lt.mpr h]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_mul_succ_self (n : ℤ) : Even (n * (n + 1))

Proof state:
n : ℤ
⊢ Even (n * (n + 1))

Tactic:
simpa [even_mul, parity_simps] using n.even_or_odd

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem exists_nested_lieIdeal_ofLe_normalizer {K : LieSubalgebra R L} (h₁ : H ≤ K)
    (h₂ : K ≤ H.normalizer) : ∃ I : LieIdeal R K, (I : LieSubalgebra R K) = ofLe h₁

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∃ I, LieIdeal.toLieSubalgebra R (↥K) I = ofLe h₁

Tactic:
rw [exists_nested_lieIdeal_coe_eq_iff]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H

Tactic:
exact fun x y hx hy => ideal_in_normalizer (h₂ hx) hy

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ⊤ f

Tactic:
simp only [top_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setLIntegral_eq_tsum' (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) (t : Set α) :
    ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :=
  calc
    ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ := h.setLIntegral_eq_tsum f t
    _ = ∑' g : G, ∫⁻ x in t ∩ g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
    _ = ∑' g : G, ∫⁻ x in g⁻¹ • (g • t ∩ s), f x ∂μ

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ

Tactic:
simp only [smul_set_inter, inv_smul_smul]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_diff_add_encard_of_subset (h : s ⊆ t) : (t \ s).encard + s.encard = t.encard

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ (t \ s).encard + s.encard = t.encard

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, diff_union_self, union_eq_self_of_subset_right h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_mkVector (p : α → Bool) (a : α) (n : Nat) :
    countP p (mkVector n a) = if p a then n else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ countP p (mkVector n a) = if p a = true then n else 0

Tactic:
simp only [mkVector_eq_mk_mkArray, countP_cast, countP_mk]

Result:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ Array.countP p (mkArray n a) = if p a = true then n else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
n : Nat
⊢ Array.countP p (mkArray n a) = if p a = true then n else 0

Tactic:
simp [Array.countP_mkArray]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_sub_right (x y z : E) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜

Tactic:
simp [sub_eq_add_neg, inner_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem findIdx?_eq_map_findFinIdx?_val {xs : Array α} {p : α → Bool} :
    xs.findIdx? p = (xs.findFinIdx? p).map (·.val)

Proof state:
α : Type u
xs : Array α
p : α → Bool
⊢ findIdx? p xs = Option.map (fun x => ↑x) (findFinIdx? p xs)

Tactic:
simp [findIdx?, findFinIdx?, findIdx?_loop_eq_map_findFinIdx?_loop_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = []

Proof state:
α✝ : Type u_1
p q : List α✝
⊢ p ++ q = [] ↔ p = [] ∧ q = []

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc]
lemma inr_f_d (n₁ n₂ : ℤ) :
    (inr φ).f n₁ ≫ (mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ (inr φ).f n₂

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
n₁ n₂ : ℤ
⊢ (inr φ).f n₁ ≫ (mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ (inr φ).f n₂

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_castSuccEmb (n : ℕ) :
    (univ : Finset (Fin (n + 1))) =
      Finset.cons (Fin.last n) (univ.map Fin.castSuccEmb) (by simp [map_eq_image])

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ last n ∉ map castSuccEmb univ

Tactic:
simp [map_eq_image]

Result:
no goals

Proof state:
n : ℕ
⊢ univ = Finset.cons (last n) (map castSuccEmb univ) ⋯

Tactic:
simp [map_eq_image]

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r • m

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ r • m = (algebraMap R A) r • m

Tactic:
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]

Result:
no goals