harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[simp]
lemma toNNReal_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (r • f).toNNReal = r • f.toNNReal

Proof state:
case h.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Tactic:
by_cases h : 0 ≤ f x

Result:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : 0 ≤ f x
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : ¬0 ≤ f x
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (r • f).toNNReal = r • f.toNNReal

Tactic:
ext x

Result:
case h.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Proof state:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : ¬0 ≤ f x
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Tactic:
push_neg at h

Result:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : f x < 0
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Proof state:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : f x < 0
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Tactic:
simpa [max_eq_right h.le, NNReal.smul_def]
  using mul_nonpos_of_nonneg_of_nonpos r.coe_nonneg h.le

Result:
no goals

Proof state:
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : 0 ≤ f x
⊢ ↑((r • f).toNNReal x) = ↑((r • f.toNNReal) x)

Tactic:
simpa [max_eq_left h, NNReal.smul_def] using mul_nonneg r.coe_nonneg h

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma LeftHomologyData.exact_iff_epi_f' [S.HasHomology] (h : LeftHomologyData S) :
    S.Exact ↔ Epi h.f'

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ Epi h.f' → S.Exact

Tactic:
intro

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
a✝ : Epi h.f'
⊢ S.Exact

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact → Epi h.f'

Tactic:
intro hS

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
hS : S.Exact
⊢ Epi h.f'

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
a✝ : Epi h.f'
⊢ S.Exact

Tactic:
simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_epi h.π, ← cancel_epi h.f',
  comp_id, h.f'_π, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ Epi h.f'

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact → Epi h.f'

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ Epi h.f' → S.Exact

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
hS : S.Exact
⊢ Epi h.f'

Tactic:
exact hS.epi_f' h

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
lemma ShortExact.unop {S : ShortComplex Cᵒᵖ} (h : S.ShortExact) : S.unop.ShortExact where
  exact := h.exact.unop
  mono_f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
⊢ Mono S.unop.f

Tactic:
have := h.epi_g

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Epi S.g
⊢ Mono S.unop.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Mono S.f
⊢ Epi S.unop.g

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Mono S.f
⊢ Epi S.f.unop

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Epi S.g
⊢ Mono S.unop.f

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Epi S.g
⊢ Mono S.g.unop

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
⊢ Epi S.unop.g

Tactic:
have := h.mono_f

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Mono S.f
⊢ Epi S.unop.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Epi S.g
⊢ Mono S.g.unop

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
this : Mono S.f
⊢ Epi S.f.unop

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem avg_le_right (h : a ≤ b) : avg a b ≤ b

Proof state:
case a
a b : Nat
h : a ≤ b
⊢ a + b ≤ 2 * b

Tactic:
simp_arith [*]

Result:
no goals

Proof state:
a b : Nat
h : a ≤ b
⊢ a.avg b ≤ b

Tactic:
apply Nat.div_le_of_le_mul

Result:
case a
a b : Nat
h : a ≤ b
⊢ a + b ≤ 2 * b
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem alternatingGroup.index_eq_one [Subsingleton α] : (alternatingGroup α).index = 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ (alternatingGroup α).index = 1

Tactic:
rw [Subgroup.index_eq_one]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ alternatingGroup α = ⊤

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ alternatingGroup α = ⊤

Tactic:
apply Subsingleton.elim

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
@[simp] lemma _root_.LinearMap.surjective_domRestrict_iff
    {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Surjective f) :
    Surjective (f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : LinearMap.range f = ⊤
⊢ LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤

Tactic:
exact LinearMap.range_domRestrict_eq_range_iff

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : LinearMap.range f = ⊤
⊢ LinearMap.range (f.domRestrict S) = ⊤ ↔ S ⊔ LinearMap.ker f = ⊤

Tactic:
rw [← hf]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : LinearMap.range f = ⊤
⊢ LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : Surjective ⇑f
⊢ Surjective ⇑(f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤

Tactic:
rw [← LinearMap.range_eq_top] at hf ⊢

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : LinearMap.range f = ⊤
⊢ LinearMap.range (f.domRestrict S) = ⊤ ↔ S ⊔ LinearMap.ker f = ⊤
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_horiz_isIso [IsIso f] [IsIso inr] (sq : CommSq f g inl inr) : IsPushout f g inl inr :=
  of_isColimit' sq
    (by
      refine
        PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
          (by simp) (by simp)
      simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g), inr ≫ (fun s => inv inr ≫ s.inr) s = s.inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ s.inr) s = s.inl

Tactic:
simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit sq.cocone

Tactic:
refine
  PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
    (by simp) (by simp)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
s : PushoutCocone f g
⊢ inl ≫ (fun s => inv inr ≫ s.inr) s = s.inl

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst✝¹ : IsIso f
inst✝ : IsIso inr
sq : CommSq f g inl inr
⊢ ∀ (s : PushoutCocone f g) (m : P ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = (fun s => inv inr ≫ s.inr) s

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_one : bernoulli' 1 = 1 / 2

Proof state:
⊢ 1 - ∑ k ∈ range 1, ↑(Nat.choose 1 k) / (↑1 - ↑k + 1) * bernoulli' k = 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ bernoulli' 1 = 1 / 2

Tactic:
rw [bernoulli'_def]

Result:
⊢ 1 - ∑ k ∈ range 1, ↑(Nat.choose 1 k) / (↑1 - ↑k + 1) * bernoulli' k = 1 / 2
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
theorem simply_connected_iff_paths_homotopic' {Y : Type*} [TopologicalSpace Y] :
    SimplyConnectedSpace Y ↔
      PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), Path.Homotopic p₁ p₂

Proof state:
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)

Tactic:
simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]

