harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_insert [DecidableEq ι] (w : ι → k) (p : ι → P) (i : ι) :
    (insert i s).weightedVSubOfPoint p (p i) w = s.weightedVSubOfPoint p (p i) w

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0

Tactic:
rw [vsub_self, smul_zero]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)

Tactic:
apply sum_insert_zero

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_singleton_self (a : α) : count a #v[a] = 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ count a { toArray := #[a], size_toArray := ⋯ } = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem eq_cons_const [AddCommMonoid M] [Semiring R] [Module R M] {r : R} (m : M) {n : M}
    {l : NF R M} (h1 : r = 0) (h2 : l.eval = n) :
    ((r, m) ::ᵣ l).eval = n

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : r = 0
h2 : l.eval = n
⊢ ((r, m) ::ᵣ l).eval = n

Tactic:
simp only [NF.eval, NF.cons] at *

Result:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : r = 0
h2 : (map (fun x => x.1 • x.2) l).sum = n
⊢ (map (fun x => x.1 • x.2) ((r, m) :: l)).sum = n

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : r = 0
h2 : (map (fun x => x.1 • x.2) l).sum = n
⊢ (map (fun x => x.1 • x.2) ((r, m) :: l)).sum = n

Tactic:
simp [h1, h2]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem map_hnot (a : α) : f (￢a) = ￢f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ f (￢a) = ￢f a

Tactic:
rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Units.lean
@[to_additive (attr := simp)]
lemma val_mem_ofUnits_iff_mem (H : Subgroup Gˣ) (x : Gˣ) : (x : G) ∈ H.ofUnits ↔ x ∈ H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : Gˣ
⊢ ↑x ∈ H.ofUnits ↔ x ∈ H

