harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Powerset.lean
theorem powerset_card_disjiUnion (s : Finset α) :
    Finset.powerset s =
      (range (s.card + 1)).disjiUnion (fun i => powersetCard i s)
        (s.pairwise_disjoint_powersetCard.set_pairwise _)

Proof state:
case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯
⊢ a ∈ s.powerset

Tactic:
rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩

Result:
case refine_2.intro.intro
α : Type u_1
s a : Finset α
ha✝ : a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset

Proof state:
case refine_2.intro.intro
α : Type u_1
s a : Finset α
ha✝ : a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset

Tactic:
exact mem_powerset.mpr (mem_powersetCard.mp ha).1

Result:
no goals

Proof state:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s

Tactic:
exact
  ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
    mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯

Tactic:
refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩

Result:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯

case refine_2
α : Type u_1
s a : Finset α
ha : a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯
⊢ a ∈ s.powerset

Proof state:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun i => powersetCard i s) ⋯

Tactic:
rw [mem_disjiUnion]

Result:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefixOf_cons₂_self [LawfulBEq α] {a : α} :
    isPrefixOf (a::as) (a::bs) = isPrefixOf as bs

Proof state:
α : Type u_1
inst✝¹ : BEq α
as bs : List α
inst✝ : LawfulBEq α
a : α
⊢ (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs

Tactic:
simp [isPrefixOf_cons₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : List α} : lex l₁ l₂ = true ↔ l₁ < l₂

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ Lex (fun x y => x < y) l₁ l₂ ↔ l₁ < l₂

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ l₁ < l₂

Tactic:
simp only [lex_eq_true_iff_lex, decide_eq_true_eq]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : List α
⊢ Lex (fun x y => x < y) l₁ l₂ ↔ l₁ < l₂
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma comp_mk_id [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W Y Y]
    (α : SmallHom.{w} W X Y)  :
    α.comp (mk W (𝟙 Y)) = α :=
  (equiv W W.Q).injective (by simp [equiv_comp])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y Y
α : SmallHom W X Y
⊢ (equiv W W.Q) (α.comp (mk W (𝟙 Y))) = (equiv W W.Q) α

Tactic:
simp [equiv_comp]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma right_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x)
    (hx_ne_top : x ≠ ⊤) (y z : EReal) :
    (y + z) * x = y * x + z * x

Proof state:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ (y + z) * x = y * x + z * x

Tactic:
simpa only [EReal.mul_comm] using left_distrib_of_nonneg_of_ne_top hx_nonneg hx_ne_top y z

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries_sum (hf : ∀ i ∈ S, LSeriesSummable (f i) s) :
    LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Proof state:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Tactic:
simpa [LSeries, term_sum] using tsum_finsetSum hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_replicate_of_isNone (h : (f a).isNone) : findSome? f (replicate n a) = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (replicate n a) = none

Tactic:
simp [findSome?_replicate, h]

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : (f a).isNone = true
⊢ findSome? f (replicate n a) = none

Tactic:
rw [Option.isNone_iff_eq_none] at h

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (replicate n a) = none
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem factorThruImage_comp_imageUnopOp_inv :
    factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op

Tactic:
rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getValueCast? k (modifyKey k f l) = (getValueCast? k l).map f

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCast? k (modifyKey k f l) = Option.map f (getValueCast? k l)

