harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
theorem vertex_mem_convexHull_iff (hx : x ∈ K.vertices) (hs : s ∈ K.faces) :
    x ∈ convexHull 𝕜 (s : Set E) ↔ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s

Tactic:
classical
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
by_contra H
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
  coe_empty, convexHull_empty] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False

Tactic:
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
  coe_empty, convexHull_empty] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s

Tactic:
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s

Tactic:
by_contra H

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h✝ : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
⊢ x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => subset_convexHull 𝕜 _ h⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ (convexHull 𝕜) ↑{x}

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/SMul.lean
theorem single_smul (a b : α) (f : α → M) (r : R) : single a r b • f a = single a (r • f b) b

Proof state:
α : Type u_1
M : Type u_3
R : Type u_6
inst✝² : Zero M
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R M
a b : α
f : α → M
r : R
⊢ (single a r) b • f a = (single a (r • f b)) b

Tactic:
by_cases h : a = b <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∃ x, x ∈ as.toList ∧ p x = true) ↔ ∃ i x, p as[i] = true

Tactic:
simp only [List.mem_iff_getElem, getElem_toList]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∃ x, (∃ i h, as[i] = x) ∧ p x = true) ↔ ∃ i x, p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.toList.any p = as.any p

Tactic:
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∃ x, x ∈ as.toList ∧ p x = true) ↔ ∃ i x, p as[i] = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (∃ x, (∃ i h, as[i] = x) ∧ p x = true) ↔ ∃ i x, p as[i] = true

Tactic:
exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem Polynomial.bernoulli_three_eval_one_quarter :
    (Polynomial.bernoulli 3).eval (1 / 4) = 3 / 64

Proof state:
⊢ eval (1 / 4) (bernoulli 3) = 3 / 64

Tactic:
simp_rw [Polynomial.bernoulli, Finset.sum_range_succ, Polynomial.eval_add,
  Polynomial.eval_monomial]

Result:
⊢ eval (1 / 4) (∑ i ∈ Finset.range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Proof state:
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one zero_ne_one, bernoulli'_zero,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1), bernoulli'_two,
  bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1), bernoulli'_three]

Result:
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      0 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Proof state:
⊢ eval (1 / 4) (∑ i ∈ Finset.range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) +
            _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) +
          _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
rw [Finset.sum_range_zero, Polynomial.eval_zero, zero_add, bernoulli_one]

Result:
⊢ _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Proof state:
⊢ 3 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      0 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 2 ≠ 1

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem c_eq_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    φ P.c = φ P.a * (x * y + x * z + y * z)

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.c = φ P.a * (x * y + x * z + y * z)

Tactic:
injection eq_sum_three_roots ha h3

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_lt_iff {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : 0 ≺[m] d) :
    m.degree f ≺[m] d ↔ ∀ c ∈ f.support, c ≺[m] d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ f.support.sup ⇑m.toSyn < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
exact Finset.sup_lt_iff hd

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : m.toSyn 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
simp only [map_zero] at hd

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
simp only [AddEquiv.apply_symm_apply]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ f.support.sup ⇑m.toSyn < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
unfold degree

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d
-- Mathlib/Data/Finsupp/AList.lean
theorem empty_lookupFinsupp : lookupFinsupp (∅ : AList fun _x : α => M) = 0

Proof state:
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ∅.lookupFinsupp a✝ = 0 a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ ∅.lookupFinsupp = 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ∅.lookupFinsupp a✝ = 0 a✝

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ ∅.lookupFinsupp = 0

Tactic:
classical
  ext
  simp

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem eval₂ :
    Polynomial.eval₂ (Subring.subtype <| (FixedPoints.subfield G F).toSubring) x (minpoly G F x) =
      0

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (subfield G F).subtype (minpoly G F x)) = Polynomial.eval x (prodXSubSMul G F x)

Tactic:
simp only [minpoly, Polynomial.map_toSubring]

Result:
no goals

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0

Tactic:
rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (subfield G F).subtype (minpoly G F x)) = Polynomial.eval x (prodXSubSMul G F x)
-- Mathlib/CategoryTheory/Pi/Basic.lean
theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙ Pi.eval C i = f i

Proof state:
case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝

Tactic:
rfl

Result:
no goals

Proof state:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ = eqToHom ⋯ ≫ (f i).map f✝ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
⊢ pi' f ⋙ Pi.eval C i = f i

Tactic:
apply Functor.ext

Result:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), (pi' f ⋙ Pi.eval C i).map f_1 = eqToHom ⋯ ≫ (f i).map f_1 ≫ eqToHom ⋯) _auto✝

case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X

Proof state:
case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X

Tactic:
intro _

Result:
case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝

Proof state:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), (pi' f ⋙ Pi.eval C i).map f_1 = eqToHom ⋯ ≫ (f i).map f_1 ≫ eqToHom ⋯) _auto✝

Tactic:
intro _ _ _

Result:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ = eqToHom ⋯ ≫ (f i).map f✝ ≫ eqToHom ⋯
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformly.comp (h : TendstoUniformly F f p) (g : γ → α) :
    TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
g : γ → α
⊢ TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p

Tactic:
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter] at h ⊢

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p ⊤

