harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Rank/Finite.lean
/-- A union of finitely many `IsRkFinite` sets is `IsRkFinite`. -/
lemma IsRkFinite.iUnion {ι : Type*} [Finite ι] {Xs : ι → Set α} (h : ∀ i, M.IsRkFinite (Xs i)) :
    M.IsRkFinite (⋃ i, Xs i)

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ (⋃ i, Xs i) ∩ M.E ⊆ M.closure (⋃ i, Is i)

Tactic:
rw [iUnion_inter, iUnion_subset_iff]

Result:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ i, Is i)

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ ∀ (i : ι), Xs i ∩ M.E ⊆ M.closure (⋃ i, Is i)

Tactic:
exact fun i ↦ (hIs i).isBasis_inter_ground.subset_closure.trans <| M.closure_subset_closure <|
  subset_iUnion ..

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs i)

Tactic:
have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_isBasis' (hIs i)

Result:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.IsRkFinite (⋃ i, Xs i)

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.IsRkFinite (⋃ i, Xs i)

Tactic:
refine isRkFinite_inter_ground_iff.1 <| (M.isRkFinite_of_finite hfin).closure.subset ?_

Result:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ (⋃ i, Xs i) ∩ M.E ⊆ M.closure (⋃ i, Is i)

Proof state:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs i)

Tactic:
choose Is hIs using fun i ↦ M.exists_isBasis' (Xs i)

Result:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs i)
-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_zero : single a b = 0 ↔ b = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ single a b = 0 ↔ b = 0

Tactic:
simp [DFunLike.ext_iff, single_eq_set_indicator]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem comp_id_right (B : BilinForm R M) (l : M →ₗ[R] M) :
    B.comp l LinearMap.id = B.compLeft l

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
l : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp l id) x✝) y✝ = ((B.compLeft l) x✝) y✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
l : M →ₗ[R] M
⊢ B.comp l id = B.compLeft l

Tactic:
ext

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
l : M →ₗ[R] M
x✝ y✝ : M
⊢ ((B.comp l id) x✝) y✝ = ((B.compLeft l) x✝) y✝
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem tsum_mul_left (a : ℝ≥0) (f : α → ℝ≥0) : ∑' x, a * f x = a * ∑' x, f x :=
  NNReal.eq <| by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]

Proof state:
α : Type u_1
a : ℝ≥0
f : α → ℝ≥0
⊢ ↑(∑' (x : α), a * f x) = ↑(a * ∑' (x : α), f x)

Tactic:
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRightAux_of {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) :
    η ▷ h = (Iso.refl _).hom ≫ η ▷ h ≫ (Iso.refl _).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ η ▷ h = (Iso.refl (f ≫ h)).hom ≫ η ▷ h ≫ (Iso.refl (g ≫ h)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a * b)⁻¹ = a⁻¹ / b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean
theorem dens_recurrence {gp : Pair K} {ppredB predB : K}
    (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_den_eq : g.dens n = ppredB)
    (succ_nth_den_eq : g.dens (n + 1) = predB) :
    g.dens (n + 2) = gp.b * predB + gp.a * ppredB

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_den_eq : g.dens n = ppredB
succ_nth_den_eq : g.dens (n + 1) = predB
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredB

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.b = ppredB :=
  exists_conts_b_of_den nth_den_eq

Result:
case intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b

Proof state:
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b

Tactic:
rw [den_eq_conts_b, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]

Result:
no goals

Proof state:
case intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
    ∃ conts, g.conts (n + 1) = conts ∧ conts.b = predB :=
  exists_conts_b_of_den succ_nth_den_eq

Result:
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem tendsto_bdd_div_atTop_nhds_zero {f g : α → 𝕜} {b B : 𝕜}
    (hb : ∀ᶠ x in l, b ≤ f x) (hB : ∀ᶠ x in l, f x ≤ B) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x / g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact bdd_le_mul_tendsto_zero hb hB hg.inv_tendsto_atTop

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
lemma FiniteDimensional.exists_mul_eq_one (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1

Proof state:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
this : Surjective ⇑(LinearMap.mulLeft F x)
⊢ ∃ y, x * y = 1

Tactic:
exact this 1

Result:
no goals

Proof state:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ ∃ y, x * y = 1

Tactic:
have : Function.Surjective (LinearMap.mulLeft F x) :=
  LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)

Result:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
this : Surjective ⇑(LinearMap.mulLeft F x)
⊢ ∃ y, x * y = 1
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem algebraMap_apply {r : R} :
    algebraMap R (MvPowerSeries σ A) r = C σ A (algebraMap R A r)

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ((map σ (algebraMap R A)).comp (C σ R)) r = (C σ A) ((algebraMap R A) r)

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R (MvPowerSeries σ A)) r = (C σ A) ((algebraMap R A) r)

Tactic:
change (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) r = _

Result:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ((map σ (algebraMap R A)).comp (C σ R)) r = (C σ A) ((algebraMap R A) r)
-- Mathlib/LinearAlgebra/SModEq.lean
theorem sub_mem : x ≡ y [SMOD U] ↔ x - y ∈ U

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U