Result:
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y

Proof state:
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
convert simply_connected_iff_paths_homotopic (Y := Y)

Result:
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)

Proof state:
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ ∀ (x y : Path a✝¹ a✝), (Path.Homotopic.setoid a✝¹ a✝) x y

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem independent_iSup_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    iSupIndep (fun μ ↦ ⨆ k : ℕ, f.genEigenspace μ k)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ iSupIndep fun μ => ⨆ k, (f.genEigenspace μ) ↑k

Tactic:
simp_rw [iSup_genEigenspace_eq]

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ iSupIndep fun μ => f.maxGenEigenspace μ

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ iSupIndep fun μ => f.maxGenEigenspace μ

Tactic:
apply independent_maxGenEigenspace

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
/-- The continuous functional calculus commutes with integration. -/
lemma cfc_integral [TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜)
    (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(spectrum 𝕜 a, 𝕜)]
    (hf₁ : ∀ x, ContinuousOn (f x) (spectrum 𝕜 a))
    (hf₂ : Continuous (fun x ↦ (⟨_, hf₁ x |>.restrict⟩ : C(spectrum 𝕜 a, 𝕜))))
    (hbound : ∀ x, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖)
    (hbound_finite_integral : HasFiniteIntegral bound μ) (ha : p a

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((spectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
hcont₂ : ContinuousOn (fun r => ∫ (x : X), f x r ∂μ) (spectrum 𝕜 a)
⊢ cfc (fun r => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
rw [integral_congr_ae (.of_forall fun _ ↦ cfc_apply ..), cfc_apply ..,
  cfcHom_integral _ _ fc_integrable]

Result:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : MeasurableSpace X
μ : Measure X
inst✝⁸ : NormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedAlgebra 𝕜 A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : CompleteSpace A
inst✝³ : ContinuousFunctionalCalculus 𝕜 p
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)
hf₁ : ∀ (x : X), ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Continuous fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
hbound : ∀ (x : X), ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ ‖bound x‖
hbound_finite_integral : HasFiniteIntegral bound μ
ha : autoParam (p a) _auto✝
fc : X → C(↑(spectrum 𝕜 a), 𝕜) := fun x => { toFun := (spectrum 𝕜 a).restrict (f x), continuous_toFun := ⋯ }
fc_integrable : Integrable fc μ
h_int_fc : ((spectrum 𝕜 a).restrict fun x => ∫ (x_1 : X), f x_1 x ∂μ) = ⇑(∫ (x : X), fc x ∂μ)
hcont₂ : ContinuousOn (fun r => ∫ (x : X), f x r ∂μ) (spectrum 𝕜 a)
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).restrict fun r => ∫ (x : X), f x r ∂μ, continuous_toFun := ⋯ } =
    (cfcHom ha) (∫ (x : X), fc x ∂μ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
    (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₂ : List α
⊢ ([] ++ l₂).replace a b = if a ∈ [] then [].replace a b ++ l₂ else [] ++ l₂.replace a b

Tactic:
simp

Result:
no goals

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

Tactic:
induction l₁ with
| nil => simp
| cons x xs ih =>
  simp only [cons_append, replace_cons]
  split <;> split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₂ : List α
x : α
xs : List α
ih : (xs ++ l₂).replace a b = if a ∈ xs then xs.replace a b ++ l₂ else xs ++ l₂.replace a b
⊢ (match a == x with
    | true => b :: (xs ++ l₂)
    | false => x :: (xs ++ l₂).replace a b) =
    if a ∈ x :: xs then
      (match a == x with
        | true => b :: xs
        | false => x :: xs.replace a b) ++
        l₂
    else x :: (xs ++ l₂.replace a b)

Tactic:
split <;> split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₂ : List α
x : α
xs : List α
ih : (xs ++ l₂).replace a b = if a ∈ xs then xs.replace a b ++ l₂ else xs ++ l₂.replace a b
⊢ (x :: xs ++ l₂).replace a b = if a ∈ x :: xs then (x :: xs).replace a b ++ l₂ else x :: xs ++ l₂.replace a b

Tactic:
simp only [cons_append, replace_cons]

Result:
case cons
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l₂ : List α
x : α
xs : List α
ih : (xs ++ l₂).replace a b = if a ∈ xs then xs.replace a b ++ l₂ else xs ++ l₂.replace a b
⊢ (match a == x with
    | true => b :: (xs ++ l₂)
    | false => x :: (xs ++ l₂).replace a b) =
    if a ∈ x :: xs then
      (match a == x with
        | true => b :: xs
        | false => x :: xs.replace a b) ++
        l₂
    else x :: (xs ++ l₂.replace a b)
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.factor_eq_gcd_right {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m) (bn : b ∣ n) :
    a = (b * a).gcd m

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m

Tactic:
apply Coprime.factor_eq_gcd_left cop am bn

Result:
no goals

Proof state:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
rw [mul_comm]

Result:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem get_dite' {p : Prop} [Decidable p] (b : ¬ p → β) (w) :
    (if h : p then none else some (b h)).get w = b (by simpa using w)

Proof state:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : p
⊢ False

Tactic:
simp at w

Result:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
h✝ : p
w : ¬p
⊢ False

Proof state:
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
⊢ (if h : p then none else some (b h)).get w = b ⋯

Tactic:
split

Result:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : p
⊢ none.get ⋯ = b ⋯

case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : ¬p
⊢ (some (b h✝)).get ⋯ = b ⋯

Proof state:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
h✝ : p
w : ¬p
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : p
⊢ none.get ⋯ = b ⋯

Tactic:
exfalso

Result:
case isTrue
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : p
⊢ False

Proof state:
β : Type ?u.51024
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
⊢ ¬p

Tactic:
simpa using w

Result:
no goals

Proof state:
case isFalse
β : Type u_1
p : Prop
inst✝ : Decidable p
b : ¬p → β
w : (if h : p then none else some (b h)).isSome = true
h✝ : ¬p
⊢ (some (b h✝)).get ⋯ = b ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_zmod_self (n : ℕ) :
    W_ (ZMod (p ^ (n + 1))) (n + 1) = expand p (W_ (ZMod (p ^ (n + 1))) n)

Proof state:
case e_a.e_a.e_a
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1

Tactic:
rw [mem_range] at hk

Result:
case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1

Proof state:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)

Tactic:
congr

Result:
case e_a.e_a.e_a
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ n + 1 - k = n - k + 1

Proof state:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k) * X k ^ p ^ (n - k))