Tactic:
simpa [principal_univ, comap_principal] using h.comp g

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_inv_iff_mul_le_one_right : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
  (mul_le_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a * b ≤ b⁻¹ * b ↔ a * b ≤ 1

Tactic:
rw [inv_mul_cancel]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn
    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
      ((x + ·)⁻¹' (insert x s) ∩ EMetric.ball (0 : E) r)

Proof state:
case intro.intro.refine_1
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ EMetric.ball 0 r ∈ 𝓝[(fun x_1 => x + x_1) ⁻¹' insert x s] y

Tactic:
apply mem_nhdsWithin_of_mem_nhds

Result:
case intro.intro.refine_1.h
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ EMetric.ball 0 r ∈ 𝓝 y

Proof state:
case intro.intro.refine_2
𝕜 : 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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 r
r' : ℝ≥0
yr' : edist y 0 < ↑r'
hr' : ↑r' < r
this : EMetric.ball 0 ↑r' ∈ 𝓝 y
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ y ∈ (fun x_1 => x + x_1) ⁻¹' insert x s ∩ EMetric.ball 0 ↑r',
      ((fun y => f (x + y)) y, (fun n y => p.partialSum n y) n y) ∈ u

Tactic:
simpa [Metric.emetric_ball_nnreal] using hf.tendstoUniformlyOn hr' u hu

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_inv (s : Finset α) : s.preimage (·⁻¹) inv_injective.injOn = s⁻¹ :=
  coe_injective <| by rw [coe_preimage, Set.inv_preimage, coe_inv]

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s : Finset α
⊢ ↑(s.preimage (fun x => x⁻¹) ⋯) = ↑s⁻¹

Tactic:
rw [coe_preimage, Set.inv_preimage, coe_inv]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_add_gt (b₁ : R) (_ : a + b₂ = c) : a + (b₁ + b₂) = b₁ + c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)

Tactic:
simp [add_left_comm]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem prod_alternatingWord_eq_prod_alternatingWord_sub (i i' : B) (m : ℕ) (hm : m ≤ M i i' * 2) :
    π (alternatingWord i i' m) = π (alternatingWord i' i (M i i' * 2 - m))

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))

Tactic:
simp_rw [prod_alternatingWord_eq_mul_pow, ← Int.even_coe_nat]

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((M.M i i' * 2 - m) / 2)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ Even (2 * k)

Tactic:
use k

Result:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 2 * k = k + k

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ Even (↑(M.M i i') * 2 - 2 * k)

Tactic:
use -k + (M i i')

Result:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ ↑(M.M i i') * 2 - 2 * k = -k + ↑(M.M i i') + (-k + ↑(M.M i i'))

Proof state:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ (1 / 2 + k) =
    cs.simple i * (cs.simple i' * cs.simple i) ^ (-1 / 2 + (-k + ↑(M.M i i')))

Tactic:
norm_num

Result:
case intro.inr
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
this✝ : ¬Even (2 * k + 1)
this : ¬Even (↑(M.M i i') * 2 - (2 * k + 1))
⊢ cs.simple i' * (cs.simple i * cs.simple i') ^ k =
    cs.simple i * (cs.simple i' * cs.simple i) ^ (-1 + (-k + ↑(M.M i i')))

Proof state:
case intro.inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ k = 1 * (1 * (cs.simple i' * cs.simple i)⁻¹ ^ k)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equiv_iff_eq_of_Z_eq' {P Q : Fin 3 → R} (hz : P z = Q z) (mem : Q z ∈ nonZeroDivisors R) :
    P ≈ Q ↔ P = Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = Q z
⊢ (fun m => m • Q) u = Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q ↔ P = Q

Tactic:
refine ⟨?_, by rintro rfl; exact Setoid.refl _⟩

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P ≈ Q → P = Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = 1 * Q z
⊢ (fun m => m • Q) u = Q

Tactic:
simp_rw [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors mem).mp hz, one_smul]

Result:
no goals

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = Q z
⊢ (fun m => m • Q) u = Q

Tactic:
rw [← one_mul (Q z)] at hz

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
mem : Q z ∈ nonZeroDivisors R
u : Rˣ
hz : (fun m => m • Q) u z = 1 * Q z
⊢ (fun m => m • Q) u = Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hz : P z = Q z
mem : Q z ∈ nonZeroDivisors R
⊢ P = Q → P ≈ Q

Tactic:
rintro rfl

Result:
R : Type r
inst✝ : CommRing R
P : Fin 3 → R
hz : P z = P z
mem : P z ∈ nonZeroDivisors R
⊢ P ≈ P

Proof state:
R : Type r
inst✝ : CommRing R
P : Fin 3 → R
hz : P z = P z
mem : P z ∈ nonZeroDivisors R
⊢ P ≈ P

Tactic:
exact Setoid.refl _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem mul_comm (x y : BitVec w) : x * y = y * x

Proof state:
w : Nat
x y : BitVec w
⊢ x * y = y * x

Tactic:
apply eq_of_toFin_eq

Result:
case a
w : Nat
x y : BitVec w
⊢ (x * y).toFin = (y * x).toFin

Proof state:
case a
w : Nat
x y : BitVec w
⊢ (x * y).toFin = (y * x).toFin

Tactic:
simpa using Fin.mul_comm ..

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zpow_add₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n

Proof state:
case hp
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

Tactic:
simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]

Result:
no goals

Proof state:
case hz
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
induction n with
| hz => simp
| hp n ihn => simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]

Result:
no goals

Proof state:
case hn
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)

Tactic:
rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sdiff_inf : a ∆ b \ (a ⊓ b) = a ∆ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b

Tactic:
rw [symmDiff_sdiff]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b

Tactic:
simp [symmDiff]

Result:
no goals