harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/ScottContinuity.lean
@[simp] lemma scottContinuousOn_univ : ScottContinuousOn univ f ↔ ScottContinuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ScottContinuousOn univ f ↔ ScottContinuous f

Tactic:
simp [ScottContinuousOn, ScottContinuous]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem support_bind : (p.bind f).support = ⋃ a ∈ p.support, (f a).support :=
  Set.ext fun b => by simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ b ∈ ⋃ a ∈ p.support, (f a).support

Tactic:
simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_one : (1 : R[X]).smeval x = 1 • x ^ 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 1 x = 1 • x ^ 0

Tactic:
rw [← C_1, smeval_C]

Result:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ 1 • x ^ 0 = 1 • x ^ 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ 1 • x ^ 0 = 1 • x ^ 0

Tactic:
simp only [Nat.cast_one, one_smul]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem dFrom_comp_xNextIso {i j : ι} (r : c.Rel i j) :
    C.dFrom i ≫ (C.xNextIso r).hom = C.d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i ≫ (C.xNextIso r).hom = C.d i j

Tactic:
simp [C.dFrom_eq r]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
    logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹

Tactic:
rw [← inv_logb_mul_base h₁ h₂ c, inv_inv]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.norm_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n]
    (x : EuclideanSpace 𝕜 n) : ‖x‖ = √(∑ i, ‖x i‖ ^ 2)

Proof state:
𝕜 : Type u_7
inst✝¹ : RCLike 𝕜
n : Type u_8
inst✝ : Fintype n
x : EuclideanSpace 𝕜 n
⊢ ‖x‖ = √(∑ i : n, ‖x i‖ ^ 2)

Tactic:
simpa only [Real.coe_sqrt, NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) x.nnnorm_eq

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

Proof state:
case refl
α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
⊢ ReflTransGen r a b

Tactic:
exact refl.tail hab

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
induction hbc with
| refl => exact refl.tail hab
| tail _ hcd hac => exact hac.tail hcd

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
b✝ c✝ : α
a✝ : ReflTransGen r b b✝
hcd : r b✝ c✝
hac : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝

Tactic:
exact hac.tail hcd

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_tensor {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] :
    inv (f ⊗ g) = inv f ⊗ inv g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝² : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
inst✝¹ : IsIso f
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (f ⊗ g) = inv f ⊗ inv g

Tactic:
simp [tensorHom_def ,whisker_exchange]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma integrable_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    Integrable (fun x ↦ density κ ν a x s) (ν a)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x => κ.density ν a x s) 1 (ν a) < ⊤

Tactic:
exact (eLpNorm_density_le hκν a s).trans_lt (measure_lt_top _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x => κ.density ν a x s) 1 (ν a)

Tactic:
refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => κ.density ν a x s

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ eLpNorm (fun x => κ.density ν a x s) 1 (ν a) < ⊤

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => κ.density ν a x s

Tactic:
exact measurable_density_right κ ν hs a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x => κ.density ν a x s) (ν a)

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (fun x => κ.density ν a x s) 1 (ν a)
-- Mathlib/Data/Finset/Basic.lean
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {s : Finset α} (hx : x ∈ s) :
    SizeOf.sizeOf x < SizeOf.sizeOf s

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < 1 + Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯

Tactic:
rw [Nat.add_comm]

Result:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯ + 1

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯ + 1

Tactic:
refine lt_trans ?_ (Nat.lt_succ_self _)

Result:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < sizeOf { val := val✝, nodup := nodup✝ }

Tactic:
dsimp [SizeOf.sizeOf, SizeOf.sizeOf, Multiset.sizeOf]

Result:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < 1 + Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯

Proof state:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => m._sizeOf_1) ⋯

Tactic:
exact Multiset.sizeOf_lt_sizeOf_of_mem hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
x : α
s : Finset α
hx : x ∈ s
⊢ sizeOf x < sizeOf s

Tactic:
cases s

Result:
case mk
α : Type u_1
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : val✝.Nodup
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < sizeOf { val := val✝, nodup := nodup✝ }
-- Mathlib/Data/Bool/Basic.lean
theorem lt_iff : ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Proof state:
⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem degMatrix_mulVec_apply [NonAssocSemiring R] (v : V) (vec : V → R) :
    (G.degMatrix R *ᵥ vec) v = G.degree v * vec v

