harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Infix.lean
theorem mem_inits : ∀ s t : List α, s ∈ inits t ↔ s <+: t
  | s, [] =>
    suffices s = nil ↔ s <+: nil by simpa only [inits, mem_singleton]
    ⟨fun h => h.symm ▸ prefix_rfl, eq_nil_of_prefix_nil⟩
  | s, a :: t =>
    suffices (s = nil ∨ ∃ l ∈ inits t, a :: l = s) ↔ s <+: a :: t by simpa
    ⟨fun o =>
      match s, o with
      | _, Or.inl rfl => ⟨_, rfl⟩
      | s, Or.inr ⟨r, hr, hs⟩ => by
        let ⟨s, ht⟩ := (mem_inits _ _).1 hr
        rw [← hs, ← ht]; exact ⟨s, rfl⟩,
      fun mi =>
      match s, mi with
      | [], ⟨_, rfl⟩ => Or.inl rfl
      | b :: s, ⟨r, hr⟩ =>
        (List.noConfusion hr) fun ba (st : s ++ r = t) =>
          Or.inr <| by rw [ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩⟩

Proof state:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s

Tactic:
exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = b :: s

Tactic:
rw [ba]

Result:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b = a
st : s ++ r = t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s

Proof state:
α : Type u_1
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ [].inits ↔ s <+: []

Tactic:
simpa only [inits, mem_singleton]

Result:
no goals

Proof state:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t

Tactic:
rw [← hs, ← ht]

Result:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Proof state:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Tactic:
exact ⟨s, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
s✝ : List α
a : α
t : List α
o : s✝ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝
s r : List α
hr : r ∈ t.inits
hs : a :: r = s
⊢ s <+: a :: t

Tactic:
let ⟨s, ht⟩ := (mem_inits _ _).1 hr

Result:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ s✝ <+: a :: t

Proof state:
α : Type u_1
s : List α
a : α
t : List α
this : (s = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s) ↔ s <+: a :: t
⊢ s ∈ (a :: t).inits ↔ s <+: a :: t

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem filter_attachWith {q : α → Prop} {l : Array α} {p : {x // q x} → Bool} (H)
    (w : stop = (l.attachWith q H).size) :
    (l.attachWith q H).filter p 0 stop =
      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩)

Proof state:
α : Type u_1
q : α → Prop
l : Array α
p : { x // q x } → Bool
H : ∀ (x : α), x ∈ l → q x
⊢ filter p (l.attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        l.attach)

Tactic:
cases l

Result:
case mk
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ filter p ({ toList := toList✝ }.attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        { toList := toList✝ }.attach)

Proof state:
α : Type u_1
stop : Nat
q : α → Prop
l : Array α
p : { x // q x } → Bool
H : ∀ (x : α), x ∈ l → q x
w : stop = (l.attachWith q H).size
⊢ filter p (l.attachWith q H) 0 stop =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        l.attach)

Tactic:
subst w

Result:
α : Type u_1
q : α → Prop
l : Array α
p : { x // q x } → Bool
H : ∀ (x : α), x ∈ l → q x
⊢ filter p (l.attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        l.attach)

Proof state:
case mk
α : Type u_1
q : α → Prop
p : { x // q x } → Bool
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ filter p ({ toList := toList✝ }.attachWith q H) =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        { toList := toList✝ }.attach)

Tactic:
simp [Function.comp_def, List.filter_map]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_smul_right_of_ne_top' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ]
    {r : ℝ≥0∞} (hr : r ≠ 0) (hr_ne_top : r ≠ ∞) :
    ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ ¬(r = 0 ∨ r = ⊤)

Tactic:
simp [hr, hr_ne_top]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
  ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ r.toNNReal ≠ 0

Tactic:
rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ ¬(r = 0 ∨ r = ⊤)

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ

Tactic:
refine rnDeriv_smul_right' ν μ ?_

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ r.toNNReal ≠ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ

Tactic:
have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ := by
  refine rnDeriv_smul_right' ν μ ?_
  rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
  simp [hr, hr_ne_top]

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ⊤
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
-- Mathlib/Data/Nat/Bits.lean
lemma shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
  fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

Proof state:
x✝² x✝¹ x✝ : ℕ
hk : x✝ ≤ x✝¹
⊢ x✝² <<< (x✝¹ - x✝) = x✝² <<< x✝¹ >>> x✝

Tactic:
simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem separable_map {S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} :
    (p.map f).Separable ↔ p.Separable

Proof state:
case intro
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable

Tactic:
have := Separable.map H (f := Ideal.Quotient.mk m)

Result:
case intro
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable

Proof state:
case intro
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable

Tactic:
rwa [map_map, separable_def, derivative_map, isCoprime_map] at this

Result:
no goals

Proof state:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
⊢ p.Separable

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal S

Result:
case intro
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable

Proof state:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩

Result:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
⊢ p.Separable
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem sum_biUnion_boxes {M : Type*} [AddCommMonoid M] (π : Prepartition I)
    (πi : ∀ J, Prepartition J) (f : Box ι → M) :
    (∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J) =
      ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Proof state:
ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J => (πi J).boxes) J₁
h₂' : J' ∈ (fun J => (πi J).boxes) J₂
⊢ False

Tactic:
exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J ∈ π.boxes.biUnion fun J => (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Tactic:
refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_

Result:
ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
J₁ : Box ι
h₁ : J₁ ∈ ↑π.boxes
J₂ : Box ι
h₂ : J₂ ∈ ↑π.boxes
hne : J₁ ≠ J₂
J' : Box ι
h₁' : J' ∈ (fun J => (πi J).boxes) J₁
h₂' : J' ∈ (fun J => (πi J).boxes) J₂
⊢ False
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_comp (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
    mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Proof state:
case h
𝕜 : 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ HasMFDerivAt I I'' (g ∘ f) x ((mfderiv I' I'' g (f x)).comp (mfderiv I I' f x))

Tactic:
exact HasMFDerivAt.comp x hg.hasMFDerivAt hf.hasMFDerivAt

Result:
no goals

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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)

Tactic:
apply HasMFDerivAt.mfderiv

Result:
case h
𝕜 : 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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ HasMFDerivAt I I'' (g ∘ f) x ((mfderiv I' I'' g (f x)).comp (mfderiv I I' f x))
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma le_rieszMeasure_of_tsupport_subset {f : C_c(X, ℝ≥0)} (hf : ∀ x, f x ≤ 1) {V : Set X}
    (h : tsupport f ⊆ V) : .ofNNReal (Λ f) ≤ rieszMeasure Λ V

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)

Tactic:
apply le_rieszMeasure_of_isCompact_tsupport_subset Λ hf f.hasCompactSupport

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ tsupport ⇑f ⊆ tsupport ⇑f

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) V

Tactic:
apply le_trans _ (measure_mono h)

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ tsupport ⇑f ⊆ tsupport ⇑f

Tactic:
exact subset_rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem homothety_zero (c : P1) : homothety c (0 : k) = const k P1 c

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 0 = const k P1 c

Tactic:
ext p

Result:
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 0) p = (const k P1 c) p

Proof state:
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 0) p = (const k P1 c) p

