harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_map_hom' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : Array α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) (w : start = l.size) :
    (l.map g).foldr f' (g a) start 0 = g (l.foldr f a)

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldr f' (g a) (List.map g toList✝) = g (List.foldr f a toList✝)

Tactic:
rw [List.foldr_map_hom _ _ _ _ _ h]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldr f' (g a) (map g { toList := toList✝ }) { toList := toList✝ }.size = g (foldr f a { toList := toList✝ })

Tactic:
simp

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ List.foldr f' (g a) (List.map g toList✝) = g (List.foldr f a toList✝)

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldr f' (g a) (map g l) l.size = g (foldr f a l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
toList✝ : List α
⊢ foldr f' (g a) (map g { toList := toList✝ }) { toList := toList✝ }.size = g (foldr f a { toList := toList✝ })

Proof state:
α : Type u_1
β : Type u_2
start : Nat
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
w : start = l.size
⊢ foldr f' (g a) (map g l) start = g (foldr f a l)

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : Array α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldr f' (g a) (map g l) l.size = g (foldr f a l)
-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Util/Compare.lean
theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α}
[Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq

Proof state:
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableEq α
a : α
inst✝ : Decidable (a < a)
lt_irrefl : ¬a < a
⊢ compareOfLessAndEq a a = Ordering.eq

Tactic:
simp [compareOfLessAndEq, lt_irrefl]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isOpen_iff_nhds : IsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s :=
  calc
    IsOpen s ↔ s ⊆ interior s := subset_interior_iff_isOpen.symm
    _ ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Tactic:
simp_rw [interior_eq_nhds, subset_def, mem_setOf]

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma IsWeaklyRegular.isWeaklyRegular_lTensor [Module.Flat R M₂]
    {rs : List R} (h : IsWeaklyRegular M rs) :
    IsWeaklyRegular (M₂ ⊗[R] M) rs

Proof state:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
e : M₂ ⊗[R] QuotSMulTop r N ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Result:
no goals

Proof state:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Tactic:
let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N

Result:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (M₂ ⊗[R] QuotSMulTop r N) rs'
e : M₂ ⊗[R] QuotSMulTop r N ≃ₗ[R] QuotSMulTop r (M₂ ⊗[R] N) := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) (r :: rs')

Proof state:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M₂ ⊗[R] M) rs

Tactic:
induction h with
| nil N => exact nil R (M₂ ⊗[R] N)
| @cons N _ _ r rs' h1 _ ih =>
  let e := tensorQuotSMulTopEquivQuotSMulTop r M₂ N
  exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.lTensor M₂)

Result:
no goals

Proof state:
case nil
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsWeaklyRegular (M₂ ⊗[R] N) []

Tactic:
exact nil R (M₂ ⊗[R] N)

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem HasFiniteFPowerSeriesOnBall.eq_partialSum'
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    ∀ y ∈ EMetric.ball x r, ∀ m, n ≤ m →
    f y = p.partialSum m (y - x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y - x ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)

Tactic:
rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball x r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)

Tactic:
rw [EMetric.mem_ball, edist_eq_enorm_sub, ← mem_emetric_ball_zero_iff] at hy

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y - x ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
⊢ ∀ y ∈ EMetric.ball x r, ∀ (m : ℕ), n ≤ m → f y = p.partialSum m (y - x)

Tactic:
intro y hy m hm

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball x r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_of_equiv {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) (hfg : f ≈ g) :
    padicNorm p (f (stationaryPoint hf)) = padicNorm p (g (stationaryPoint hg))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
⊢ False

Tactic:
cases lt_or_le (padicNorm p (g (stationaryPoint hg))) (padicNorm p (f (stationaryPoint hf))) with
| inl hlt =>
  exact norm_eq_of_equiv_aux hf hg hfg h hlt
| inr hle =>
  apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
  exact lt_of_le_of_ne hle h

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False

Tactic:
exact norm_eq_of_equiv_aux hf hg hfg h hlt

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))

Tactic:
exact lt_of_le_of_ne hle h

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))

Tactic:
by_contra h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
⊢ False

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ False

