harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean
theorem IsLocalExtr.hasLineDerivAt_eq_zero (h : IsLocalExtr f a) (hd : HasLineDerivAt ℝ f f' a b) :
    f' = 0 :=
  IsExtrFilter.hasLineDerivAt_eq_zero h hd <| Continuous.tendsto' (by fun_prop) _ _ (by simp)

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalExtr f a
hd : HasLineDerivAt ℝ f f' a b
⊢ a + 0 • b = a

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalExtr f a
hd : HasLineDerivAt ℝ f f' a b
⊢ Continuous fun t => a + t • b

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjUnion_singleton (s : Finset α) (a : α) (h : Disjoint s {a}) :
    disjUnion s {a} h = cons a s (disjoint_singleton_right.mp h)

Proof state:
α : Type u_1
s : Finset α
a : α
h : Disjoint s {a}
⊢ s.disjUnion {a} h = cons a s ⋯

Tactic:
rw [disjUnion_comm, singleton_disjUnion]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem isUnitTrinomial_iff'' (h : p * p.mirror = q * q.mirror) :
    p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Proof state:
p q : ℤ[X]
h : p * p.mirror = q * q.mirror
⊢ p.IsUnitTrinomial ↔ q.IsUnitTrinomial

Tactic:
rw [isUnitTrinomial_iff', isUnitTrinomial_iff', h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_allOnes : ~~~ allOnes w = 0#w

Proof state:
w : Nat
⊢ ~~~allOnes w = 0#w

Tactic:
ext

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w
⊢ (~~~allOnes w).getLsbD i✝ = (0#w).getLsbD i✝

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w
⊢ (~~~allOnes w).getLsbD i✝ = (0#w).getLsbD i✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.smul {f : E → 𝕜} {g : E → F} (hf : ContDiffAt 𝕜 n f x)
    (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x • g x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → 𝕜
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (fun x => f x • g x) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → 𝕜
g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => f x • g x) univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f : E → 𝕜
g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (fun x => f x • g x) univ x

Tactic:
exact hf.smul hg

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem isNormal_veblenWith' (f : Ordinal → Ordinal) (h : o ≠ 0) : IsNormal (veblenWith f o)

Proof state:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (derivFamily fun x => veblenWith f ↑x)

Tactic:
exact isNormal_derivFamily _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (veblenWith f o)

Tactic:
rw [veblenWith_of_ne_zero f h]

Result:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ IsNormal (derivFamily fun x => veblenWith f ↑x)
-- Mathlib/Data/Nat/Count.lean
theorem count_monotone : Monotone (count p) :=
  monotone_nat_of_le_succ fun n ↦ by by_cases h : p n <;> simp [count_succ, h]

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ count p (n + 1)

Tactic:
by_cases h : p n <;> simp [count_succ, h]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_congr' {p : ι → Prop} {f g : (i : ι) → p i → α}
    (h : ∀ i (hi : p i), f i hi = g i hi) :
    ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi

Proof state:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ ⨆ (hi : p i), f i hi = ⨆ (hi : p i), g i hi

Tactic:
congr

Result:
case e_s.h.e_s
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ (fun hi => f i hi) = fun hi => g i hi

Proof state:
case e_s
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ (fun i => ⨆ (hi : p i), f i hi) = fun i => ⨆ (hi : p i), g i hi

Tactic:
ext i

Result:
case e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ ⨆ (hi : p i), f i hi = ⨆ (hi : p i), g i hi

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ ⨆ i, ⨆ (hi : p i), f i hi = ⨆ i, ⨆ (hi : p i), g i hi

Tactic:
congr

Result:
case e_s
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
⊢ (fun i => ⨆ (hi : p i), f i hi) = fun i => ⨆ (hi : p i), g i hi

Proof state:
case e_s.h.e_s
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
⊢ (fun hi => f i hi) = fun hi => g i hi

Tactic:
ext hi

Result:
case e_s.h.e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
hi : p i
⊢ f i hi = g i hi

Proof state:
case e_s.h.e_s.h
α : Type u_1
ι : Sort u_4
inst✝ : SupSet α
p : ι → Prop
f g : (i : ι) → p i → α
h : ∀ (i : ι) (hi : p i), f i hi = g i hi
i : ι
hi : p i
⊢ f i hi = g i hi

Tactic:
exact h i hi

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem directedOn_sUnion {r} {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S)
    (h : ∀ x ∈ S, DirectedOn r x) : DirectedOn r (⋃₀ S)

Proof state:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ i, ↑i)

Tactic:
exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Result:
α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃ i, ↑i)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffAt.fderiv {f : E → F → G} {g : E → F}
    (hf : ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀)) (hg : ContDiffAt 𝕜 m g x₀)
    (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x₀ : E
m n : WithTop ℕ∞
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀

Tactic:
simp_rw [← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x₀ : E
m n : WithTop ℕ∞
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) univ (g x)) x₀

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x₀ : E
m n : WithTop ℕ∞
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ univ ⊆ g ⁻¹' univ

Tactic:
rw [preimage_univ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x₀ : E
m n : WithTop ℕ∞
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) univ (g x)) x₀

