harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
    (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this : ∀ (cs : Array β), foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as
⊢ foldl (fun bs a => bs ++ f a) (f a) as = f a ++ foldl (fun bs a => bs ++ f a) #[] as

Tactic:
simpa using this #[]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
cs : Array β
⊢ foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as

Tactic:
induction as generalizing cs <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ foldl (fun bs a => bs ++ f a) #[] as

Tactic:
suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
    f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
  erw [empty_append] simpa using this #[]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ ∀ (cs : Array β), foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ Array.flatMap f (a :: as).toArray = f a ++ Array.flatMap f as.toArray

Tactic:
simp [Array.flatMap]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ foldl (fun bs a => bs ++ f a) #[] as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ ∀ (cs : Array β), foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as

Tactic:
intro cs

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
cs : Array β
⊢ foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this : ∀ (cs : Array β), foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as
⊢ foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ foldl (fun bs a => bs ++ f a) #[] as

Tactic:
erw [empty_append]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this : ∀ (cs : Array β), foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ foldl (fun bs a => bs ++ f a) cs as
⊢ foldl (fun bs a => bs ++ f a) (f a) as = f a ++ foldl (fun bs a => bs ++ f a) #[] as
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma integrable_llr_tilted_right [IsFiniteMeasure μ] [SigmaFinite ν]
    (hμν : μ ≪ ν) (hfμ : Integrable f μ)
    (h_int : Integrable (llr μ ν) μ) (hfν : Integrable (fun x ↦ exp (f x)) ν) :
    Integrable (llr μ (ν.tilted f)) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfν : Integrable (fun x => rexp (f x)) ν
⊢ Integrable (fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ

Tactic:
exact Integrable.add (hfμ.neg.add (integrable_const _)) h_int

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfν : Integrable (fun x => rexp (f x)) ν
⊢ Integrable (llr μ (ν.tilted f)) μ

Tactic:
rw [integrable_congr (llr_tilted_right hμν hfν)]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hfμ : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfν : Integrable (fun x => rexp (f x)) ν
⊢ Integrable (fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x) μ
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
lemma diracProbaInverse_eq [T0Space X] {x : X} {μ : range (diracProba (X := X))}
    (h : μ = diracProba x) :
    diracProbaInverse μ = x

Proof state:
case a
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ (fun x => diracProba x) (diracProbaInverse μ) = (fun x => diracProba x) x

Tactic:
simp only [← h]

Result:
case a
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ diracProba (diracProbaInverse μ) = ↑μ

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ diracProbaInverse μ = x

Tactic:
apply injective_diracProba_of_T0 (X := X)

Result:
case a
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ (fun x => diracProba x) (diracProbaInverse μ) = (fun x => diracProba x) x

Proof state:
case a
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ diracProba (diracProbaInverse μ) = ↑μ

Tactic:
exact (mem_range.mp μ.prop).choose_spec

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem range_eq_top_of_cancel {f : A →* B}
    (h : ∀ u v : B →* B ⧸ f.range, u.comp f = v.comp f → u = v) : f.range = ⊤

Proof state:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ 1 = ↑(f x)

Tactic:
rw [show (1 : B ⧸ f.range) = (1 : B) from QuotientGroup.mk_one _, QuotientGroup.eq, inv_one,
  one_mul]

Result:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ f x ∈ f.range

Proof state:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' f.range
⊢ (QuotientGroup.mk' f.range).ker = ker 1

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ (comp 1 f) x = ((QuotientGroup.mk' f.range).comp f) x

Tactic:
simp only [one_apply, coe_comp, coe_mk', Function.comp_apply]

Result:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ 1 = ↑(f x)

Proof state:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : (QuotientGroup.mk' f.range).ker = ker 1
⊢ f.range = ⊤

Tactic:
rwa [ker_one, QuotientGroup.ker_mk'] at h

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
⊢ comp 1 f = (QuotientGroup.mk' f.range).comp f

Tactic:
ext1 x

Result:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ (comp 1 f) x = ((QuotientGroup.mk' f.range).comp f) x

Proof state:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
⊢ f.range = ⊤

Tactic:
specialize h 1 (QuotientGroup.mk' _) _

Result:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
⊢ comp 1 f = (QuotientGroup.mk' f.range).comp f

A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' f.range
⊢ f.range = ⊤

Proof state:
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ f x ∈ f.range

Tactic:
exact ⟨x, rfl⟩

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' f.range
⊢ f.range = ⊤

Tactic:
replace h : (QuotientGroup.mk' f.range).ker = (1 : B →* B ⧸ f.range).ker := by rw [h]

Result:
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : (QuotientGroup.mk' f.range).ker = ker 1
⊢ f.range = ⊤
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- Every point is either an interior or a boundary point. -/
lemma isInteriorPoint_or_isBoundaryPoint (x : M) : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

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
x : M
⊢ ↑(extChartAt I x) x ∉ interior (range ↑I) → ↑(extChartAt I x) x ∈ range ↑I ∧ ↑(extChartAt I x) x ∉ interior (range ↑I)

Tactic:
exact fun h ↦ ⟨mem_range_self _, h⟩

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
x : M
⊢ I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

Tactic:
rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior,
  I.isClosed_range.closure_eq, mem_diff]

Result:
𝕜 : 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
x : M
⊢ ↑(extChartAt I x) x ∉ interior (range ↑I) → ↑(extChartAt I x) x ∈ range ↑I ∧ ↑(extChartAt I x) x ∉ interior (range ↑I)
-- Mathlib/Order/Partition/Equipartition.lean
theorem isEquipartition_iff_card_parts_eq_average :
    P.IsEquipartition ↔
      ∀ a : Finset α, a ∈ P.parts → #a = #s / #P.parts ∨ #a = #s / #P.parts + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ P.IsEquipartition ↔ ∀ a ∈ P.parts, #a = #s / #P.parts ∨ #a = #s / #P.parts + 1

Tactic:
simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem hasSum_sum_range_mul_of_summable_norm' {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (h'f : Summable f)
    (hg : Summable fun x => ‖g x‖) (h'g : Summable g) :
    HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' n, f n) * ∑' n, g n)

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ HasSum (fun n => ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
convert (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum

Result:
case h.e'_6
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Proof state:
case h.e'_6
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
h'f : Summable f
hg : Summable fun x => ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem tensor_id (M N : ModuleCat R) : tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (M ⊗ N))

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ Hom.hom (tensorHom (𝟙 M) (𝟙 N)) = Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N)))

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ (mk R ↑M ↑N).compr₂ (Hom.hom (tensorHom (𝟙 M) (𝟙 N))) = (mk R ↑M ↑N).compr₂ (Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N))))

Tactic:
rfl

Result:
no goals

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ Hom.hom (tensorHom (𝟙 M) (𝟙 N)) = Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N)))

Tactic:
apply TensorProduct.ext

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ (mk R ↑M ↑N).compr₂ (Hom.hom (tensorHom (𝟙 M) (𝟙 N))) = (mk R ↑M ↑N).compr₂ (Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N))))
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem Scheme.isoSpec_hom_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    X.isoSpec.hom ≫ Spec.map (f.appTop) = f ≫ Y.isoSpec.hom

Proof state:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ X.isoSpec.hom ≫ Spec.map (Hom.appTop f) = f ≫ Y.isoSpec.hom

Tactic:
simp only [isoSpec, asIso_hom, Scheme.toSpecΓ_naturality]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_nat_iff_continuous_differentiable {n : ℕ} :
    ContDiff 𝕜 n f ↔
      (∀ m : ℕ, m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
        ∀ m : ℕ, m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x) ↔
    (∀ m ≤ n, Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧ ∀ m < n, Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ ContDiff 𝕜 (↑n) f ↔
    (∀ m ≤ n, Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧ ∀ m < n, Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x

Tactic:
rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
⊢ ((∀ (m : ℕ), ↑m ≤ ↑n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < ↑n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x) ↔
    (∀ m ≤ n, Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧ ∀ m < n, Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_lt_of_emultiplicity_lt {n : ℕ} (h : emultiplicity a b < n) :
    multiplicity a b < n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b < ↑n
⊢ multiplicity a b < n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem div_self_mul_self' (a : G₀) : a / (a * a) = a⁻¹ :=
  calc
    a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹

Tactic:
simp [mul_inv_rev]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem of_eq {f g : α → β → σ} (hg : Primrec₂ f) (H : ∀ a b, f a b = g a b) : Primrec₂ g :=
  (by funext a b; apply H : f = g) ▸ hg

Proof state:
case h.h
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b

Tactic:
apply H

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
⊢ f = g

Tactic:
funext a b

Result:
case h.h
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α → β → σ
hg : Primrec₂ f
H : ∀ (a : α) (b : β), f a b = g a b
a : α
b : β
⊢ f a b = g a b
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_eq_of_tendsto [NormOneClass E] {r : NNReal} (hr : r ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 r)) :
      (ofScalars E c).radius = ofNNReal r

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)

Tactic:
convert hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ (fun n => ‖c n.succ‖ / ‖c n‖) = fun x => (‖c x‖ / ‖c x.succ‖)⁻¹

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ (fun n => ‖c n.succ‖ / ‖c n‖) = fun x => (‖c x‖ / ‖c x.succ‖)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ r = r⁻¹⁻¹

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ (ofScalars E c).radius = ↑r

Tactic:
suffices Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r⁻¹) by
  convert ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
  simp

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ (ofScalars E c).radius = ↑r

Tactic:
convert ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this

Result:
case h.e'_3.h.e'_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) atTop (𝓝 ↑r)
this : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r)⁻¹)
⊢ r = r⁻¹⁻¹
-- Mathlib/Data/Real/EReal.lean
lemma div_self {a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1

Proof state:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : a ≠ 0
⊢ a / a = 1

Tactic:
rw [← coe_toReal h₂ h₁] at h₃ ⊢

Result:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1

Proof state:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1

Tactic:
rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measure_lt_top_of_nhdsWithin (h : IsCompact s) (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝[s] x)) :
    μ s < ∞ :=
  IsCompact.induction_on h (by simp) (fun _ _ hst ht => (measure_mono hst).trans_lt ht)
    (fun s t hs ht => (measure_union_le s t).trans_lt (ENNReal.add_lt_top.2 ⟨hs, ht⟩)) hμ

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝[s] x)
⊢ μ ∅ < ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem zipIdx_toVector {l : Array α} {k : Nat} :
    l.toVector.zipIdx k = (l.zipIdx k).toVector.cast (by simp)