Proof state:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocSemiring R
v : V
vec : V → R
⊢ (degMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v

Tactic:
rw [degMatrix, mulVec_diagonal]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
/-- Two morphisms of presheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree. -/
lemma hom_ext_yoneda {P Q : Cᵒᵖ ⥤ Type v₁} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g) :
    f = g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Result:
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ f.app X x = g.app X x

Proof state:
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ f.app X x = g.app X x

Tactic:
simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
  using congr_arg (yonedaEquiv) (h _ (yonedaEquiv.symm x))

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piRight_symm_apply (x : N) (m : ∀ i, M i) :
    (piRight R S N M).symm (fun i ↦ x ⊗ₜ m i) = x ⊗ₜ m

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ((piRight R S N M).symm fun i => x ⊗ₜ[R] m i) = x ⊗ₜ[R] m

Tactic:
simp [piRight]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_intCast_mul (x : ℝ≥0) (n : ℤ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ≥0
n : ℤ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_intCast]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem lift_eq_aleph1 {c : Cardinal.{u}} : lift.{v} c = ℵ₁ ↔ c = ℵ₁

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ_ 1 ↔ c = ℵ_ 1

Tactic:
simpa using lift_inj (b := ℵ₁)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_inv_app (n m : A) (h : n + m = 0) (X : C) :
    ((shiftFunctorCompIsoId C n m h).inv.app X)⟦n⟧' =
    ((shiftFunctorCompIsoId C m n
      (by rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel])).inv.app (X⟦n⟧))

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ 𝟙 ((shiftFunctor C n).obj ((𝟭 C).obj X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0

Tactic:
rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n m h).inv.app X) =
    (shiftFunctorCompIsoId C m n ⋯).inv.app ((shiftFunctor C n).obj X)

Tactic:
rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'),
  ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
  shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n m : A