Tactic:
refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
  hmn (mem_univ x₀) ?_).contDiffAt univ_mem

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x₀ : E
m n : WithTop ℕ∞
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ univ ⊆ g ⁻¹' univ
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma dft_const_smul {R : Type*} [DistribSMul R E] [SMulCommClass R ℂ E] (r : R) (Φ : ZMod N → E) :
    𝓕 (r • Φ) = r • 𝓕 Φ

Proof state:
N : ℕ
inst✝⁴ : NeZero N
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℂ E
R : Type u_2
inst✝¹ : DistribSMul R E
inst✝ : SMulCommClass R ℂ E
r : R
Φ : ZMod N → E
⊢ 𝓕 (r • Φ) = r • 𝓕 Φ

Tactic:
simp only [Pi.smul_def, dft_def, smul_sum, smul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerRight_η_ε (T : D) : η F ▷ T ≫ ε F ▷ T = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
T : D
⊢ η F ▷ T ≫ ε F ▷ T = 𝟙 (F.obj (𝟙_ C) ⊗ T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, η_ε, id_whiskerRight]

Result:
no goals
-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_algebraMap {F K : Type*} [Field F] [Field K] [Differential F] [Differential K]
    [Algebra F K] [DifferentialAlgebra F K]
    (a : F) : logDeriv (algebraMap F K a) = algebraMap F K (logDeriv a)

Proof state:
F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ ((algebraMap F K) a)′ / (algebraMap F K) a = (algebraMap F K) (a′ / a)

Tactic:
simp [deriv_algebraMap]

Result:
no goals

Proof state:
F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ logDeriv ((algebraMap F K) a) = (algebraMap F K) (logDeriv a)

Tactic:
unfold logDeriv

Result:
F : Type u_2
K : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Differential F
inst✝² : Differential K
inst✝¹ : Algebra F K
inst✝ : DifferentialAlgebra F K
a : F
⊢ ((algebraMap F K) a)′ / (algebraMap F K) a = (algebraMap F K) (a′ / a)
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem map_restrictScalars_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] D) :
    ((map f g).restrictScalars R).comp includeRight = includeRight.comp g :=
  AlgHom.ext <| by simp

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (x : B), ((AlgHom.restrictScalars R (map f g)).comp includeRight) x = (includeRight.comp g) x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem hom.faithful : ∀ c d, Function.Injective fun f : c ⟶ d => (hom S).map f

Proof state:
case mk.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hf : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
g : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hg : g ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
hfg : (fun f => S.hom.map f) ⟨f, hf⟩ = (fun f => S.hom.map f) ⟨g, hg⟩
⊢ ⟨f, hf⟩ = ⟨g, hg⟩

Tactic:
exact Subtype.eq hfg

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (c d : ↑S.objs), Function.Injective fun f => S.hom.map f

Tactic:
rintro ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, hf⟩ ⟨g, hg⟩ hfg

Result:
case mk.mk.mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hf : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
g : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩
hg : g ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩
hfg : (fun f => S.hom.map f) ⟨f, hf⟩ = (fun f => S.hom.map f) ⟨g, hg⟩
⊢ ⟨f, hf⟩ = ⟨g, hg⟩
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero
    (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) : ∀ y ∈ EMetric.ball x r, f 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ EMetric.ball x r
⊢ f y = 0

Tactic:
rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]

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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ EMetric.ball x r
⊢ (∑ k ∈ Finset.range 0, (pf k) fun x_1 => y - x) = 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
⊢ ∀ y ∈ EMetric.ball x r, f y = 0

Tactic:
intro y 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ EMetric.ball x r
⊢ f 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ EMetric.ball x r
⊢ (∑ k ∈ Finset.range 0, (pf k) fun x_1 => y - x) = 0