Tactic:
simp [homothety_apply]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem eq_compl_iff_isCompl : x = yᶜ ↔ IsCompl x y :=
  ⟨fun h => by
    rw [h]
    exact isCompl_compl.symm, IsCompl.eq_compl⟩

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y

Tactic:
exact isCompl_compl.symm

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl x y

Tactic:
rw [h]

Result:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.pow
    (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hD : D.Injective)
    (hp : p.Monic D) : (p ^ n).Monic D

Proof state:
case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p ^ (n + 1))

Tactic:
rw [pow_succ']

Result:
case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Proof state:
case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Tactic:
exact hp.mul hD hadd ih

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D (p ^ n)

Tactic:
induction n with
| zero => rw [pow_zero]; exact monic_one hD
| succ n ih => rw [pow_succ']; exact hp.mul hD hadd ih

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D 1

Tactic:
exact monic_one hD

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D (p ^ 0)

Tactic:
rw [pow_zero]

Result:
case zero
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
⊢ Monic D 1
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive]
lemma pow_mul_comm' (a : M) (n : ℕ) : a ^ n * a = a * a ^ n

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ n * a = a * a ^ n

Tactic:
rw [← pow_succ, pow_succ']

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma cfcHom_eq_of_isStarNormal {A : Type*} [CStarAlgebra A] (a : A) [ha : IsStarNormal a] :
    cfcHom ha = (StarAlgebra.elemental ℂ a).subtype.comp (continuousFunctionalCalculus a)

Proof state:
case refine_1
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Continuous ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))

Tactic:
exact continuous_subtype_val.comp <|
  (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ cfcHom ha = (elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a)

Tactic:
refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_

Result:
case refine_1
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Continuous ⇑((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))

case refine_2
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ ((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a

Proof state:
case refine_2
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ ((elemental ℂ a).subtype.comp ↑(continuousFunctionalCalculus a))
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a

Tactic:
simp [continuousFunctionalCalculus_map_id a]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma iSup_ucs_le_genWeightSpace_zero :
    ⨆ k, (⊥ : LieSubmodule R L M).ucs k ≤ genWeightSpace M (0 : L → R)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
⊢ ⨆ k, LieSubmodule.ucs k ⊥ ≤ genWeightSpace M 0

Tactic:
simpa using
  LieSubmodule.ucs_le_of_normalizer_eq_self (genWeightSpace_zero_normalizer_eq_self R L M)

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_right_one' : preimage 1 (· * b⁻¹) (mul_left_injective _).injOn = {b}

Proof state:
α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x => x * b⁻¹) ⋯ = {b}

Tactic:
rw [preimage_mul_right_one, inv_inv]

Result:
no goals
-- Mathlib/Logic/Relation.lean
lemma reflTransGen_eq_transGen (hr : Reflexive r) :
    ReflTransGen r = TransGen r

Proof state:
α : Type u_1
r : α → α → Prop
hr : Reflexive r
⊢ ReflTransGen r = TransGen r

Tactic:
rw [← transGen_reflGen, reflGen_eq_self hr]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem liftAlgHom_fieldRange_eq_of_range_eq (hg : Function.Injective g)
    {s : Set L} (hs : g.range = Algebra.adjoin F s) :
    (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F s :=
  algHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
s : Set L
hs : g.range = Algebra.adjoin F s
x✝ : A
⊢ ((↑(liftAlgHom hg)).comp (algebraMap A K)) x✝ = ↑g x✝

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ (↑(liftAlgHom hg)).comp (algebraMap A K) = ↑g

Tactic:
ext

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
s : Set L
hs : g.range = Algebra.adjoin F s
x✝ : A
⊢ ((↑(liftAlgHom hg)).comp (algebraMap A K)) x✝ = ↑g x✝