Proof state:
α : Type u_1
l : Array α
k : Nat
⊢ l.toVector.zipIdx k = Vector.cast ⋯ (l.zipIdx k).toVector

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type ?u.10593
l : Array α
k : Nat
⊢ (l.zipIdx k).size = l.size

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_mul_C_le (p : MvPolynomial σ R) (i : σ) (c : R) :
    (p * C c).degreeOf i ≤ p.degreeOf i

Proof state:
case h.e'_4.h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = p.degrees + (C c).degrees

Tactic:
simp only [degrees_C, add_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (p * C c) ≤ degreeOf i p

Tactic:
unfold degreeOf

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i (p * C c).degrees ≤ Multiset.count i p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i (p * C c).degrees ≤ Multiset.count i p.degrees

Tactic:
convert Multiset.count_le_of_le i degrees_mul_le

Result:
case h.e'_4.h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = p.degrees + (C c).degrees
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem finRotate_bit1_mem_alternatingGroup {n : ℕ} :
    finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))

Proof state:
n : ℕ
⊢ finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))

Tactic:
rw [mem_alternatingGroup, sign_finRotate, pow_mul, pow_two, Int.units_mul_self, one_pow]

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem extendSubtype_apply_of_not_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) :
    e.extendSubtype x = e.toCompl ⟨x, hx⟩

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ (sumCompl q) (Sum.map (⇑e) (⇑e.toCompl) ((sumCompl p).symm x)) = ↑(e.toCompl ⟨x, hx⟩)

Tactic:
rw [sumCompl_apply_symm_of_neg _ _ hx, Sum.map_inr, sumCompl_apply_inr]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ (e.subtypeCongr e.toCompl) x = ↑(e.toCompl ⟨x, hx⟩)

Tactic:
simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]

Result:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ (sumCompl q) (Sum.map (⇑e) (⇑e.toCompl) ((sumCompl p).symm x)) = ↑(e.toCompl ⟨x, hx⟩)

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)

Tactic:
dsimp only [extendSubtype]

Result:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ (e.subtypeCongr e.toCompl) x = ↑(e.toCompl ⟨x, hx⟩)