Tactic:
simp only [Finset.range_zero, Finset.sum_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_flatten (f : β → α → β) (b : β) (L : Array (Array α)) :
    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b

Proof state:
case of
β : Type u_1
α : Type u_2
f : β → α → β
b : β
xss✝ : List (List α)
⊢ foldl f b (List.map List.toArray xss✝).toArray.flatten =
    foldl (fun b l => foldl f b l) b (List.map List.toArray xss✝).toArray

Tactic:
simp [List.foldl_flatten, List.foldl_map]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
b : β
L : Array (Array α)
⊢ foldl f b L.flatten = foldl (fun b l => foldl f b l) b L

Tactic:
cases L using array₂_induction

Result:
case of
β : Type u_1
α : Type u_2
f : β → α → β
b : β
xss✝ : List (List α)
⊢ foldl f b (List.map List.toArray xss✝).toArray.flatten =
    foldl (fun b l => foldl f b l) b (List.map List.toArray xss✝).toArray
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivRight_X_none : optionEquivRight R S₁ (X none) = C Polynomial.X

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X

Tactic:
simp [optionEquivRight_apply, aeval_X]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tight.lean
protected lemma subset (hT : IsTightMeasureSet T) (hST : S ⊆ T) :
    IsTightMeasureSet S :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hT (fun _ ↦ by simp)
    (iSup_le_iSup_of_subset hST)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hT : IsTightMeasureSet T
hST : S ⊆ T
x✝ : Set α
⊢ 0 ≤ (⨆ μ ∈ S, ⇑μ) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)]
lemma antivaryOn_inv_right : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_swap

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem mul_slash_SL2 (k1 k2 : ℤ) (A : SL(2, ℤ)) (f g : ℍ → ℂ) :
    (f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A :=
  calc
    (f * g) ∣[k1 + k2] (A : GL(2, ℝ)⁺) =
        ((↑ₘA).det : ℝ) • f ∣[k1] A * g ∣[k2] A

Proof state:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (↑↑↑A).det • f ∣[k1] A * g ∣[k2] A = 1 • f ∣[k1] A * g ∣[k2] A

Tactic:
rw [det_coe]

Result:
no goals

Proof state:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] ↑A = (↑↑↑A).det • f ∣[k1] A * g ∣[k2] A

Tactic:
apply mul_slash

Result:
no goals

Proof state:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ 1 • f ∣[k1] A * g ∣[k2] A = f ∣[k1] A * g ∣[k2] A

