harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isLeftDescent_inv_iff {w : W} {i : B} :
    cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i

Tactic:
unfold IsLeftDescent IsRightDescent

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w

Tactic:
nth_rw 1 [← length_inv]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma CochainComplex.quasiIsoAt₀_iff {K L : CochainComplex C ℕ} (f : K ⟶ L)
    [K.HasHomology 0] [L.HasHomology 0] [(K.sc' 0 0 1).HasHomology] [(L.sc' 0 0 1).HasHomology] :
    QuasiIsoAt f 0 ↔
      ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C _ 0 0 1).map f) :=
  quasiIsoAt_iff' _ _ _ _ (by simp) (by simp)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 0 0 1).HasHomology
inst✝ : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 0 0 1).HasHomology
inst✝ : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem compMultilinearMap_alternatization (g : N' →ₗ[R] N'₂)
    (f : MultilinearMap R (fun _ : ι => M) N') :
    MultilinearMap.alternatization (g.compMultilinearMap f)
      = g.compAlternatingMap (MultilinearMap.alternatization f)

Proof state:
R : Type u_1
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
⊢ MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)

Tactic:
ext

Result:
case H
R : Type u_1
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
x✝ : ι → M
⊢ (MultilinearMap.alternatization (g.compMultilinearMap f)) x✝ =
    (g.compAlternatingMap (MultilinearMap.alternatization f)) x✝

Proof state:
case H
R : Type u_1
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x => M) N'
x✝ : ι → M
⊢ (MultilinearMap.alternatization (g.compMultilinearMap f)) x✝ =
    (g.compAlternatingMap (MultilinearMap.alternatization f)) x✝

Tactic:
simp [MultilinearMap.alternatization_def]

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
theorem X_pow_sub_C_eq_prod'
    {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (hn : 0 < n) (e : α ^ n = a) :
    (X ^ n - C a) = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ (Multiset.map ((fun a => X - C a) ∘ fun x => ζ ^ x * α) (Multiset.range n)).prod =
    ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
rw [eq_prod_roots_of_monic_of_splits_id (monic_X_pow_sub_C _ (Nat.pos_iff_ne_zero.mp hn))
  (X_pow_sub_C_splits_of_isPrimitiveRoot hζ e), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]

Result:
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ (Multiset.map ((fun a => X - C a) ∘ fun x => ζ ^ x * α) (Multiset.range n)).prod =
    ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
-- Mathlib/Algebra/Divisibility/Units.lean
theorem dvd_mul_right : a ∣ b * u ↔ a ∣ b :=
  Iff.intro (fun ⟨c, eq⟩ ↦ ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]⟩)
    fun ⟨_, eq⟩ ↦ eq.symm ▸ (_root_.dvd_mul_right _ _).mul_right _

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = a * (c * ↑u⁻¹)

Tactic:
rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_def (G : C) :
    IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g :=
  ⟨fun hG X Y f g hfg =>
    hG _ _ fun H hH h => by
      obtain rfl := Set.mem_singleton_iff.1 hH
      exact hfg h,
    fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (Set.mem_singleton _) _⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : H ∈ {G}
h : H ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
obtain rfl := Set.mem_singleton_iff.1 hH

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
H : C
h : H ⟶ X
hG : IsSeparator H
hfg : ∀ (h : H ⟶ X), h ≫ f = h ≫ g
hH : H ∈ {H}
⊢ h ≫ f = h ≫ g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
H : C
h : H ⟶ X
hG : IsSeparator H
hfg : ∀ (h : H ⟶ X), h ≫ f = h ≫ g
hH : H ∈ {H}
⊢ h ≫ f = h ≫ g