Tactic:
rw [SModEq.def, Submodule.Quotient.eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem sup_le (K₁ K₂ : Compacts G) : μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂

Proof state:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂

Tactic:
simpa [← toNNReal_add] using μ.sup_le' _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_some {a b : α} : a ∈ some b ↔ b = a

Proof state:
α : Type u_1
a b : α
⊢ a ∈ some b ↔ b = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ 0 < a - b ↔ b < a

Tactic:
rw [tsub_pos_iff_not_le, not_le]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem image_mul_left' :
    image (fun b => a⁻¹ * b) t = preimage t (fun b => a * b) (mul_right_injective _).injOn

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
t : Finset α
a : α
⊢ image (fun b => a⁻¹ * b) t = t.preimage (fun b => a * b) ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma llr_self (μ : Measure α) [SigmaFinite μ] : llr μ μ =ᵐ[μ] 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
a : α
ha : μ.rnDeriv μ a = 1
⊢ llr μ μ a = 0 a

Tactic:
simp [llr, ha]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ llr μ μ =ᶠ[ae μ] 0

Tactic:
filter_upwards [μ.rnDeriv_self] with a ha using by simp [llr, ha]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem Convex.mem_Icc (h : x ≤ y) :
    z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x ≤ y
⊢ z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
simp only [← segment_eq_Icc h, segment, mem_setOf_eq, smul_eq_mul, exists_and_left]

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_union_empty_singleton [DecidableEq α] (s : Finset α) :
    Finset.fold (· ∪ ·) ∅ singleton s = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x1 x2 => x1 ∪ x2) ∅ singleton s = s

Tactic:
induction' s using Finset.induction_on with a s has ih

Result:
case empty
α : Type u_1
inst✝ : DecidableEq α
⊢ fold (fun x1 x2 => x1 ∪ x2) ∅ singleton ∅ = ∅

case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 => x1 ∪ x2) ∅ singleton s = s
⊢ fold (fun x1 x2 => x1 ∪ x2) ∅ singleton (insert a s) = insert a s

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
⊢ fold (fun x1 x2 => x1 ∪ x2) ∅ singleton ∅ = ∅

Tactic:
simp only [fold_empty]

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 => x1 ∪ x2) ∅ singleton s = s
⊢ fold (fun x1 x2 => x1 ∪ x2) ∅ singleton (insert a s) = insert a s

Tactic:
rw [fold_insert has, ih, insert_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    support (C x * X ^ k + C y * X ^ m) = {k, m}

Proof state:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (C x * X ^ k + C y * X ^ m).support = {k, m}

Tactic:
apply subset_antisymm (support_binomial' k m x y)

Result:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ (C x * X ^ k + C y * X ^ m).support

Proof state:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ (C x * X ^ k + C y * X ^ m).support

Tactic:
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
  coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
  add_zero, Ne, hx, hy, not_false_eq_true, and_true]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem left_lt_lineMap_iff_lt (h : 0 < r) : a < lineMap a b r ↔ a < b :=
  Iff.trans (by rw [lineMap_apply_zero]) (lineMap_lt_lineMap_iff_of_lt h)

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r : k
h : 0 < r
⊢ a < (lineMap a b) r ↔ (lineMap a b) 0 < (lineMap a b) r

Tactic:
rw [lineMap_apply_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_mul_sq_norm (hb : 0 < b.re) :
    ∫ v : V, cexp (- b * ‖v‖^2) = (π / b) ^ (Module.finrank ℝ V / 2 : ℂ)

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2) = (↑π / b) ^ (↑(Module.finrank ℝ V) / 2)

Tactic:
simpa using integral_cexp_neg_mul_sq_norm_add hb 0 (0 : V)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem borel_eq_generateFrom_Ici_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ici (a : ℝ)})

Proof state:
⊢ borel ℝ = generateFrom (⋃ a, {Ici ↑a})

Tactic:
rw [borel_eq_generateFrom_Iio_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]

Result:
⊢ generateFrom (range fun a => Iio ↑a) = generateFrom (range fun a => Ici ↑a)

Proof state:
⊢ generateFrom (range fun a => Iio ↑a) = generateFrom (range fun a => Ici ↑a)

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
rintro _ ⟨q, rfl⟩ <;>
dsimp only <;>
[rw [← compl_Ici]; rw [← compl_Iio]] <;>
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_add_goldConj : φ + ψ = 1

Proof state:
⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1

Tactic:
ring

Result:
no goals

Proof state:
⊢ φ + ψ = 1

Tactic:
rw [goldenRatio, goldenConj]

Result:
⊢ (1 + √5) / 2 + (1 - √5) / 2 = 1
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
lemma summable_partition {α β : Type*} {f : β → ℝ} (hf : 0 ≤ f) {s : α  → Set β}
    (hs : ∀ i, ∃! j, i ∈ s j) : Summable f ↔
      (∀ j, Summable fun i : s j ↦ f i) ∧ Summable fun j ↦ ∑' i : s j, f i

