harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem append_left_lt [LT α] {l₁ l₂ l₃ : Array α} (h : l₂ < l₃) :
    l₁ ++ l₂ < l₁ ++ l₃

Proof state:
case mk
α : Type u_1
inst✝ : LT α
l₂ l₃ : Array α
h : l₂ < l₃
toList✝ : List α
⊢ { toList := toList✝ } ++ l₂ < { toList := toList✝ } ++ l₃

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝ : LT α
l₃ : Array α
toList✝¹ toList✝ : List α
h : { toList := toList✝ } < l₃
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } < { toList := toList✝¹ } ++ l₃

Proof state:
case mk.mk.mk
α : Type u_1
inst✝ : LT α
toList✝² toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } < { toList := toList✝ }
⊢ { toList := toList✝² } ++ { toList := toList✝¹ } < { toList := toList✝² } ++ { toList := toList✝ }

Tactic:
simpa using List.append_left_lt h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
inst✝ : LT α
l₃ : Array α
toList✝¹ toList✝ : List α
h : { toList := toList✝ } < l₃
⊢ { toList := toList✝¹ } ++ { toList := toList✝ } < { toList := toList✝¹ } ++ l₃

Tactic:
cases l₃

Result:
case mk.mk.mk
α : Type u_1
inst✝ : LT α
toList✝² toList✝¹ toList✝ : List α
h : { toList := toList✝¹ } < { toList := toList✝ }
⊢ { toList := toList✝² } ++ { toList := toList✝¹ } < { toList := toList✝² } ++ { toList := toList✝ }

Proof state:
α : Type u_1
inst✝ : LT α
l₁ l₂ l₃ : Array α
h : l₂ < l₃
⊢ l₁ ++ l₂ < l₁ ++ l₃

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝ : LT α
l₂ l₃ : Array α
h : l₂ < l₃
toList✝ : List α
⊢ { toList := toList✝ } ++ l₂ < { toList := toList✝ } ++ l₃
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem preimage_mul_sphere (a b : E) (r : ℝ) : (b * ·) ⁻¹' sphere a r = sphere (a / b) r

Proof state:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r

Tactic:
simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x => b * x) ⁻¹' sphere a r = sphere (a / b) r

Tactic:
ext c

Result:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_quasispectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σₙ 𝕜 a) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σₙ 𝕜 a
ha : autoParam (p a) _auto✝
⊢ ‖x‖ ≤ ‖a‖

Tactic:
simpa only [cfcₙ_id 𝕜 a] using norm_apply_le_norm_cfcₙ (id : 𝕜 → 𝕜) a hx

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem eq_of_prime_pow_eq' (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂)
    (h : p₁ ^ k₁ = p₂ ^ k₂) : p₁ = p₂

Proof state:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Result:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
-- Mathlib/Topology/Covering.lean
theorem isCoveringMap_iff_isCoveringMapOn_univ : IsCoveringMap f ↔ IsCoveringMapOn f Set.univ

Proof state:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
⊢ IsCoveringMap f ↔ IsCoveringMapOn f Set.univ

Tactic:
simp only [IsCoveringMap, IsCoveringMapOn, Set.mem_univ, forall_true_left]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem toεNFA_correct (M : NFA α σ) : M.toεNFA.accepts = M.accepts

Proof state:
α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : NFA α σ
⊢ M.toεNFA.accepts = M.accepts

Tactic:
rw [εNFA.accepts, εNFA.eval, toεNFA_evalFrom_match]

Result:
α : Type u
σ : Type v
M : NFA α σ
⊢ {x | ∃ S ∈ M.toεNFA.accept, S ∈ M.evalFrom M.toεNFA.start x} = M.accepts
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem normalize_eq_of_nonzero (nonzero : μ ≠ 0) (s : Set Ω) : μ.normalize s = μ.mass⁻¹ * μ s

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
⊢ μ.normalize s = μ.mass⁻¹ * μ s

Tactic:
simp only [μ.self_eq_mass_mul_normalize, μ.mass_nonzero_iff.mpr nonzero, inv_mul_cancel_left₀,
  Ne, not_false_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toStream_toList {t : RBNode α} : t.toStream.toList = t.toList

Proof state:
α : Type u_1
t : RBNode α
⊢ t.toStream.toList = t.toList

Tactic:
simp [toStream_toList']

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean
lemma dualSubmodule_flip_dualSubmodule_of_basis {ι : Type*} [Finite ι]
    (hB : B.Nondegenerate) (b : Basis ι S M) :
    B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) =
      Submodule.span R (Set.range b)

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
classical
letI := FiniteDimensional.of_fintype_basis b
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
  dualBasis_flip_dualBasis B hB]

Result:
no goals

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
letI := FiniteDimensional.of_fintype_basis b

Result:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Proof state:
R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
⊢ B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
  dualBasis_flip_dualBasis B hB]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem measurable_of_measurable_coe (f : β → Measure α)
    (h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => f b s) : Measurable f :=
  Measurable.of_le_map <|
    iSup₂_le fun s hs =>
      MeasurableSpace.comap_le_iff_le_map.2 <| by rw [MeasurableSpace.map_comp]; exact h s hs

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ => μ s) ∘ f) mβ

