harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_union_inter' (hs : (s ∩ mulSupport f).Finite) (ht : (t ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s ∪ t, f i) * ∏ᶠ i ∈ s ∩ t, f i) = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ t, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mulSupport f s, ← finprod_mem_inter_mulSupport f t, ←
  finprod_mem_union_inter hs ht, ← union_inter_distrib_right, finprod_mem_inter_mulSupport, ←
  finprod_mem_inter_mulSupport f (s ∩ t)]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i

Proof state:
case e_a.e_f
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i

Tactic:
rw [inter_left_comm, inter_assoc, inter_assoc, inter_self, inter_left_comm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i

Tactic:
congr 2

Result:
case e_a.e_f
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (fun i => ∏ᶠ (_ : i ∈ s ∩ t ∩ mulSupport f), f i) = fun i => ∏ᶠ (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
lemma strictMono_add_right_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono (fun x ↦ b + x)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono fun x => b + x

Tactic:
simpa [add_comm] using strictMono_add_left_of_ne_top b h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈ xs, f x = none

Proof state:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
h : filterMap f { toList := toList✝ } = #[]
⊢ ∀ (x : α✝¹), x ∈ { toList := toList✝ } → f x = none

Tactic:
simpa using h

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : Array α✝¹
h : filterMap f xs = #[]
⊢ ∀ (x : α✝¹), x ∈ xs → f x = none

Tactic:
cases xs

Result:
case mk
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
toList✝ : List α✝¹
h : filterMap f { toList := toList✝ } = #[]
⊢ ∀ (x : α✝¹), x ∈ { toList := toList✝ } → f x = none
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_append_left [LawfulBEq α] {l₁ l₂ : List α} (h : a ∈ l₁) :
    (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₁ l₂ : List α
h : a ∈ l₁
⊢ (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂

Tactic:
simp [replace_append, h]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
lemma trunc_map (p : R⟦X⟧) (n : ℕ) : (p.map f).trunc n = (p.trunc n).map f

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
⊢ trunc n ((map f) p) = Polynomial.map f (trunc n p)

Tactic:
ext m

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n m : ℕ
⊢ (trunc n ((map f) p)).coeff m = (Polynomial.map f (trunc n p)).coeff m

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n m : ℕ
⊢ (trunc n ((map f) p)).coeff m = (Polynomial.map f (trunc n p)).coeff m

Tactic:
simp [coeff_trunc, apply_ite f]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_closedBall (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r

Tactic:
rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem dvd_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : n ∣ orderOf σ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ orderOf σ

Tactic:
rw [← lcm_cycleType]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Tactic:
exact dvd_lcm h

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharTwoJEqZeroNF : W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 2 * W.b₈ - 8 * (2 * W.a₄) ^ 3 - 27 * W.b₆ ^ 2 + 9 * 0 * (2 * W.a₄) * W.b₆ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
rw [Δ, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 2 * W.b₈ - 8 * (2 * W.a₄) ^ 3 - 27 * W.b₆ ^ 2 + 9 * 0 * (2 * W.a₄) * W.b₆ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_mul_neg (a b : Int) : -a * -b = a * b

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

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_ite_eq' (i : ι) (f : ι → M) :
    𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ #s else 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j ∈ s, if j = i then f j else 0) = if i ∈ s then (↑(#s))⁻¹ • f i else 0

Tactic:
split_ifs <;> simp [expect, *]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableWithinAt.mfderivWithin (h : MDifferentiableWithinAt I I' f s x) :
    mfderivWithin I I' f s x =
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f :) ((extChartAt I x).symm ⁻¹' s ∩ range I)
        ((extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ mfderivWithin I I' f s x =
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [mfderivWithin, h, if_pos]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma polyCharpoly_natDegree [Nontrivial R] :
    (polyCharpoly φ b).natDegree = finrank R M

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).natDegree = finrank R M

Tactic:
rw [polyCharpoly, polyCharpolyAux, (charpoly.univ_monic _ _).natDegree_map,
  charpoly.univ_natDegree, finrank_eq_card_chooseBasisIndex]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.right_mem_affineSpan_of_left_ne {x y z : P} (h : Wbtw R x y z) (hne : x ≠ y) :
    z ∈ line[R, x, y]

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : x ≠ y
⊢ z ∈ affineSpan R {x, y}

Tactic:
rcases h.right_mem_image_Ici_of_left_ne hne with ⟨r, ⟨-, rfl⟩⟩

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ affineSpan R {x, y}

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ affineSpan R {x, y}

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_mul_X_sub_C_pow {p : R[X]} {a : R} {n : ℕ} (h : p ≠ 0) :
    (p * (X - C a) ^ n).rootMultiplicity a = p.rootMultiplicity a + n

Proof state:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
exact pow_rootMultiplicity_not_dvd h a

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)

Tactic:
rw [le_rootMultiplicity_iff h2, pow_add]

Result:
case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ (X - C a) ^ rootMultiplicity a p * (X - C a) ^ n ∣ p * (X - C a) ^ n

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) ≤ rootMultiplicity a p + n

case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)

Proof state:
case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ (X - C a) ^ rootMultiplicity a p * (X - C a) ^ n ∣ p * (X - C a) ^ n

Tactic:
exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

Tactic:
have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

Proof state:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) ≤ rootMultiplicity a p + n

Tactic:
rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
  dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]

Result:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem boundedBy_zero : boundedBy (0 : Set α → ℝ≥0∞) = 0

Proof state:
α : Type u_1
⊢ boundedBy 0 ≤ ⊥

Tactic:
apply boundedBy_le

Result:
no goals

Proof state:
α : Type u_1
⊢ boundedBy 0 = 0

Tactic:
rw [← coe_bot, eq_bot_iff]

Result:
α : Type u_1
⊢ boundedBy 0 ≤ ⊥
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_empty_left : image₂ f ∅ t = ∅ :=
  coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
⊢ ↑(image₂ f ∅ t) = ↑∅

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma eval_det_add_X_smul (A : Matrix n n R[X]) (M : Matrix n n R) :
    (det (A + (X : R[X]) • M.map C)).eval 0 = (det A).eval 0

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R[X]
M : Matrix n n R
⊢ (eval 0 (matPolyEquiv A) +
        eval 0 (matPolyEquiv ((algebraMap R[X] (Matrix n n R[X])) X) * matPolyEquiv (M.map ⇑C))).det =
    (eval 0 (matPolyEquiv A)).det

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X,
  mul_zero, add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R[X]
M : Matrix n n R
⊢ eval 0 (A + X • M.map ⇑C).det = eval 0 A.det

Tactic:
simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, _root_.map_mul]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R[X]
M : Matrix n n R
⊢ (eval 0 (matPolyEquiv A) +
        eval 0 (matPolyEquiv ((algebraMap R[X] (Matrix n n R[X])) X) * matPolyEquiv (M.map ⇑C))).det =
    (eval 0 (matPolyEquiv A)).det
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
    natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i

Proof state:
n m : Nat
i : Fin (n + m)
h : n ≤ ↑i
⊢ natAdd n (subNat n (Fin.cast ⋯ i) h) = i

Tactic:
simp [← cast_addNat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.alter_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : Option β → Option β} :
    Raw.Const.alter m k f = Raw₀.Const.alter ⟨m, h.size_buckets_pos⟩ k f

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
k : α
f : Option β → Option β
⊢ Raw.Const.alter m k f = (Raw₀.Const.alter ⟨m, ⋯⟩ k f).val

Tactic:
simp [Raw.Const.alter, h.size_buckets_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_twoPow {i j : Nat} (h : j < w) : (twoPow w i)[j] = decide (j = i)

Proof state:
w i j : Nat
h : j < w
⊢ i = j → i < w

Tactic:
omega

Result:
no goals

Proof state:
w i j : Nat
h : j < w
⊢ (twoPow w i)[j] = decide (j = i)

Tactic:
rw [←getLsbD_eq_getElem, getLsbD_twoPow]

Result:
w i j : Nat
h : j < w
⊢ (decide (i < w) && decide (i = j)) = decide (j = i)

Proof state:
w i j : Nat
h : j < w
⊢ (decide (i < w) && decide (i = j)) = decide (j = i)

Tactic:
simp [eq_comm]

Result:
w i j : Nat
h : j < w
⊢ i = j → i < w
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma spectrum_le (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σ ℝ≥0 a) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
⊢ x ≤ ‖a‖₊

Tactic:
simpa [cfc_id ℝ≥0 a] using apply_le_nnnorm_cfc_nnreal id a hx

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞)
    (hμt : μ t ≠ ∞) (hst : Disjoint s t) (x : G) :
    condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
⊢ condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

Tactic:
have hμst : μ (s ∪ t) ≠ ∞ :=
  ((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne

Result:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
⊢ condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
⊢ condExpIndL1 hm μ (s ∪ t) x = condExpIndL1 hm μ s x + condExpIndL1 hm μ t x

Tactic:
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x,
  condExpIndL1_of_measurableSet_of_measure_ne_top ht hμt x,
  condExpIndL1_of_measurableSet_of_measure_ne_top (hs.union ht) hμst x]

Result:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
⊢ condExpIndL1Fin hm ⋯ hμst x = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
x : G
hμst : μ (s ∪ t) ≠ ⊤
⊢ condExpIndL1Fin hm ⋯ hμst x = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x

Tactic:
exact condExpIndL1Fin_disjoint_union hs ht hμs hμt hst x

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
lemma mem_Gamma_one (γ : SL(2, ℤ)) : γ ∈ Γ(1)

Proof state:
γ : SL(2, ℤ)
⊢ γ ∈ Γ(1)

Tactic:
simp only [Gamma_one_top, Subgroup.mem_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem unzip_zipIdx_eq_prod (l : Vector α n) {m : Nat} :
    (l.zipIdx m).unzip = (l, range' m n)

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m : Nat
⊢ (l.zipIdx m).unzip = (l, range' m n)

Tactic:
simp only [zipIdx_eq_zip_range', unzip_zip]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial ↥(Submodule.span 𝕜 {x})
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Tactic:
exact ContinuousLinearMap.homothety_norm _ fun y =>
  homothety_inverse _ hx _ (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h) _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Tactic:
have hx : 0 < ‖x‖ := norm_pos_iff.mpr h

Result:
𝕜 : Type u_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Tactic:
haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h

Result:
𝕜 : Type u_1
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial ↥(Submodule.span 𝕜 {x})
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
@[mono]
protected lemma Connected.mono {H H' : G.Subgraph} (hle : H ≤ H') (hv : H.verts = H'.verts)
    (h : H.Connected) : H'.Connected

Proof state:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ H.coe ≤ (H'.copy H.verts hv H'.Adj ⋯).coe

Tactic:
rintro ⟨v, hv⟩ ⟨w, hw⟩ hvw

Result:
case mk.mk
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv✝ : H.verts = H'.verts
h : H.Connected
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : H.coe.Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ (H'.copy H.verts hv✝ H'.Adj ⋯).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
rw [← Subgraph.copy_eq H' H.verts hv H'.Adj rfl]

Result:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv✝ : H.verts = H'.verts
h : H.Connected
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : H.coe.Adj ⟨v, hv⟩ ⟨w, hw⟩
⊢ (H'.copy H.verts hv✝ H'.Adj ⋯).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
exact hle.2 hvw

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ (H'.copy H.verts hv H'.Adj ⋯).Connected

Tactic:
refine ⟨h.coe.mono ?_⟩

Result:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : H ≤ H'
hv : H.verts = H'.verts
h : H.Connected
⊢ H.coe ≤ (H'.copy H.verts hv H'.Adj ⋯).coe
-- Mathlib/Order/Atoms.lean
theorem covBy_iff_coatom_Iic (h : a ≤ b) : a ⋖ b ↔ IsCoatom (⟨a, h⟩ : Set.Iic b)

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom ⟨a, h⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem map_mul [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β]
    {f : α →+* β} : (L * M).map f = L.map f * M.map f

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
i✝ : m
j✝ : o
⊢ (L * M).map (⇑f) i✝ j✝ = (L.map ⇑f * M.map ⇑f) i✝ j✝

Tactic:
simp [mul_apply, map_sum]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
⊢ (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝ : NonAssocSemiring β
f : α →+* β
i✝ : m
j✝ : o
⊢ (L * M).map (⇑f) i✝ j✝ = (L.map ⇑f * M.map ⇑f) i✝ j✝
-- Mathlib/Analysis/MeanInequalitiesPow.lean
lemma rpow_add_rpow_le {p q : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp_pos : 0 < p)
    (hpq : p ≤ q) :
    (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
case intro.intro
p q : ℝ
hp_pos : 0 < p
hpq : p ≤ q
a b : ℝ≥0
⊢ (↑a ^ q + ↑b ^ q) ^ (1 / q) ≤ (↑a ^ p + ↑b ^ p) ^ (1 / p)

Tactic:
exact_mod_cast NNReal.rpow_add_rpow_le a b hp_pos hpq

Result:
no goals

Proof state:
p q a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
lift a to NNReal using ha

Result:
case intro
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ (↑a ^ q + b ^ q) ^ (1 / q) ≤ (↑a ^ p + b ^ p) ^ (1 / p)

Proof state:
case intro
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ (↑a ^ q + b ^ q) ^ (1 / q) ≤ (↑a ^ p + b ^ p) ^ (1 / p)

Tactic:
lift b to NNReal using hb

Result:
case intro.intro
p q : ℝ
hp_pos : 0 < p
hpq : p ≤ q
a b : ℝ≥0
⊢ (↑a ^ q + ↑b ^ q) ^ (1 / q) ≤ (↑a ^ p + ↑b ^ p) ^ (1 / p)