Proof state:
α : Type u_3
β : Type u_4
f : β → ℝ
hf : 0 ≤ f
s : α → Set β
hs : ∀ (i : β), ∃! j, i ∈ s j
⊢ Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i

Tactic:
simpa only [← (Set.sigmaEquiv s hs).summable_iff] using summable_sigma_of_nonneg (fun _ ↦ hf _)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem spanSingleton_mul_inv {x : K} (hx : x ≠ 0) :
    spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ x * (spanSingleton R₁⁰ x)⁻¹ = 1

Tactic:
rw [spanSingleton_inv, spanSingleton_mul_spanSingleton, mul_inv_cancel₀ hx, spanSingleton_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Basic.lean
theorem isUniformEmbedding_bot_of_pairwise_le_dist {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α}
    (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) :
    @IsUniformEmbedding _ _ ⊥ (by infer_instance) f :=
  isUniformEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

Proof state:
α : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s : Set γ
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y => ε ≤ dist (f x) (f y)
⊢ UniformSpace α

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y => ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y => (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_sub [Fintype n] (A : Matrix m n α) (x y : n → α) :
    A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
⊢ A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x - y)) x✝ = (A *ᵥ x - A *ᵥ y) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x - y)) x✝ = (A *ᵥ x - A *ᵥ y) x✝

Tactic:
apply dotProduct_sub

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toMultiset_inf : toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g :=
  Multiset.toDFinsupp_injective <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset (f ⊓ g)) = Multiset.toDFinsupp (toMultiset f ∩ toMultiset g)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem piMap {ι} [Fintype ι] {α β : ι → Type*} [∀ i, PseudoEMetricSpace (α i)]
    [∀ i, PseudoEMetricSpace (β i)] (f : ∀ i, α i → β i) (hf : ∀ i, Isometry (f i)) :
    Isometry (Pi.map f) := fun x y => by
  simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]

Proof state:
ι : Type u_4
inst✝² : Fintype ι
α : ι → Type u_2
β : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist (Pi.map f x) (Pi.map f y) = edist x y

Tactic:
simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isGE_of_iso (n : ℤ) [K.IsGE n] : L.IsGE n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsGE n
⊢ L.IsGE n

Tactic:
apply isSupported_of_iso e

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem tsub_encard_le_encard_diff (s t : Set α) : s.encard - t.encard ≤ (s \ t).encard

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

Tactic:
apply encard_le_encard_diff_add_encard

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ s.encard - t.encard ≤ (s \ t).encard

Tactic:
rw [tsub_le_iff_left, add_comm]

Result:
α : Type u_1
s t : Set α
⊢ s.encard ≤ (s \ t).encard + t.encard
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]?

Proof state:
α✝ : outParam (Type u_1)
a : α✝
l : List α✝
i : Nat
⊢ (a :: l)[i]? = if i = 0 then some a else l[i - 1]?

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Combinatorics/Young/SemistandardTableau.lean
theorem ext {μ : YoungDiagram} {T T' : SemistandardYoungTableau μ} (h : ∀ i j, T i j = T' i j) :
    T = T' :=
  DFunLike.ext T T' fun _ ↦ by
    funext
    apply h

Proof state:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), T i j = T' i j
x✝ : ℕ
⊢ T x✝ = T' x✝

Tactic:
funext

Result:
case h
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), T i j = T' i j
x✝¹ x✝ : ℕ
⊢ T x✝¹ x✝ = T' x✝¹ x✝

Proof state:
case h
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), T i j = T' i j
x✝¹ x✝ : ℕ
⊢ T x✝¹ x✝ = T' x✝¹ x✝

Tactic:
apply h

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem Antitone.ne_of_lt_of_lt_int {f : ℤ → α} (hf : Antitone f) (n : ℤ) {x : α}
    (h1 : f (n + 1) < x) (h2 : x < f n) (a : ℤ) : f a ≠ x

Proof state:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_le (Int.le_of_lt_add_one <| hf.reflect_lt h1)

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl

Result:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma isDynCoverOf_zero (T : X → X) (F : Set X) (U : Set (X × X)) {s : Set X} (h : s.Nonempty) :
    IsDynCoverOf T F U 0 s

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
s : Set X
h : s.Nonempty
⊢ F ⊆ ⋃ x ∈ s, univ

Tactic:
rcases h with ⟨x, x_s⟩

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
s : Set X
x : X
x_s : x ∈ s
⊢ F ⊆ ⋃ x ∈ s, univ

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
s : Set X
x : X
x_s : x ∈ s
⊢ F ⊆ ⋃ x ∈ s, univ

Tactic:
exact subset_iUnion₂_of_subset x x_s (subset_univ F)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
s : Set X
h : s.Nonempty
⊢ IsDynCoverOf T F U 0 s

Tactic:
simp only [IsDynCoverOf, ball, dynEntourage, not_lt_zero', Prod.map_iterate, iInter_of_empty,
  iInter_univ, preimage_univ]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
s : Set X
h : s.Nonempty
⊢ F ⊆ ⋃ x ∈ s, univ