Tactic:
exact h s hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ => μ s) (MeasurableSpace.map f mβ)

Tactic:
rw [MeasurableSpace.map_comp]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ => μ s) ∘ f) mβ
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.unit⁻¹ • A

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A.adjugate⁻¹ = h.unit⁻¹ • A

Tactic:
refine inv_eq_left_inv ?_

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ h.unit⁻¹ • A * A.adjugate = 1

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ h.unit⁻¹ • A * A.adjugate = 1

Tactic:
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_natCast_re (z : ℂ) (n : ℕ) : (z / n).re = z.re / n

Proof state:
z : ℂ
n : ℕ
⊢ (z / ↑n).re = z.re / ↑n

Tactic:
rw [div_natCast]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma eq_union_right (h : s ≤ t) : s ∪ t = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ s ∪ t = t

Tactic:
rw [union_comm, eq_union_left h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma continuousOn_evenKernel (a : UnitAddCircle) : ContinuousOn (evenKernel a) (Ioi 0)

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (evenKernel ↑a') (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))

Result:
case H
a' : ℝ
⊢ ContinuousOn (fun x => ↑(evenKernel (↑a') x)) (Ioi 0)

Proof state:
a : UnitAddCircle
⊢ ContinuousOn (evenKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
simp only [evenKernel_def]
refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
  (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

Result:
no goals

Proof state:
a' x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (I * ↑x).im

Tactic:
simpa

Result:
no goals

Proof state:
case H
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) x

Tactic:
exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
  (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

Result:
no goals

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (fun x => cexp (-↑π * ↑a' ^ 2 * ↑x) * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)

Result:
case H
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) x

Proof state:
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun u => (↑a' * I * ↑u, I * ↑u)) x

Tactic:
fun_prop

Result:
no goals

Proof state:
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => cexp (-↑π * ↑a' ^ 2 * ↑x)) x

Tactic:
fun_prop

Result:
no goals

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (fun x => ↑(evenKernel (↑a') x)) (Ioi 0)

Tactic:
simp only [evenKernel_def]

Result:
case H
a' : ℝ
⊢ ContinuousOn (fun x => cexp (-↑π * ↑a' ^ 2 * ↑x) * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) (Ioi 0)
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem exists_linearIndependent :
    ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K ((↑) : b → V)

Proof state:
case intro.intro.intro.intro
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
t b : Set V
hb₁ : b ⊆ t
hb₂ : t ⊆ ↑(span K b)
hb₃ : LinearIndepOn K id b
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val

Tactic:
exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
t : Set V
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val

Tactic:
obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
  exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)

Result:
case intro.intro.intro.intro
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
t b : Set V
hb₁ : b ⊆ t
hb₂ : t ⊆ ↑(span K b)
hb₃ : LinearIndepOn K id b
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem bypass_isPath {u v : V} (p : G.Walk u v) : p.bypass.IsPath

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
⊢ (cons h✝ p').bypass.IsPath

Tactic:
simp only [bypass]

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
⊢ (if hs : u✝ ∈ p'.bypass.support then p'.bypass.dropUntil u✝ hs else cons h✝ p'.bypass).IsPath

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ : V
⊢ nil.bypass.IsPath

Tactic:
simp!

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath

Tactic:
simp [*, cons_isPath_iff]

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath

Tactic:
exact ih.dropUntil hs

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
⊢ (if hs : u✝ ∈ p'.bypass.support then p'.bypass.dropUntil u✝ hs else cons h✝ p'.bypass).IsPath

Tactic:
split_ifs with hs

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∈ p'.bypass.support
⊢ (p'.bypass.dropUntil u✝ hs).IsPath

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.bypass.IsPath
hs : u✝ ∉ p'.bypass.support
⊢ (cons h✝ p'.bypass).IsPath
-- Mathlib/Data/PNat/Prime.lean
theorem coe_pnat_injective : Function.Injective ((↑) : Nat.Primes → ℕ+) := fun p q h =>
  Subtype.ext (by injection h)

Proof state:
p q : Primes
h : ↑p = ↑q
⊢ ↑p = ↑q

Tactic:
injection h

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_eq_zero_iff_of_nonpos (hs : s.Nonempty) (hf : ∀ i ∈ s, f i ≤ 0) :
    𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : OrderedAddCommMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hs : s.Nonempty
hf : ∀ i ∈ s, f i ≤ 0
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp [expect, sum_eq_zero_iff_of_nonpos hf, hs.ne_empty]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv_add_const (c : F) : deriv (fun y => f y + c) x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun y => f y + c) x = deriv f x

Tactic:
simp only [deriv, fderiv_add_const]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem conjTranspose_circulant [Star α] [AddGroup n] (v : n → α) :
    (circulant v)ᴴ = circulant (star fun i => v (-i))

Proof state:
α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᴴ = circulant (star fun i => v (-i))

Tactic:
ext

Result:
case a
α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᴴ i✝ j✝ = circulant (star fun i => v (-i)) i✝ j✝

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᴴ i✝ j✝ = circulant (star fun i => v (-i)) i✝ j✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Replicate.lean
theorem rel_replicate_left {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
    (replicate n a).Rel r m ↔ card m = n ∧ ∀ x, x ∈ m → r a x :=
  ⟨fun h =>
    ⟨(card_eq_card_of_rel h).symm.trans (card_replicate _ _), fun x hx => by
      obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx
      rwa [eq_of_mem_replicate hb1] at hb2⟩,
    fun h =>
    rel_of_forall (fun _ _ hx hy => (eq_of_mem_replicate hx).symm ▸ h.2 _ hy)
      (Eq.trans (card_replicate _ _) h.1.symm)⟩

Proof state:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x

Tactic:
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx

Result:
case intro.intro
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x

Proof state:
case intro.intro
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x

Tactic:
rwa [eq_of_mem_replicate hb1] at hb2

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero {s₁ s₂ : CompositionSeries X}
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) (hs₁0 : s₁.length = 0) : s₁ = s₂

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
⊢ s₁ = s₂

Tactic:
have : ∀ x, x ∈ s₂ ↔ x = s₂.last := fun x =>
  ⟨fun hx =>
    subsingleton_of_length_eq_zero
      (length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb ht
        hs₁0) hx s₂.last_mem,
    fun hx => hx.symm ▸ s₂.last_mem⟩

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
⊢ s₁ = s₂

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
⊢ s₁ = s₂

Tactic:
have : ∀ x, x ∈ s₁ ↔ x = s₁.last := fun x =>
  ⟨fun hx =>  subsingleton_of_length_eq_zero hs₁0 hx s₁.last_mem, fun hx => hx.symm ▸ s₁.last_mem⟩

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
⊢ s₁ = s₂

Proof state:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
x✝ : X
⊢ x✝ ∈ s₁ ↔ x✝ ∈ s₂

Tactic:
simp [*]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
⊢ s₁ = s₂

Tactic:
ext

Result:
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂
x✝ : X
⊢ x✝ ∈ s₁ ↔ x✝ ∈ s₂
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem norm_eq_zero {x : FreeGroup α} : norm x = 0 ↔ x = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x.norm = 0 ↔ x = 1

Tactic:
simp only [norm, List.length_eq_zero, toWord_eq_nil_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive posPart_eq_of_posPart_pos]
lemma oneLePart_of_one_lt_oneLePart (ha : 1 < a⁺ᵐ) : a⁺ᵐ = a

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ a⁺ᵐ = a

Tactic:
rw [oneLePart_def, right_lt_sup, not_le] at ha

Result:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
ha : 1 < a
⊢ a⁺ᵐ = a

Tactic:
exact oneLePart_eq_self.2 ha.le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem suffix_iff_eq_append : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
  ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e =>
    ⟨_, e⟩⟩

Proof state:
case intro
α✝ : Type u_1
l₁ r : List α✝
⊢ take ((r ++ l₁).length - l₁.length) (r ++ l₁) ++ l₁ = r ++ l₁

Tactic:
simp only [length_append, Nat.add_sub_cancel_right, take_left]

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <:+ l₂ → take (l₂.length - l₁.length) l₂ ++ l₁ = l₂

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
α✝ : Type u_1
l₁ r : List α✝
⊢ take ((r ++ l₁).length - l₁.length) (r ++ l₁) ++ l₁ = r ++ l₁
-- Mathlib/Data/Real/Pi/Wallis.lean
theorem le_W (k : ℕ) : ((2 : ℝ) * k + 1) / (2 * k + 2) * (π / 2) ≤ W k

Proof state:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k

Tactic:
rw [W_eq_integral_sin_pow_div_integral_sin_pow, le_div_iff₀ (integral_sin_pow_pos _)]

Result:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Proof state:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * (π / 2) ≤ W k

Tactic:
rw [← le_div_iff₀ pi_div_two_pos, div_eq_inv_mul (W k) _]

Result:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) ≤ (π / 2)⁻¹ * W k

Proof state:
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)

Tactic:
rw [integral_sin_pow (2 * k)]

Result:
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Proof state:
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1)

Tactic:
convert integral_sin_pow_succ_le (2 * k + 1)

Result:
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1 + 1)

Proof state:
case h.e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_add : (f + g).smeval x = f.smeval x + g.smeval x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
⊢ (Finsupp.sum (f + g) fun n r => r • ↑(x ^ n)) =
    (Finsupp.sum f fun n r => r • ↑(x ^ n)) + Finsupp.sum g fun n r => r • ↑(x ^ n)

Tactic:
rw [Finsupp.sum_add_index (fun n _ => zero_smul R (x ^ n).val) (fun n _ r r' => add_smul r r' _)]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
⊢ (f + g).smeval x = f.smeval x + g.smeval x

Tactic:
simp only [smeval_eq_sum]

Result:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
⊢ (Finsupp.sum (f + g) fun n r => r • ↑(x ^ n)) =
    (Finsupp.sum f fun n r => r • ↑(x ^ n)) + Finsupp.sum g fun n r => r • ↑(x ^ n)