h : n + m = 0
X : C
⊢ 𝟙 ((shiftFunctor C n).obj ((𝟭 C).obj X)) = 𝟙 ((𝟭 C).obj ((shiftFunctor C n).obj X))
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_ring_inverse (x : Rˣ) :
    HasStrictFDerivAt Ring.inverse (-mulLeftRight 𝕜 R ↑x⁻¹ ↑x⁻¹) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasStrictFDerivAt Ring.inverse (-((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

Tactic:
convert (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt

Result:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
e_4✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ -((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹ = fderiv 𝕜 Ring.inverse ↑x

Proof state:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
R : Type u_5
inst✝² : NormedRing R
inst✝¹ : HasSummableGeomSeries R
inst✝ : NormedAlgebra 𝕜 R
x : Rˣ
e_4✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ -((mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹ = fderiv 𝕜 Ring.inverse ↑x

Tactic:
exact (fderiv_inverse x).symm

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma coproducts_le_llp_rlp : (coproducts.{w} T) ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : coproducts.{w, v, u} T i
⊢ T.rlp.llp i

Tactic:
rw [coproducts_iff] at hi

Result:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : ∃ J, T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
J : Type w
hi : T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Tactic:
exact T.colimitsOfShape_discrete_le_llp_rlp J _ hi

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
intro A B i hi

Result:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : coproducts.{w, v, u} T i
⊢ T.rlp.llp i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
hi : ∃ J, T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i

Tactic:
obtain ⟨J, hi⟩ := hi

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
A B : C
i : A ⟶ B
J : Type w
hi : T.colimitsOfShape (Discrete J) i
⊢ T.rlp.llp i
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_image_eq_span_vsub_set_left_ne (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
    vectorSpan k (p '' s) = Submodule.span k ((p i -ᵥ ·) '' (p '' (s \ {i})))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))

Tactic:
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
    Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert (p i -ᵥ p i) ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert (p i -ᵥ p i) ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x => p i -ᵥ x) '' (p '' (s \ {i})))

Tactic:
simp [Submodule.span_insert_eq_span]

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_comp_hom_inv_comp [HasEqualizers V] [HasImages V] {Z : V} {i : B ≅ Z} (w) :
    imageToKernel (f ≫ i.hom) (i.inv ≫ g) w =
      (imageSubobjectCompIso _ _).hom ≫
        imageToKernel f g (by simpa using w) ≫ (kernelSubobjectIsoComp i.inv g).inv

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w =
    (imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (kernelSubobjectIsoComp i.inv g).inv

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ (kernelSubobject (i.inv ≫ g)).arrow =
    ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (kernelSubobjectIsoComp i.inv g).inv) ≫
      (kernelSubobject (i.inv ≫ g)).arrow

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ (kernelSubobject (i.inv ≫ g)).arrow =
    ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g ⋯ ≫ (kernelSubobjectIsoComp i.inv g).inv) ≫
      (kernelSubobject (i.inv ≫ g)).arrow

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ f ≫ g = 0

Tactic:
simpa using w

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_toReal {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hf : ∀ᵐ x ∂μ, f x < ∞) :
    ∫ a, (f a).toReal ∂μ = (∫⁻ a, f a ∂μ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_toReal.aestronglyMeasurable,
  lintegral_congr_ae (ofReal_toReal_ae_eq hf)]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => (f x).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
⊢ 0 ≤ᶠ[ae μ] fun x => (f x).toReal

Tactic:
exact Eventually.of_forall fun x => ENNReal.toReal_nonneg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem erase_range' :
    (range' s n).erase i =
      range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Proof state:
s n i : Nat
⊢ ((List.range' s n).erase i).toArray =
    (List.range' s (min n (i - s))).toArray ++ (List.range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))).toArray

Tactic:
simp [List.erase_range']

Result:
no goals

Proof state:
s n i : Nat
⊢ (range' s n).erase i = range' s (min n (i - s)) ++ range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))

Tactic:
simp only [← List.toArray_range', List.erase_toArray]

Result:
s n i : Nat
⊢ ((List.range' s n).erase i).toArray =
    (List.range' s (min n (i - s))).toArray ++ (List.range' (max s (i + 1)) (min s (i + 1) + n - (i + 1))).toArray
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem sum (n : ℕ) : (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν) = 1 :=
  calc
    (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν) = (X + (1 - X)) ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m ∈ Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(n.choose m)

Tactic:
simp only [bernsteinPolynomial, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = (X + (1 - X)) ^ n

Tactic:
rw [add_pow]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν =
    ∑ m ∈ Finset.range (n + 1), X ^ m * (1 - X) ^ (n - m) * ↑(n.choose m)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem_drop (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
    (L.drop i)[j] = L[i + j]'(by
      rw [Nat.add_comm]
      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h))

Proof state:
α : Type u_1
L : List α
i j : Nat
h : j < (drop i L).length
⊢ (drop i L)[j] = L[i + j]

Tactic:
rw [getElem_drop']

Result:
no goals

Proof state:
α : Type ?u.19578
L : List α
i j : Nat
h : j < (drop i L).length
⊢ j + i < L.length

Tactic:
exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)

Result:
no goals

Proof state:
α : Type ?u.19578
L : List α
i j : Nat
h : j < (drop i L).length
⊢ i + j < L.length

Tactic:
rw [Nat.add_comm]

Result:
α : Type ?u.19578
L : List α
i j : Nat
h : j < (drop i L).length
⊢ j + i < L.length
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_nat_pos_inv_mul_lt (ha : a ≠ ∞) (hb : b ≠ 0) :
    ∃ n > 0, ((n : ℕ) : ℝ≥0∞)⁻¹ * a < b

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
⊢ ∃ n > 0, (↑n)⁻¹ * a < b

Tactic:
rcases exists_nat_pos_mul_gt hb ha with ⟨n, npos, hn⟩

Result:
case intro.intro
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ ∃ n > 0, (↑n)⁻¹ * a < b

Proof state:
case intro.intro
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ ∃ n > 0, (↑n)⁻¹ * a < b

Tactic:
use n, npos

Result:
case right
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b

Proof state:
case right
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ (↑n)⁻¹ * a < b

Tactic:
rw [← ENNReal.div_eq_inv_mul]

Result:
case right
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b

Proof state:
case right
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ 0
n : ℕ
npos : n > 0
hn : a < ↑n * b
⊢ a / ↑n < b

Tactic:
exact div_lt_of_lt_mul' hn

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_mul_X : (p * X).smeval x = p.smeval x * x

Proof state:
case h_monomial
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
a : R
⊢ ((monomial n) a * X).smeval x = ((monomial n) a).smeval x * x

Tactic:
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one, pow_succ',
  mul_assoc, npow_add, smul_mul_assoc, npow_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
⊢ (p * X).smeval x = p.smeval x * x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
simp only [add_mul, smeval_add, ph, qh]
| h_monomial n a =>
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one, pow_succ',
  mul_assoc, npow_add, smul_mul_assoc, npow_one]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
p q : R[X]
ph : (p * X).smeval x = p.smeval x * x
qh : (q * X).smeval x = q.smeval x * x
⊢ ((p + q) * X).smeval x = (p + q).smeval x * x

Tactic:
simp only [add_mul, smeval_add, ph, qh]

Result:
no goals