harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Composition.lean
theorem id_comp (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0 → E) :
    (id 𝕜 F (p 0 v0)).comp p = p

Proof state:
case h.inr.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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos)) v = (p n) v

Tactic:
rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]

Result:
case h.inr.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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ p.applyComposition (Composition.single n n_pos) v ⟨0, ⋯⟩ = (p n) v

Proof state:
case h.inr.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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

Tactic:
ext v

Result:
case h.inr.h₀.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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p b) v = 0 v

Proof state:
case h.inl.H.h.e_6.h.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
p : FormalMultilinearSeries 𝕜 E F
v0 v : Fin 0 → E
i : Fin 0
⊢ v0 i = v i

Tactic:
exact i.elim0

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
⊢ 1 < b.length

Tactic:
have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb

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
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
this : b.length ≠ 1
⊢ 1 < b.length
-- Mathlib/Probability/StrongLaw.lean
theorem sum_prob_mem_Ioc_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) {K : ℕ} {N : ℕ}
    (hKN : K ≤ N) :
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} ≤ ENNReal.ofReal (𝔼[X] + 1)

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ

Tactic:
apply sum_le_sum fun i _ => ?_

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
i : ℕ
x✝ : i ∈ range N
⊢ (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ

Proof state:
case hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ IntervalIntegrable (fun x => x) ρ 0 ↑N

Tactic:
exact continuous_id.intervalIntegrable _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_map_coe (l : Array α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun i => f i.val) l.attach = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map (fun i => f i.val) { toList := toList✝ }.attach = map f { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map (fun i => f i.val) { toList := toList✝ }.attach = map f { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem FormalMultilinearSeries.hasSum_of_finite (p : FormalMultilinearSeries 𝕜 E F)
    {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
    HasSum (fun n : ℕ => p n fun _ => x) (p.sum x) :=
  summable_of_ne_finset_zero (s := .range n)
    (fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [hn m hm]; rfl)
    |>.hasSum

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ (0 fun x_1 => x) = 0

Tactic:
rfl

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x_1 => x) = 0

Tactic:
rw [hn 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ (0 fun x_1 => 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : m ∉ Finset.range n
⊢ ((p m) fun x_1 => x) = 0

Tactic:
rw [Finset.mem_range, not_lt] at 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ ((p m) fun x_1 => x) = 0
-- Mathlib/Topology/Sheaves/LocalPredicate.lean
theorem PrelocalPredicate.sheafifyOf {T : X → Type v} {P : PrelocalPredicate T} {U : Opens X}
    {f : ∀ x : U, T x} (h : P.pred f) : P.sheafify.pred f := fun x =>
  ⟨U, x.2, 𝟙 _, by convert h⟩

Proof state:
X : TopCat
T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
h : P.pred f
x : ↥U
⊢ P.pred fun x => f ((𝟙 U) x)

Tactic:
convert h

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma equation_neg_iff (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Proof state:
case a.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (-y - W'.a₁ * x - W'.a₃) ^ 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) + W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (-y - W'.a₁ * x - W'.a₃) ^ 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) + W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
      x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆ ↔
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆

Tactic:
congr! 1

Result:
case a.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (-y - W'.a₁ * x - W'.a₃) ^ 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) + W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Tactic:
rw [equation_iff, equation_iff, negY]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ (-y - W'.a₁ * x - W'.a₃) ^ 2 + W'.a₁ * x * (-y - W'.a₁ * x - W'.a₃) + W'.a₃ * (-y - W'.a₁ * x - W'.a₃) =
      x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆ ↔
    y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme.{u})
    {U : X.Opens} (hU : IsCompact U.1) (x f : Γ(X, U))
    (H : x |_ (X.basicOpen f) = 0) :
    ∃ n : ℕ, f ^ n * x = 0

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ ∃ n, f ^ n * x = 0

Tactic:
replace e : U = iSup fun i : s => (i : X.Opens) := by
  ext1; simpa using e

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
⊢ ∃ n, f ^ n * x = 0
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₁_comp_rename {υ : Type*} (f : τ → MvPolynomial υ R) (g : σ → τ) :
    (bind₁ f).comp (rename g) = bind₁ (f ∘ g)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ((bind₁ f).comp (rename g)) (X i) = (bind₁ (f ∘ g)) (X i)

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
⊢ (bind₁ f).comp (rename g) = bind₁ (f ∘ g)

Tactic:
ext1 i

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : τ → MvPolynomial υ R
g : σ → τ
i : σ
⊢ ((bind₁ f).comp (rename g)) (X i) = (bind₁ (f ∘ g)) (X i)
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Basic.lean
theorem sub.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
    (had : ad = a.den / g) (hbd : bd = b.den / g) :
    let den := ad * b.den; let num := a.num * bd - b.num * ad
    num.natAbs.gcd g = num.natAbs.gcd den

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
have := add.aux a (-b) hg had hbd

Result:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  let den := ad * (-b).den;
  let num := a.num * ↑bd + (-b).num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
this : (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd g = (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd (ad * (-b).den)
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
exact this

Result:
no goals

Proof state:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
this :
  let den := ad * (-b).den;
  let num := a.num * ↑bd + (-b).num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den

Tactic:
simp only [show (-b).num = -b.num from rfl, Int.neg_mul] at this

Result:
a b : Rat
g ad bd : Nat
hg : g = a.den.gcd b.den
had : ad = a.den / g
hbd : bd = b.den / g
this : (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd g = (a.num * ↑bd + -(b.num * ↑ad)).natAbs.gcd (ad * (-b).den)
⊢ let den := ad * b.den;
  let num := a.num * ↑bd - b.num * ↑ad;
  num.natAbs.gcd g = num.natAbs.gcd den
-- Mathlib/Analysis/Convex/Exposed.lean
theorem eq_inter_halfSpace' {A B : Set E} (hAB : IsExposed 𝕜 A B) (hB : B.Nonempty) :
    ∃ l : E →L[𝕜] 𝕜, ∃ a, B = { x ∈ A | a ≤ l x }

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hAB hB

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}.Nonempty
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}

Tactic:
obtain ⟨w, hw⟩ := hB

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
w : E
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
w : E
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}

Tactic:
exact ⟨l, l w, Subset.antisymm (fun x hx => ⟨hx.1, hx.2 w hw.1⟩) fun x hx =>
  ⟨hx.1, fun y hy => (hw.2 y hy).trans hx.2⟩⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Reflection.lean
lemma preReflection_apply_self (h : f x = 2) :
    preReflection x f x = - x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
⊢ x - (x + x) = -x

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
⊢ (preReflection x f) x = -x

Tactic:
rw [preReflection_apply, h, two_smul]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
⊢ x - (x + x) = -x
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffOn.ftaylorSeriesWithin
    (h : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) :
    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s

Proof state:
case fderivWithin.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩

Result:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : o ∩ s ⊆ u
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Proof state:
case fderivWithin.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
this✝ : ↑(m + 1) ≤ n
u : Set E
hu : u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
Hp : HasFTaylorSeriesUpToOn (↑(m + 1)) f p u
o : Set E
o_open : IsOpen o
xo : x ∈ o
ho : s ∩ o ⊆ u
this : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ
A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m
⊢ HasFDerivWithinAt (fun x => ftaylorSeriesWithin 𝕜 f s x m) (p x m.succ).curryLeft (s ∩ o) x

Tactic:
exact
  ((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr
    (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm

Result:
no goals

Proof state:
case zero_eq
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ContDiffOn 𝕜 n f s
hs : UniqueDiffOn 𝕜 s
x : E
a✝ : x ∈ s
⊢ (ftaylorSeriesWithin 𝕜 f s x 0).curry0 = f x

Tactic:
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
  iteratedFDerivWithin_zero_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
lemma LieModule.toEnd_pow_lie (x y : L) (z : M) (n : ℕ) :
    ((φ x) ^ n) ⁅y, z⁆ =
      ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L x) ^ ij.1) y, ((φ x) ^ ij.2) z⁆

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ (φ x ^ (n + 1)) ⁅y, z⁆ = ∑ ij ∈ antidiagonal (n + 1), (n + 1).choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆

Tactic:
rw [Finset.sum_antidiagonal_choose_succ_nsmul
  (fun i j ↦ ⁅((ad R L x) ^ i) y, ((φ x) ^ j) z⁆) n]

Result:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ (φ x ^ (n + 1)) ⁅y, z⁆ =
    ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ (ij.2 + 1)) z⁆ +
      ∑ ij ∈ antidiagonal n, n.choose ij.2 • ⁅((ad R L) x ^ (ij.1 + 1)) y, (φ x ^ ij.2) z⁆
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) :
    SeparableSpace s

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure (Subtype.val '' t)
⊢ SeparableSpace ↑s

Tactic:
refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure (Subtype.val '' t)
⊢ Dense t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
⊢ SeparableSpace ↑s

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set α
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure t
⊢ SeparableSpace ↑s

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure (Subtype.val '' t)
⊢ Dense t

Tactic:
rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set α
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure t
⊢ SeparableSpace ↑s

Tactic:
lift t to Set s using hts

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure (Subtype.val '' t)
⊢ SeparableSpace ↑s
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem left_lt_right {x : PGame} (o : Numeric x) (i : x.LeftMoves) (j : x.RightMoves) :
    x.moveLeft i < x.moveRight j

Proof state:
x : PGame
o : x.Numeric
i : x.LeftMoves
j : x.RightMoves
⊢ x.moveLeft i < x.moveRight j

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves
j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i < (PGame.mk α✝ β✝ a✝¹ a✝).moveRight j

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
i : (PGame.mk α✝ β✝ a✝¹ a✝).LeftMoves
j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (PGame.mk α✝ β✝ a✝¹ a✝).moveLeft i < (PGame.mk α✝ β✝ a✝¹ a✝).moveRight j

Tactic:
exact o.1 i j

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem le_opNorm_mul_pow_card_of_le (f : ContinuousMultilinearMap 𝕜 E G) {m b} (hm : ‖m‖ ≤ b) :
    ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
b : ℝ
hm : ‖m‖ ≤ b
⊢ ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι

Tactic:
simpa only [prod_const] using f.le_opNorm_mul_prod_of_le fun i => (norm_le_pi_norm m i).trans hm

Result:
no goals
-- Mathlib/Data/Finsupp/Lex.lean
theorem lex_le_iff_of_unique [Unique α] {a b : Lex (α →₀ N)} :
    a ≤ b ↔ ofLex a default ≤ ofLex b default

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a = b ↔ (ofLex a) default = (ofLex b) default

Tactic:
conv_lhs => rw [← toLex_ofLex a, ← toLex_ofLex b, toLex_inj]

Result:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ ofLex a = ofLex b ↔ (ofLex a) default = (ofLex b) default

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a = b ∨ a < b ↔ (ofLex a) default = (ofLex b) default ∨ (ofLex a) default < (ofLex b) default

Tactic:
apply or_congr _ lex_lt_iff_of_unique

Result:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a = b ↔ (ofLex a) default = (ofLex b) default

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ ofLex a = ofLex b ↔ (ofLex a) default = (ofLex b) default

Tactic:
simp only [Finsupp.ext_iff, Unique.forall_iff]

Result:
no goals

Proof state:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a ≤ b ↔ (ofLex a) default ≤ (ofLex b) default

Tactic:
simp only [le_iff_eq_or_lt, EmbeddingLike.apply_eq_iff_eq]

Result:
α : Type u_1
N : Type u_2
inst✝³ : Zero N
inst✝² : LinearOrder α
inst✝¹ : PartialOrder N
inst✝ : Unique α
a b : Lex (α →₀ N)
⊢ a = b ∨ a < b ↔ (ofLex a) default = (ofLex b) default ∨ (ofLex a) default < (ofLex b) default