Tactic:
apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))
-- Mathlib/Probability/StrongLaw.lean
theorem abs_truncation_le_abs_self (f : α → ℝ) (A : ℝ) (x : α) : |truncation f A x| ≤ |f x|

Proof state:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|

Tactic:
split_ifs

Result:
case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Proof state:
case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Tactic:
simp [abs_nonneg]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
simp only [truncation, indicator, Set.mem_Icc, id, Function.comp_apply]

Result:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_zero_X_mul (φ : MvPowerSeries σ R) (s : σ) : coeff R (0 : σ →₀ ℕ) (X s * φ) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ (coeff R 0) (X s * φ) = 0

Tactic:
rw [← (φ.commute_X s).eq, coeff_zero_mul_X]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[gcongr] lemma height_strictMono {x y : α} (hxy : x < y) (hfin : height x < ⊤) :
    height x < height y

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ height x < height y

Tactic:
rw [← ENat.add_one_le_iff hfin.ne, height_add_const, iSup₂_le_iff]

Result:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length + 1 ≤ height y

Tactic:
have := length_le_height_last (p := p.snoc y (by simp [*]))

Result:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
this : ↑(RelSeries.snoc p y ⋯).length ≤ height (RelSeries.snoc p y ⋯).last
⊢ ↑p.length + 1 ≤ height y

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ RelSeries.last p < y

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y

Tactic:
intro p hlast

Result:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length + 1 ≤ height y

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
p : LTSeries α
hlast : RelSeries.last p = x
this : ↑(RelSeries.snoc p y ⋯).length ≤ height (RelSeries.snoc p y ⋯).last
⊢ ↑p.length + 1 ≤ height y

Tactic:
simpa using this

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem HasFiniteFPowerSeriesOnBall.eq_partialSum
    (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    ∀ y ∈ EMetric.ball (0 : E) r, ∀ m, n ≤ m →
    f (x + y) = p.partialSum m y :=
  fun y hy m hm ↦ (hf.hasSum hy).unique (hasSum_sum_of_ne_finset_zero
    (f := fun m => p m (fun _ => y)) (s := Finset.range m)
    (fun N hN => by simp only; simp only [Finset.mem_range, not_lt] at hN
                    rw [hf.finite _ (le_trans hm hN), ContinuousMultilinearMap.zero_apply]))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
⊢ ((p N) fun x => y) = 0

Tactic:
simp only [Finset.mem_range, not_lt] at hN

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : m ≤ N
⊢ ((p N) fun x => y) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
⊢ (fun m => (p m) fun x => y) N = 0

Tactic:
simp only

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
⊢ ((p N) fun x => y) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ EMetric.ball 0 r
m : ℕ
hm : n ≤ m
N : ℕ
hN : m ≤ N
⊢ ((p N) fun x => y) = 0

Tactic:
rw [hf.finite _ (le_trans hm hN), ContinuousMultilinearMap.zero_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma exists_maximal_isMatchingFree [Finite V] (h : G.IsMatchingFree) :
    ∃ Gmax : SimpleGraph V, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧
      ∀ G', G' > Gmax → ∃ M : Subgraph G', M.IsPerfectMatching

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
obtain ⟨Gmax, hGmax⟩ := Finite.exists_le_maximal h

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
Gmax : SimpleGraph V
hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
Gmax : SimpleGraph V
hGmax : G ≤ Gmax ∧ Maximal IsMatchingFree Gmax
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching

Tactic:
exact ⟨Gmax, ⟨hGmax.1, ⟨hGmax.2.prop, fun _ h' ↦ hGmax.2.not_prop_of_gt h'⟩⟩⟩

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ∃ M, M.IsPerfectMatching

Tactic:
simp_rw [← @not_forall_not _ Subgraph.IsPerfectMatching]

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : G.IsMatchingFree
⊢ ∃ Gmax, G ≤ Gmax ∧ Gmax.IsMatchingFree ∧ ∀ G' > Gmax, ¬∀ (x : G'.Subgraph), ¬x.IsPerfectMatching
-- Mathlib/Data/Complex/Module.lean
@[simp]
lemma realPart_ofReal (r : ℝ) : (ℜ (r : ℂ) : ℂ) = r

Proof state:
r : ℝ
⊢ ↑(ℜ ↑r) = ↑r

Tactic:
rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]