Tactic:
simp_rw [mem_ofUnits_iff_toUnits_mem, toUnits_val_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem PiToModule.fromMatrix_apply_single_one [DecidableEq ι] (A : Matrix ι ι R) (j : ι) :
    PiToModule.fromMatrix R b A (Pi.single j 1) = ∑ i : ι, A i j • b i

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (MulOpposite.op 1 • Aᵀ j) i • b i = ∑ i : ι, A i j • b i

Tactic:
simp_rw [MulOpposite.op_one, one_smul, transpose_apply]

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ((fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i

Tactic:
rw [PiToModule.fromMatrix_apply, Fintype.linearCombination_apply, Matrix.mulVec_single]

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (MulOpposite.op 1 • Aᵀ j) i • b i = ∑ i : ι, A i j • b i
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem isConjRoot_iff_mem_minpoly_rootSet {x y : S}
    (h : IsIntegral K x) : IsConjRoot K x y ↔ y ∈ (minpoly K x).rootSet S :=
  (isConjRoot_iff_mem_minpoly_aroots h).trans (by simp [rootSet])

Proof state:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ y ∈ (minpoly K x).aroots S ↔ y ∈ (minpoly K x).rootSet S

Tactic:
simp [rootSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x

Proof state:
w : Nat
x : BitVec w
⊢ x ^^^ allOnes w = ~~~x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x ^^^ allOnes w).getLsbD i = (~~~x).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x ^^^ allOnes w).getLsbD i = (~~~x).getLsbD i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_top : (⊤ : Prepartition I).iUnion = I

Proof state:
ι : Type u_1
I : Box ι
⊢ ⊤.iUnion = ↑I

Tactic:
simp [Prepartition.iUnion]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_smul {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜)
    (f : ℂⁿ → E) (c : ℂⁿ) (R : ℝⁿ) : (∯ x in T(c, R), a • f x) = a • ∯ x in T(c, R), f x

Proof state:
n : ℕ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x

Tactic:
simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasSubgroupToLpTrim_sub (hm : m ≤ m0) (f g : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim F p μ hm (f - g) =
      lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, lpMeasSubgroupToLpTrim_add,
  lpMeasSubgroupToLpTrim_neg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_polynomialZ : (W'.baseChange B).toProjective.polynomialZ =
    MvPolynomial.map f (W'.baseChange A).toProjective.polynomialZ

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toProjective.polynomialZ = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialZ

Tactic:
rw [← map_polynomialZ, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_add_cancel_of_le (h : a ≤ b) : b - a + a = b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ b - a + a = b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) = b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
exact add_tsub_cancel_of_le h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a)

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m α
⊢ f <$> x = do
    let a ← x
    pure (f a)

Tactic:
rw [← bind_pure_comp]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Function.Surjective.tprod_eq_tprod_of_hasProd_iff_hasProd {α' : Type*} [CommMonoid α']
    [TopologicalSpace α'] {e : α' → α} (hes : Function.Surjective e) (h1 : e 1 = 1) {f : β → α}
    {g : γ → α'} (h : ∀ {a}, HasProd f (e a) ↔ HasProd g a) : ∏' b, f b = e (∏' c, g c) :=
  by_cases (fun x ↦ (h.mpr x.hasProd).tprod_eq) fun hg : ¬Multipliable g ↦ by
    have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg
    simp [tprod_def, hf, hg, h1]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
α' : Type u_4
inst✝¹ : CommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)

Tactic:
have hf : ¬Multipliable f := mt (hes.multipliable_iff_of_hasProd_iff @h).1 hg

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
α' : Type u_4
inst✝¹ : CommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
hf : ¬Multipliable f
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
α' : Type u_4
inst✝¹ : CommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
hf : ¬Multipliable f
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)

Tactic:
simp [tprod_def, hf, hg, h1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_assoc {α β} (l : Array α) (f : α → Array β) (g : β → Array γ) :
    (l.flatMap f).flatMap g = l.flatMap fun x => (f x).flatMap g

Proof state:
case mk
γ : Type u_1
α : Type u_2
β : Type u_3
f : α → Array β
g : β → Array γ
l : List α
⊢ flatMap g (flatMap f { toList := l }) = flatMap (fun x => flatMap g (f x)) { toList := l }

Tactic:
simp [List.flatMap_assoc, ← toList_flatMap]

Result:
no goals

Proof state:
γ : Type u_1
α : Type u_2
β : Type u_3
l : Array α
f : α → Array β
g : β → Array γ
⊢ flatMap g (flatMap f l) = flatMap (fun x => flatMap g (f x)) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
γ : Type u_1
α : Type u_2
β : Type u_3
f : α → Array β
g : β → Array γ
l : List α
⊢ flatMap g (flatMap f { toList := l }) = flatMap (fun x => flatMap g (f x)) { toList := l }
-- Mathlib/Probability/Martingale/Centering.lean
theorem predictablePart_zero : predictablePart f ℱ μ 0 = 0

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ predictablePart f ℱ μ 0 = 0

Tactic:
simp_rw [predictablePart, Finset.range_zero, Finset.sum_empty]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_inv (hf' : ∀ x ∈ spectrum R a, f x ≠ 0)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => (f x)⁻¹) a = Ring.inverse (cfc f a)

Tactic:
rw [← val_inv_cfcUnits f a hf', ← val_cfcUnits f a hf', Ring.inverse_unit]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Ioo : (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioo]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_hasStrictDerivAt_of_tendsto_ae_left (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 a)) (ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 c)) :
    HasStrictDerivAt (fun u => ∫ x in u..b, f x) (-c) a

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f (𝓝 a) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 c)
⊢ HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a

Tactic:
simpa only [← integral_symm] using
  (integral_hasStrictDerivAt_of_tendsto_ae_right hf.symm hmeas ha).neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m

Proof state:
m : Nat
m_pos : m > 0
x✝ y x : Nat
⊢ (m + y - m) / m = y / m

Tactic:
rw [Nat.add_comm, Nat.add_sub_cancel]

Result:
no goals

Proof state:
m : Nat
m_pos : m > 0
x✝ y x : Nat
⊢ (m * (x + 1) + y) / m = x + 1 + y / m

Tactic:
rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]

Result:
m : Nat
m_pos : m > 0
x✝ y x : Nat
⊢ (x + if 0 < m ∧ m ≤ m + y then (m + y - m) / m + 1 else 0) = x + 1 + y / m

Proof state:
m : Nat
m_pos : m > 0
x y : Nat
⊢ (m * 0 + y) / m = 0 + y / m

Tactic:
simp

Result:
no goals

Proof state:
m : Nat
m_pos : m > 0
x✝ y x : Nat
⊢ (x + if 0 < m ∧ m ≤ m + y then (m + y - m) / m + 1 else 0) = x + 1 + y / m

Tactic:
simp_arith [m_pos]

Result:
m : Nat
m_pos : m > 0
x✝ y x : Nat
⊢ (m + y - m) / m = y / m

Proof state:
m : Nat
m_pos : m > 0
x y : Nat
⊢ (m * x + y) / m = x + y / m

Tactic:
match x with
| 0 => simp
| x + 1 =>
  rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
  simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem coe_iInf₂ [DecidableRel (α := α) (· ≤ ·)] (f : ∀ i, κ i → Interval α) :
    ↑(⨅ (i) (j), f i j) = ⋂ (i) (j), (f i j : Set α)

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
simp_rw [coe_iInf]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem Fintype.linearIndependent_iff_injective [Fintype ι] :
    LinearIndependent R v ↔ Injective (Fintype.linearCombination R ℕ v)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ Injective ⇑((Fintype.linearCombination R ℕ) v)

Tactic:
simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem le_mul_of_one_le_left [MulPosMono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a * b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_sigma {f : Sigma σ → X} : IsOpenMap f ↔ ∀ i, IsOpenMap fun a => f ⟨i, a⟩

Proof state:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f ⟨i, a⟩

Tactic:
simp only [isOpenMap_iff_nhds_le, Sigma.forall, Sigma.nhds_eq, map_map, comp_def]

Result:
no goals
-- Mathlib/Data/DFinsupp/Lex.lean
theorem lex_lt_of_lt [∀ i, PartialOrder (α i)] (r) [IsStrictOrder ι r] {x y : Π₀ i, α i}
    (hlt : x < y) : Pi.Lex r (· < ·) x y

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ Pi.Lex r (fun {i} x1 x2 => x1 < x2) ⇑x ⇑y

Tactic:
simp_rw [Pi.Lex, le_antisymm_iff]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
exact lex_lt_of_lt_of_preorder r hlt

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_nsmul [AddMonoid α] [StarAddMonoid α] (c : ℕ) (M : Matrix m n α) :
    (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpIndSMul_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (c : 𝕜) (x : F) :
    condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

Proof state:
α : Type u_1
F : Type u_4
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

Tactic:
rw [condExpIndSMul, condExpIndSMul, toSpanSingleton_smul',
  (toSpanSingleton ℝ x).smul_compLpL c, smul_apply]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem norm_coe_unitary [Nontrivial E] (U : unitary E) : ‖(U : E)‖ = 1

Proof state:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖↑U‖ = 1

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
  unitary.coe_star_mul_self, CStarRing.norm_one]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `r` is a positive constant, `fun x ↦ f x / r` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter. -/
lemma tendsto_div_const_atBot_of_pos (hr : 0 < r) :
    Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => f x / r) l atBot ↔ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_pos, hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_reverse (l : Array α) (f : β → α → β) (b) :
    l.reverse.foldl f b = l.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : β → α → β
b : β
⊢ foldl f b l.reverse = foldr (fun x y => f y x) b l

Tactic:
simp [foldl_eq_foldlM, foldr_eq_foldrM]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integral_exp_neg_Ioi (c : ℝ) : (∫ x : ℝ in Ioi c, exp (-x)) = exp (-c)

Proof state:
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, rexp (-x) = rexp (-c)

Tactic:
simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
@[simp]
lemma lift_eqToHom_comp_iff {R' R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R) :
    p.IsHomLift (eqToHom h ≫ f) φ ↔ p.IsHomLift f φ where
  mp hφ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : R' = R
hφ' : p.IsHomLift (eqToHom h ≫ f) φ
⊢ p.IsHomLift f φ

Tactic:
subst h

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' S : 𝒮
a b : 𝒳
φ : a ⟶ b
f : R' ⟶ S
hφ' : p.IsHomLift (eqToHom ⋯ ≫ f) φ
⊢ p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R' S : 𝒮
a b : 𝒳
φ : a ⟶ b
f : R' ⟶ S
hφ' : p.IsHomLift (eqToHom ⋯ ≫ f) φ
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma hasProduct_of_equiv_of_iso (f : α → C) (g : β → C)
    [HasProduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasProduct g

Proof state:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
this : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasProduct g

Tactic:
exact hasLimitOfIso α.symm

Result:
no goals

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasProduct g

Tactic:
have : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
  hasLimitEquivalenceComp _

Result:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
this : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasProduct g

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
this : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasProduct g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
  Discrete.natIso (fun ⟨j⟩ => iso j)

Result:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
this : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasProduct g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_neg (a b : Int) : a - -b = a + b

Proof state:
a b : Int
⊢ a - -b = a + b

Tactic:
simp [Int.sub_eq_add_neg]

Result:
no goals