Tactic:
exact hfg h

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) : succAbove i.succ 0 = 0 :=
  succAbove_of_castSucc_lt i.succ 0 (by simp only [castSucc_zero', succ_pos])

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ castSucc 0 < i.succ

Tactic:
simp only [castSucc_zero', succ_pos]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_empty (I : Set α) : uniqueBaseOn ∅ I = loopyOn I

Proof state:
α : Type u_1
I : Set α
⊢ uniqueBaseOn ∅ I = loopyOn I

Tactic:
rw [← dual_inj, uniqueBaseOn_dual_eq, diff_empty, uniqueBaseOn_self, loopyOn_dual_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem under_left (U : Under X) : U.left = ⟨⟨⟩⟩

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U : Under X
⊢ U.left = { as := PUnit.unit }

Tactic:
simp only

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_mem_zipIdx_iff_getElem? {i : Nat} {x : α} {l : List α} : (x, i) ∈ zipIdx l ↔ l[i]? = x

Proof state:
α : Type u_1
i : Nat
x : α
l : List α
⊢ (x, i) ∈ l.zipIdx ↔ l[i]? = some x

Tactic:
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem finite_of_toPiLocalization_surjective
    (surj : Function.Surjective (toPiLocalization R)) :
    Finite (PrimeSpectrum R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)

Tactic:
exact finite_of_toPiLocalization_pi_surjective surj.of_comp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (PrimeSpectrum R)

Tactic:
replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj

Result:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)

Tactic:
rw [← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj

Result:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (PrimeSpectrum R)
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_compl (a : α) : a ⇨ aᶜ = aᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ aᶜ = aᶜ

Tactic:
rw [← himp_bot, himp_himp, inf_idem]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCardAux_eq_map_coe {n} {l : List α} :
    powersetCardAux n l = (sublistsLen n l).map (↑)

Proof state:
α : Type u_1
n : ℕ
l : List α
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)

Tactic:
rw [powersetCardAux, sublistsLenAux_eq, append_nil]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
    (xs.any fun x => x == a) = xs.contains a

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
xs : Array α
⊢ (xs.any fun x => x == a) = xs.contains a

Tactic:
simp only [BEq.comm, any_beq]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mk_add [∀ i, AddZeroClass (β i)] {s : Finset ι} {x y : ∀ i : (↑s : Set ι), β i} :
    mk s (x + y) = mk s x + mk s y :=
  ext fun i => by simp only [add_apply, mk_apply]; split_ifs <;> [rfl; rw [zero_add]]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x + y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) + if H : i ∈ s then y ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [zero_add]]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (x + y)) i = (mk s x + mk s y) i

Tactic:
simp only [add_apply, mk_apply]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x + y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) + if H : i ∈ s then y ⟨i, H⟩ else 0
-- Mathlib/Algebra/GroupWithZero/WithZero.lean
@[simp]
lemma map'_id : map' (MonoidHom.id β) = MonoidHom.id (WithZero β)

Proof state:
case h
β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x

Tactic:
induction x <;> rfl

Result:
no goals

Proof state:
β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

Tactic:
ext x

Result:
case h
β : Type u_2
inst✝ : MulOneClass β
x : WithZero β
⊢ ↑(map' (MonoidHom.id β)) x = (MonoidHom.id (WithZero β)) x
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_atTop_iff_eventually_exists_pos {α : Type*}
    [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} :
    f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Proof state:
G : Type u_5
G' : Type u_8
inst✝³ : Norm G
inst✝² : SeminormedAddCommGroup G'
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → G
g : α → G'
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_eq_zero (h : ∀ n : ℕ, ∃ k, map f p ≤ P ^ k ∧ n < k) :
    ramificationIdx f p P = 0 :=
  dif_neg (by push_neg; exact h)

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ a ∈ {n | map f p ≤ P ^ n}, n < a

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ¬∃ n, ∀ a ∈ {n | map f p ≤ P ^ n}, a ≤ n

Tactic:
push_neg

Result:
R : Type u
inst✝¹ : CommRing R
S : Type v
inst✝ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ∀ (n : ℕ), ∃ a ∈ {n | map f p ≤ P ^ n}, n < a
-- Mathlib/Data/Seq/WSeq.lean
theorem bind_congr {s1 s2 : WSeq α} {f1 f2 : α → WSeq β} (h1 : s1 ~ʷ s2) (h2 : ∀ a, f1 a ~ʷ f2 a) :
    bind s1 f1 ~ʷ bind s2 f2 :=
  liftRel_bind _ _ h1 fun {a b} h => by rw [h]; apply h2

Proof state:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel (fun x1 x2 => x1 = x2) (f1 b) (f2 b)

Tactic:
apply h2

Result:
no goals

Proof state:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel (fun x1 x2 => x1 = x2) (f1 a) (f2 b)

Tactic:
rw [h]

Result:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel (fun x1 x2 => x1 = x2) (f1 b) (f2 b)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem eq_bot_or_nonempty (Q : AffineSubspace k P) : Q = ⊥ ∨ (Q : Set P).Nonempty

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥

Tactic:
apply eq_or_ne

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ (↑Q).Nonempty

Tactic:
rw [nonempty_iff_ne_bot]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- A translation of the relation `Λ * ↑ζ = log` of (real-valued) arithmetic functions
to an equality of complex sequences. -/
lemma convolution_vonMangoldt_zeta : ↗Λ ⍟ ↗ζ = ↗Complex.log

Proof state:
⊢ ((fun n => ↑(Λ n)) ⍟ fun n => ↑(ζ n)) = fun n => Complex.log ↑n

Tactic:
ext n

Result:
case h
n : ℕ
⊢ ((fun n => ↑(Λ n)) ⍟ fun n => ↑(ζ n)) n = Complex.log ↑n
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_zsmul_sub_self (a b : α) : toIocDiv hp a b • p - b = -toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b

Tactic:
rw [toIocMod, neg_sub]

Result:
no goals
-- Mathlib/Probability/Variance.lean
lemma variance_of_integral_eq_zero (hX : AEMeasurable X μ) (hXint : μ[X] = 0) :
    variance X μ = ∫ ω, X ω ^ 2 ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ Var[X; μ] = ∫ (ω : Ω), X ω ^ 2 ∂μ

Tactic:
simp [variance_eq_integral hX, hXint]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
lemma Ioo_smul_sphere_zero {a b r : ℝ} (ha : 0 ≤ a) (hr : 0 < r) :
    Ioo a b • sphere (0 : E) r = ball 0 (b * r) \ closedBall 0 (a * r)

Proof state:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x => ‖x‖) id (Ioo a b)
x : E
⊢ x ∈ (fun x => ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x => ‖x‖) id (Ioo a b)
⊢ 0 ∉ Ioo a b