Result:
r : ℝ
⊢ 2⁻¹ • 2 • ↑r = ↑r

Proof state:
r : ℝ
⊢ 2⁻¹ • 2 • ↑r = ↑r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.reverse (h : l ~r l') : l.reverse ~r l'.reverse

Proof state:
α : Type u
l l' : List α
h : l ~r l'
⊢ l.reverse ~r l'.reverse

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse

Proof state:
case intro
α : Type u
l : List α
n : ℕ
⊢ l.reverse ~r (l.rotate n).reverse

Tactic:
exact ⟨_, (reverse_rotate _ _).symm⟩

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem mono (h : t.WellFoundedOn r') (hle : r ≤ r') (hst : s ⊆ t) :
    s.WellFoundedOn r

Proof state:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
exact Subrelation.wf (fun xy => ⟨hle _ _ xy.1, hst xy.2.1, hst xy.2.2⟩) h

Result:
no goals

Proof state:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : t.WellFoundedOn r'
hle : r ≤ r'
hst : s ⊆ t
⊢ s.WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff] at *

Result:
α : Type u_2
r r' : α → α → Prop
s t : Set α
h : WellFounded fun a b => r' a b ∧ a ∈ t ∧ b ∈ t
hle : r ≤ r'
hst : s ⊆ t
⊢ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma LSeriesSummable.of_re_le_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re ≤ s'.re)
    (hf : LSeriesSummable f s) : LSeriesSummable f s'

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : LSeriesSummable f s
⊢ LSeriesSummable f s'

Tactic:
rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢

Result:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable fun x => ‖term f s x‖
⊢ Summable fun x => ‖term f s' x‖

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
hf : Summable fun x => ‖term f s x‖
⊢ Summable fun x => ‖term f s' x‖

Tactic:
exact hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (norm_term_le_of_re_le_re f h)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
lemma op_list_prod : ∀ l : List M, op l.prod = (l.map op).reverse.prod

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Result:
no goals

Proof state:
case nil
M : Type u_4
inst✝ : Monoid M
⊢ op [].prod = (map op []).reverse.prod

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
⊢ ∀ (l : List M), op l.prod = (map op l).reverse.prod

Tactic:
intro l

Result:
M : Type u_4
inst✝ : Monoid M
l : List M
⊢ op l.prod = (map op l).reverse.prod

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod

Tactic:
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_le_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n ≤ toENat c ↔ ↑n ≤ c

Proof state:
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma one_succAbove_one {n : ℕ} : (1 : Fin (n + 3)).succAbove 1 = 2

Proof state:
n : ℕ
⊢ succAbove 1 1 = 2

Tactic:
simpa only [succ_zero_eq_one, val_zero, zero_succAbove, succ_one_eq_two]
  using succ_succAbove_succ (0 : Fin (n + 2)) (0 : Fin (n + 2))

Result:
no goals
-- Mathlib/Algebra/Colimit/Ring.lean
theorem of_injective [IsDirected ι (· ≤ ·)] [DirectedSystem G fun i j h ↦ f' i j h]
    (hf : ∀ i j hij, Function.Injective (f' i j hij)) (i) :
    Function.Injective (of G (fun i j h ↦ f' i j h) i) :=
  have := Nonempty.intro i
  ((ringEquiv _ _).comp_injective _).mp
    fun _ _ eq ↦  DirectLimit.mk_injective f' hf _ (by simpa only [← ringEquiv_of])

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)
i : ι
this : Nonempty ι
x✝¹ x✝ : G i
eq :
  (⇑(ringEquiv G f').toEquiv ∘ ⇑(of G (fun i j h => ⇑(f' i j h)) i)) x✝¹ =
    (⇑(ringEquiv G f').toEquiv ∘ ⇑(of G (fun i j h => ⇑(f' i j h)) i)) x✝
⊢ (fun x => ⟦⟨i, x⟩⟧) x✝¹ = (fun x => ⟦⟨i, x⟩⟧) x✝

Tactic:
simpa only [← ringEquiv_of]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem not_nonempty_empty : ¬PSet.Nonempty ∅

Proof state:
⊢ ¬∅.Nonempty

Tactic:
simp [PSet.Nonempty]

Result:
no goals