Tactic:
rw [one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False

Proof state:
u v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ v → u + k₂ < v

Tactic:
omega

Result:
no goals

Proof state:
u v k₁ k₂ : Nat
⊢ isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ v → u + k₂ < v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_total : ∀ (x y : Bool), x ≤ y ∨ y ≤ x

Proof state:
⊢ ∀ (x y : Bool), x ≤ y ∨ y ≤ x

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetAux_perm_powersetAux' {l : List α} : powersetAux l ~ powersetAux' l

Proof state:
α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l

Tactic:
exact (sublists_perm_sublists' _).map _

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ powersetAux l ~ powersetAux' l

Tactic:
rw [powersetAux_eq_map_coe]

Result:
α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l
-- Mathlib/Tactic/Ring/Basic.lean
theorem sub_congr {R} [Ring R] {a a' b b' c : R} (_ : a = a') (_ : b = b')
    (_ : a' - b' = c) : (a - b : R) = c

Proof state:
R : Type u_2
inst✝ : Ring R
a' b' : R
⊢ a' - b' = a' - b'

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' - b' = c
⊢ a - b = c

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a' b' : R
⊢ a' - b' = a' - b'
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullbackSymmetry_hom_comp_fst [HasPullback f g] :
    (pullbackSymmetry f g).hom ≫ pullback.fst g f = pullback.snd f g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).hom ≫ pullback.fst g f = pullback.snd f g

Tactic:
simp [pullbackSymmetry]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_eq_zero_iff' {θ : ℝ} (hθ : cos θ ≠ 0) : tan θ = 0 ↔ ∃ k : ℤ, k * π = θ

Proof state:
θ : ℝ
⊢ cos θ ≠ 0 → (tan θ = 0 ↔ ∃ k, ↑k * π = θ)

Tactic:
exact_mod_cast @Complex.tan_eq_zero_iff' θ

Result:
no goals

Proof state:
θ : ℝ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ k, ↑k * π = θ

Tactic:
revert hθ

Result:
θ : ℝ
⊢ cos θ ≠ 0 → (tan θ = 0 ↔ ∃ k, ↑k * π = θ)
-- Mathlib/Data/Ordmap/Ordset.lean
theorem equiv_iff {t₁ t₂ : Ordnode α} (h₁ : Sized t₁) (h₂ : Sized t₂) :
    Equiv t₁ t₂ ↔ toList t₁ = toList t₂ :=
  and_iff_right_of_imp fun h => by rw [← length_toList h₁, h, length_toList h₂]

Proof state:
α : Type u_1
t₁ t₂ : Ordnode α
h₁ : t₁.Sized
h₂ : t₂.Sized
h : t₁.toList = t₂.toList
⊢ t₁.size = t₂.size

Tactic:
rw [← length_toList h₁, h, length_toList h₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sign_sign : sign (sign x) = sign x

Proof state:
x : Int
n✝ : Nat
⊢ (ofNat (n✝ + 1)).sign.sign = (ofNat (n✝ + 1)).sign

Tactic:
rfl

Result:
no goals

Proof state:
x : Int
⊢ x.sign.sign = x.sign

Tactic:
match x with
| 0 => rfl
| .ofNat (_ + 1) => rfl
| .negSucc _ => rfl

Result:
no goals

Proof state:
x : Int
⊢ (sign 0).sign = sign 0

Tactic:
rfl

Result:
no goals

Proof state:
x : Int
a✝ : Nat
⊢ -[a✝+1].sign.sign = -[a✝+1].sign

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
lemma iSup_sequence_lt_omega1 {α : Type u} [Countable α]
    (o : α → Ordinal.{max u v}) (ho : ∀ n, o n < (aleph 1).ord) :
    iSup o < (aleph 1).ord

Proof state:
α : Type u
inst✝ : Countable α
o : α → Ordinal.{max u v}
ho : ∀ (n : α), o n < (ℵ_ 1).ord
⊢ Cardinal.lift.{v, u} #α < (ℵ_ 1).ord.cof

Tactic:
rw [Cardinal.isRegular_aleph_one.cof_eq]

Result:
α : Type u
inst✝ : Countable α
o : α → Ordinal.{max u v}
ho : ∀ (n : α), o n < (ℵ_ 1).ord
⊢ Cardinal.lift.{v, u} #α < ℵ_ 1

Proof state:
α : Type u
inst✝ : Countable α
o : α → Ordinal.{max u v}
ho : ∀ (n : α), o n < (ℵ_ 1).ord
⊢ Cardinal.lift.{v, u} #α < ℵ_ 1

Tactic:
exact lt_of_le_of_lt mk_le_aleph0 aleph0_lt_aleph_one

Result:
no goals

Proof state:
α : Type u
inst✝ : Countable α
o : α → Ordinal.{max u v}
ho : ∀ (n : α), o n < (ℵ_ 1).ord
⊢ iSup o < (ℵ_ 1).ord

Tactic:
apply iSup_lt_ord_lift _ ho

Result:
α : Type u
inst✝ : Countable α
o : α → Ordinal.{max u v}
ho : ∀ (n : α), o n < (ℵ_ 1).ord
⊢ Cardinal.lift.{v, u} #α < (ℵ_ 1).ord.cof
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_eq_zero_of_char_three (h : W.b₂ = 0) : W.j = 0

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
h : W.b₂ = 0
⊢ W.j = 0

Tactic:
rw [j_eq_zero_iff_of_char_three', h, zero_pow (Nat.succ_ne_zero _)]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem eqOn_of_isPreconnected_of_isMaxOn_norm {f : E → F} {U : Set E} {c : E}
    (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn ℂ f U) (hcU : c ∈ U)
    (hm : IsMaxOn (norm ∘ f) U c) : EqOn f (const E (f c)) U := fun x hx =>
  have H₁ : ‖f x‖ = ‖f c‖ := norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hd hcU hm hx
  have H₂ : ‖f x + f c‖ = ‖f c + f c‖ :=
    norm_eqOn_of_isPreconnected_of_isMaxOn hc ho (hd.add_const _) hcU hm.norm_add_self hx
  eq_of_norm_eq_of_norm_add_eq H₁ <| by simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : E
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + Function.const E (f c) x‖ = ‖f x‖ + ‖Function.const E (f c) x‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

Result:
no goals