Tactic:
simp [ha.not_lt]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x => ‖x‖) id (Ioo a b)
⊢ (fun x => ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
ext x

Result:
case h
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x => ‖x‖) id (Ioo a b)
x : E
⊢ x ∈ (fun x => ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)
-- Mathlib/Data/Finset/Card.lean
theorem card_le_one_iff : #s ≤ 1 ↔ ∀ {a b}, a ∈ s → b ∈ s → a = b

Proof state:
α : Type u_1
s : Finset α
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rw [card_le_one]

Result:
α : Type u_1
s : Finset α
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_symm : (canonicalEquiv S P P').symm = canonicalEquiv S P' P :=
  RingEquiv.ext fun I =>
    SetLike.ext_iff.mpr fun x => by
      rw [mem_canonicalEquiv_apply, canonicalEquiv, mapEquiv_symm, mapEquiv_apply,
        mem_map]
      exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ x ∈ (canonicalEquiv S P P').symm I ↔ x ∈ (canonicalEquiv S P' P) I

Tactic:
rw [mem_canonicalEquiv_apply, canonicalEquiv, mapEquiv_symm, mapEquiv_apply,
  mem_map]

Result:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
              { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
x : P
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
              { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }).symm
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P (RingHom.id R) ⋯) y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem apply_mem_span_image_iff_mem_span [RingHomSurjective σ₁₂] {f : F} {x : M}
    {s : Set M} (hf : Function.Injective f) :
    f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₂ M₂
F : Type u_8
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
x : M
s : Set M
hf : Injective ⇑f
⊢ f x ∈ span R₂ (⇑f '' s) ↔ x ∈ span R s

Tactic:
rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α}
    (h₁ : (l.map Prod.fst).contains k = false)
    {h'} :
    get (insertMany m l).1 k h' = get m k (contains_of_contains_insertMany_list _ h h' h₁)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
h₁ : (List.map Prod.fst l).contains k = false
h' : (insertMany m l).val.contains k = true
⊢ get (insertMany m l).val k h' = get m k ⋯

Tactic:
simp_to_model [Const.insertMany] using List.getValue_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylor_within_apply (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ) :
    taylorWithinEval f n s x₀ x =
      ∑ k ∈ Finset.range (n + 1), ((k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Proof state:
case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f 0 s x₀ x = ∑ k ∈ Finset.range (0 + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Tactic:
simp

Result:
no goals

Proof state:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀

Tactic:
simp [Nat.factorial]

Result:
no goals

Proof state:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ taylorWithinEval f (k + 1) s x₀ x =
    ∑ k ∈ Finset.range (k + 1 + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Tactic:
rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]

Result:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f n s x₀ x = ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀

Tactic:
induction n with
| zero => simp
| succ k hk =>
  rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
  simp [Nat.factorial]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem K'.elim_update_aux {a b c d c'} : update (K'.elim a b c d) aux c' = K'.elim a b c' d

Proof state:
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' = elim a b c' d

Tactic:
funext x

Result:
case h
a b c d c' : List Γ'
x : K'
⊢ update (elim a b c d) aux c' x = elim a b c' d x

Proof state:
case h
a b c d c' : List Γ'
x : K'
⊢ update (elim a b c d) aux c' x = elim a b c' d x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_succ_self_right : ∀ n : ℕ, (n + 1).choose n = n + 1
  | 0 => rfl
  | n + 1 => by rw [choose_succ_succ, choose_succ_self_right n, choose_self]

Proof state:
n : ℕ
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1

Tactic:
rw [choose_succ_succ, choose_succ_self_right n, choose_self]

Result:
no goals