Tactic:
simp [getValueCast?_modifyKey, hl]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toBasicOpen_mk' (s f : R) (g : Submonoid.powers s) :
    toBasicOpen R s (IsLocalization.mk' (Localization.Away s) f g) =
      const R f g (PrimeSpectrum.basicOpen s) fun _ hx => Submonoid.powers_le.2 hx g.2 :=
  (IsLocalization.lift_mk'_spec _ _ _ _).2 <| by
    rw [toOpen_eq_const, toOpen_eq_const, const_mul_cancel']

Proof state:
R : Type u
inst✝ : CommRing R
s f : R
g : ↥(Submonoid.powers s)
⊢ (ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen s))) f =
    (ConcreteCategory.hom (toOpen R (PrimeSpectrum.basicOpen s))) ↑g * const R f (↑g) (PrimeSpectrum.basicOpen s) ⋯

Tactic:
rw [toOpen_eq_const, toOpen_eq_const, const_mul_cancel']

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalComp_nil_cons {f g h i j : C} (α : f ≅ g) (β : g ≅ h) (η : h ⟶ i) (ηs : i ⟶ j) :
    α.hom ≫ (β.hom ≫ η ≫ ηs) = (α ≪≫ β).hom ≫ η ≫ ηs

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem liftAlgHom_mkAlgHom_apply (f : A →ₐ[S] B) {s : A → A → Prop}
    (w : ∀ ⦃x y⦄, s x y → f x = f y) (x) : (liftAlgHom S ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ({
          toFun := fun f' =>
            { toFun := fun x => Quot.lift ⇑↑f' ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
              commutes' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯, commutes' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ }
        x) =
    f x

Tactic:
rfl

Result:
no goals

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Tactic:
simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]

Result:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ({
          toFun := fun f' =>
            { toFun := fun x => Quot.lift ⇑↑f' ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
              commutes' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯, commutes' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ }
        x) =
    f x
-- Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean
theorem preserves_mono_of_preservesLimit {X Y : C} (f : X ⟶ Y) [PreservesLimit (cospan f f) F]
    [Mono f] : Mono (F.map f)

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
⊢ Mono (F.map f)

Tactic:
have := isLimitPullbackConeMapOfIsLimit F _ (PullbackCone.isLimitMkIdId f)

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  let_fun this := ⋯;
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono (F.map f)

Tactic:
apply PullbackCone.mono_of_isLimitMkIdId _ this

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  let_fun this := ⋯;
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)

Tactic:
simp_rw [F.map_id] at this

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono (F.map f)
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_map (f : R →+* S) (M : Matrix m n R) (i : m) :
    (M.map f).toMvPolynomial i = MvPolynomial.map f (M.toMvPolynomial i)

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
S : Type u_5
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
M : Matrix m n R
i : m
⊢ (M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)

Tactic:
simp only [toMvPolynomial, map_apply, map_sum, map_monomial]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_eq_one : (mulIndicator s f = fun _ => 1) ↔ Disjoint (mulSupport f) s

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
⊢ (s.mulIndicator f = fun x => 1) ↔ Disjoint (mulSupport f) s

Tactic:
simp only [funext_iff, mulIndicator_apply_eq_one, Set.disjoint_left, mem_mulSupport,
  not_imp_not]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Ici : (pi univ fun i ↦ Ici (x i)) = Ici x :=
  ext fun y ↦ by simp [Pi.le_def]

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ (y ∈ univ.pi fun i => Ici (x i)) ↔ y ∈ Ici x

Tactic:
simp [Pi.le_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem PosSemidef.toLinearMap₂'_zero_iff [DecidableEq n]
    {A : Matrix n n 𝕜} (hA : PosSemidef A) (x : n → 𝕜) :
    Matrix.toLinearMap₂' 𝕜 A (star x) x = 0 ↔ Matrix.toLin' A x = 0

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ (((toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ (toLin' A) x = 0

Tactic:
simpa only [toLinearMap₂'_apply', toLin'_apply] using hA.dotProduct_mulVec_zero_iff x

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative
    {K : Type*} [Field K] (f : K[X]) (a : K) :
    f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Tactic:
have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : derivative ((X - C a) * (f /ₘ (X - C a))) = derivative (f - f %ₘ (X - C a))
⊢ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
key : derivative ((X - C a) * (f /ₘ (X - C a))) = derivative (f - f %ₘ (X - C a))
⊢ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Tactic:
simpa only [derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
  modByMonic_X_sub_C_eq_C_eval] using key

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
⊢ ?m.197960

Tactic:
apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem support_map_subset (p : MvPolynomial σ R) : (map f p).support ⊆ p.support

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0

Tactic:
contrapose!

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x p = 0 → coeff x ((map f) p) = 0

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ x ∈ ((map f) p).support → x ∈ p.support

Tactic:
simp only [mem_support_iff]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ((map f) p).support ⊆ p.support

Tactic:
intro x

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ x ∈ ((map f) p).support → x ∈ p.support

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ f (coeff x p) = 0

Tactic:
rw [hx]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ f 0 = 0

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x p = 0 → f (coeff x p) = 0

Tactic:
intro hx

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ f (coeff x p) = 0

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ f 0 = 0

Tactic:
exact RingHom.map_zero f

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x p = 0 → coeff x ((map f) p) = 0

Tactic:
rw [coeff_map]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
⊢ coeff x p = 0 → f (coeff x p) = 0
-- Mathlib/Data/Finset/Card.lean
theorem card_insert_of_mem (h : a ∈ s) : #(insert a s) = #s

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s

Tactic:
rw [insert_eq_of_mem h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j)
    (a : α) : ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : α
⊢ (∏ i : ι, if p i then a else 1) = if ∃ i, p i then a else 1

Tactic:
simp [prod_ite_one univ p (by simpa using h)]

Result:
no goals

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : α
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem exists_pos_bound_of_bound {V W : Type*} [SeminormedAddCommGroup V]
    [SeminormedAddCommGroup W] {f : V → W} (M : ℝ) (h : ∀ x, ‖f x‖ ≤ M * ‖x‖) :
    ∃ N, 0 < N ∧ ∀ x, ‖f x‖ ≤ N * ‖x‖ :=
  ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), fun x =>
    calc
      ‖f x‖ ≤ M * ‖x‖ := h x
      _ ≤ max M 1 * ‖x‖

Proof state:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M * ‖x‖ ≤ (M ⊔ 1) * ‖x‖

Tactic:
gcongr

Result:
case h
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ M ⊔ 1

Proof state:
case h
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ M ⊔ 1

Tactic:
apply le_max_left

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
/-- A function `f` from `Finset α` is monotone if and only if `f s ≤ f (cons a s ha)` for all `s`
and `a ∉ s`. -/
lemma monotone_iff_forall_le_cons : Monotone f ↔ ∀ s, ∀ ⦃a⦄ (ha), f s ≤ f (cons a s ha)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)

Tactic:
classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)

Tactic:
simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂Hom_zero (f : R →+* S₂) : eval₂Hom f (0 : σ → S₂) = f.comp constantCoeff

Proof state:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
⊢ eval₂Hom f 0 = f.comp constantCoeff

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Probability/CondVar.lean
lemma condVar_smul (c : ℝ) (X : Ω → ℝ) : Var[c • X; μ | m] =ᵐ[μ] c ^ 2 • Var[X; μ | m]

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ (c • X - μ[c • X|m]) ^ 2 =ᶠ[ae μ] c ^ 2 • (X - μ[X|m]) ^ 2

Tactic:
filter_upwards [condExp_smul (m := m) c X] with ω hω

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
ω : Ω
hω : (μ[c • X|m]) ω = (c • μ[X|m]) ω
⊢ ((c • X - μ[c • X|m]) ^ 2) ω = (c ^ 2 • (X - μ[X|m]) ^ 2) ω

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ Var[c • X; μ | m] =ᶠ[ae μ] c ^ 2 • Var[X; μ | m]

Tactic:
calc
  Var[c • X; μ | m]
  _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
    rw [condVar]
    refine condExp_congr_ae ?_
    filter_upwards [condExp_smul (m := m) c X] with ω hω
    simp [hω, ← mul_sub, mul_pow]
  _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..

Result:
no goals

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
ω : Ω
hω : (μ[c • X|m]) ω = (c • μ[X|m]) ω
⊢ ((c • X - μ[c • X|m]) ^ 2) ω = (c ^ 2 • (X - μ[X|m]) ^ 2) ω

Tactic:
simp [hω, ← mul_sub, mul_pow]

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[(c • X - μ[c • X|m]) ^ 2|m] =ᶠ[ae μ] μ[c ^ 2 • (X - μ[X|m]) ^ 2|m]

Tactic:
refine condExp_congr_ae ?_

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ (c • X - μ[c • X|m]) ^ 2 =ᶠ[ae μ] c ^ 2 • (X - μ[X|m]) ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ Var[c • X; μ | m] =ᶠ[ae μ] μ[c ^ 2 • (X - μ[X|m]) ^ 2|m]

Tactic:
rw [condVar]

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[(c • X - μ[c • X|m]) ^ 2|m] =ᶠ[ae μ] μ[c ^ 2 • (X - μ[X|m]) ^ 2|m]
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_η_ε (T : D) : T ◁ η F ≫ T ◁ ε F = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ T ◁ η F ≫ T ◁ ε F = 𝟙 (T ⊗ F.obj (𝟙_ C))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_id]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} :
    (CauchySeq fun s : Finset ι => ∑ i ∈ s, f i) ↔
      ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Proof state:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b ∈ t, f b ∈ s
⊢ ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Tactic:
exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (CauchySeq fun s => ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]

Result:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Tactic:
rintro s t hst ⟨s', hs'⟩

Result:
case intro
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b ∈ t, f b ∈ s
⊢ ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b ∈ t, f b ∈ ball 0 i) ↔
    ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
simp only [ball_zero_eq, Set.mem_setOf_eq]

Result:
no goals