Tactic:
rw [map_mul (expand p), map_pow (expand p), expand_X, algHom_C, ← pow_mul, ← pow_succ']

Result:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) =
    (algebraMap (ZMod (p ^ (n + 1))) (MvPolynomial ℕ (ZMod (p ^ (n + 1))))) (↑p ^ k) * X k ^ p ^ (n - k + 1)

Proof state:
p n : ℕ
⊢ ∑ i ∈ range (n + 1 + 1), C (↑p ^ i) * X i ^ p ^ (n + 1 - i) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))

Tactic:
rw [sum_range_succ, ← Nat.cast_pow, CharP.cast_eq_zero (ZMod (p ^ (n + 1))) (p ^ (n + 1)), C_0,
  zero_mul, add_zero, map_sum, sum_congr rfl]

Result:
p n : ℕ
⊢ ∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))

Proof state:
case e_a.e_a.e_a
p n k : ℕ
hk : k < n + 1
⊢ n + 1 - k = n - k + 1

Tactic:
rw [add_comm, add_tsub_assoc_of_le (Nat.lt_succ_iff.mp hk), ← add_comm]

Result:
no goals

Proof state:
p n : ℕ
⊢ ∀ x ∈ range (n + 1), C (↑p ^ x) * X x ^ p ^ (n + 1 - x) = (expand p) (C (↑p ^ x) * X x ^ p ^ (n - x))

Tactic:
intro k hk

Result:
p n k : ℕ
hk : k ∈ range (n + 1)
⊢ C (↑p ^ k) * X k ^ p ^ (n + 1 - k) = (expand p) (C (↑p ^ k) * X k ^ p ^ (n - k))

Proof state:
p n : ℕ
⊢ W_ (ZMod (p ^ (n + 1))) (n + 1) = (expand p) (W_ (ZMod (p ^ (n + 1))) n)

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow]

Result:
p n : ℕ
⊢ ∑ i ∈ range (n + 1 + 1), C (↑p ^ i) * X i ^ p ^ (n + 1 - i) =
    (expand p) (∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i))