harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracket_add_right
    (hW : MDifferentiableAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) x)
    (hW₁ : MDifferentiableAt I I.tangent (fun x ↦ (W₁ x : TangentBundle I M)) x) :
    mlieBracket I V (W + W₁) x =
      mlieBracket I V W x + mlieBracket I V W₁ x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
hW₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W₁ x }) x
⊢ mlieBracket I V (W + W₁) x = mlieBracket I V W x + mlieBracket I V W₁ x

Tactic:
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hW hW₁ ⊢

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
hW₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W₁ x }) x
⊢ mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
hW₁ : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W₁ x }) x
⊢ mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x

Tactic:
exact mlieBracketWithin_add_right hW hW₁ (uniqueMDiffWithinAt_univ _)

Result:
no goals
-- Mathlib/Combinatorics/Derangements/Finite.lean
theorem card_derangements_fin_eq_numDerangements {n : ℕ} :
    card (derangements (Fin n)) = numDerangements n

Proof state:
case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)

Tactic:
rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp] <;> omega

Result:
no goals

Proof state:
case ind.zero
hyp : ∀ m < 0, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin 0)) = numDerangements 0

Tactic:
rfl

Result:
no goals

Proof state:
case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
induction n using Nat.strongRecOn with | ind n hyp => _

Result:
case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n

Proof state:
case ind
n : ℕ
hyp : ∀ m < n, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n

Tactic:
rcases n with _ | _ | n

Result:
case ind.zero
hyp : ∀ m < 0, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin 0)) = numDerangements 0

case ind.succ.zero
hyp : ∀ m < 0 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (0 + 1))) = numDerangements (0 + 1)

case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = numDerangements (n + 1 + 1)
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux6 (x y z : E) :
    (‖(I : 𝕜) • (2 • x + y)‖ * ‖(I : 𝕜) • (2 • x + y)‖ +
    ‖(I : 𝕜) • y - 2 • z‖ * ‖(I : 𝕜) • y - 2 • z‖)
    = 2 * (‖(I : 𝕜) • (x + y) - z‖ * ‖(I : 𝕜) • (x + y) - z‖ +
    ‖(I : 𝕜) • x + z‖ * ‖(I : 𝕜) • x + z‖)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)

Tactic:
convert parallelogram_identity ((I : 𝕜) • (x + y) - z) ((I : 𝕜) • x + z) using 4 <;> module

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem comp_traverse {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : σ ⊕ α) :
    Sum.traverse (Comp.mk ∘ (f <$> ·) ∘ g) x =
    Comp.mk.{u} (Sum.traverse f <$> Sum.traverse g x)

Proof state:
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)

Tactic:
cases x <;> (simp! [Sum.traverse, map_id, functor_norm] <;> rfl)

Result:
no goals

Proof state:
case inr
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) (inr val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))

Tactic:
simp! [Sum.traverse, map_id, functor_norm] <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_mulVec_const_apply [NonAssocSemiring α] {a : α} {v : V} :
    (G.adjMatrix α *ᵥ Function.const _ a) v = G.degree v * a

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
a : α
v : V
⊢ (adjMatrix α G *ᵥ Function.const V a) v = ↑(G.degree v) * a

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem support_eq_symm_image :
    support f = (extChartAt I c).symm '' (ball (extChartAt I c c) f.rOut ∩ range I)

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ support ↑f = ↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
rw [f.support_eq_inter_preimage, ← extChartAt_source I,
  ← (extChartAt I c).symm_image_target_inter_eq', inter_comm,
  ball_inter_range_eq_ball_inter_target]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_sUnion (x : PSet.{u}) : (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Proof state:
x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
ext

Result:
case h
x x✝ : PSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)

Proof state:
case h
x x✝ : PSet.{u}
⊢ x✝ ∈ (⋃₀ x).toSet ↔ x✝ ∈ ⋃₀ (toSet '' x.toSet)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V]
    (hd : finrank ℝ V = n) (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n}
    (hsx₁ : Set.range sx₁.points ⊆ ps) (hsx₂ : Set.range sx₂.points ⊆ ps) :
    sx₁.circumcenter = sx₂.circumcenter

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rcases exists_circumcenter_eq_of_cospherical hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem periodic_circleMap (c : ℂ) (R : ℝ) : Periodic (circleMap c R) (2 * π) := fun θ => by
  simp [circleMap, add_mul, exp_periodic _]

Proof state:
c : ℂ
R θ : ℝ
⊢ circleMap c R (θ + 2 * π) = circleMap c R θ

Tactic:
simp [circleMap, add_mul, exp_periodic _]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem Sublist.prod_dvd_prod [CommMonoid M] {l₁ l₂ : List M} (h : l₁ <+ l₂) :
    l₁.prod ∣ l₂.prod

Proof state:
case intro
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₂.prod

Tactic:
rw [hl.prod_eq, prod_append]

Result:
case intro
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
⊢ l₁.prod ∣ l₂.prod

Tactic:
obtain ⟨l, hl⟩ := h.exists_perm_append

Result:
case intro
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₂.prod

Proof state:
case intro
M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod

Tactic:
exact dvd_mul_right _ _

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem one_antipode (A : Hopf_ C) : A.X.X.one ≫ A.antipode = A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Tactic:
have := (rfl : A.X.X.one ≫ A.X.comul.hom ≫ (A.antipode ▷ A.X.X.X) ≫ A.X.X.mul = _)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul =
    A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul =
    A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Tactic:
conv at this =>
  rhs
  rw [A.antipode_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this : A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul = A.X.X.one ≫ A.X.counit.hom ≫ A.X.X.one
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this : A.X.X.one ≫ A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul = A.X.X.one ≫ A.X.counit.hom ≫ A.X.X.one
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Tactic:
rw [A.X.one_comul_assoc, tensorHom_def, Category.assoc, whisker_exchange_assoc] at this

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  (λ_ (𝟙_ C)).inv ≫ A.X.X.one ▷ 𝟙_ C ≫ A.antipode ▷ 𝟙_ C ≫ A.X.X.X ◁ A.X.X.one ≫ A.X.X.mul =
    A.X.X.one ≫ A.X.counit.hom ≫ A.X.X.one
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  (λ_ (𝟙_ C)).inv ≫ A.X.X.one ▷ 𝟙_ C ≫ A.antipode ▷ 𝟙_ C ≫ A.X.X.X ◁ A.X.X.one ≫ A.X.X.mul =
    A.X.X.one ≫ A.X.counit.hom ≫ A.X.X.one
⊢ A.X.X.one ≫ A.antipode = A.X.X.one

Tactic:
simpa [unitors_inv_equal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_empty_list_le [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.size ≤ l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (insertMany empty l).val.val.size ≤ l.length

Tactic:
rw [← Nat.zero_add l.length]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (insertMany empty l).val.val.size ≤ 0 + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (insertMany empty l).val.val.size ≤ 0 + l.length

Tactic:
apply (size_insertMany_list_le _ Raw.WF.empty₀)

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem absorbs_iff_eventually_nhdsWithin_zero :
    Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝[≠] 0, MapsTo (c • ·) t s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x => c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x => c • x) t s

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun x => c • x) t s

Tactic:
rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x => c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x => c • x) t s
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_le_nat_iff {a : Cardinal.{u}} {n : ℕ} : lift.{v} a ≤ n ↔ a ≤ n

Proof state:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n

Tactic:
rw [← lift_natCast.{v,u}, lift_le]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a :=
  .trans
    ⟨fun h => by rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
    fun h => by
      conv_rhs =>
        rw [← modByMonic_add_div p (monic_X_sub_C a)]
        rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
    IsRoot.def.symm

Proof state:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : (X - C a) * (p /ₘ (X - C a)) = p
⊢ eval a p = 0

Tactic:
rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
⊢ (X - C a) * (p /ₘ (X - C a)) = p

Tactic:
conv_rhs =>
  rw [← modByMonic_add_div p (monic_X_sub_C a)]
  rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]

Result:
no goals
-- Mathlib/Order/Antisymmetrization.lean
theorem wellFoundedLT_antisymmetrization_iff :
    WellFoundedLT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedLT α

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedLT (Antisymmetrization α fun x1 x2 => x1 ≤ x2) ↔ WellFoundedLT α

Tactic:
simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default

Proof state:
α : Type u_1
inst✝ : Inhabited α
a : Array α
⊢ (match a[a.size - 1]? with
    | some e => e
    | none => default) =
    match a[a.size - 1]? with
    | some e => e
    | none => default

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
a : Array α
⊢ a.back! = a.back?.getD default

Tactic:
simp [back!, back?, getElem!_def, Option.getD]

Result:
α : Type u_1
inst✝ : Inhabited α
a : Array α
⊢ (match a[a.size - 1]? with
    | some e => e
    | none => default) =
    match a[a.size - 1]? with
    | some e => e
    | none => default
-- Mathlib/Order/Filter/Map.lean
theorem range_mem_map : range m ∈ map m f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f

Tactic:
exact image_mem_map univ_mem

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_iff_tendsto_nat {f : ℕ → ℝ≥0} {r : ℝ≥0} :
    HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Proof state:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
rw [← ENNReal.hasSum_coe, ENNReal.hasSum_iff_tendsto_nat]

Result:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Proof state:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ↑(∑ a ∈ Finset.range n, f a)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ a ∈ Finset.range n, f a) atTop (𝓝 r)

Tactic:
exact ENNReal.tendsto_coe

Result:
no goals

Proof state:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
simp only [← ENNReal.coe_finset_sum]

Result:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ Tendsto (fun n => ↑(∑ a ∈ Finset.range n, f a)) atTop (𝓝 ↑r) ↔
    Tendsto (fun n => ∑ a ∈ Finset.range n, f a) atTop (𝓝 r)
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
lemma exists_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
    ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Proof state:
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
this : ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)
⊢ ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Tactic:
simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Tactic:
have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
  eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)

Result:
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
this : ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)
⊢ ∃ r, 0 < r ∧ IsCompact (closedBall x r)
-- Mathlib/Algebra/Star/CHSH.lean
theorem tsirelson_inequality_aux : √2 * √2 ^ 3 = √2 * (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹))

Proof state:
case h.e'_2

⊢ √2 ^ 4 = (√2 ^ 2) ^ 2

Tactic:
simp only [← pow_mul]

Result:
case h.e'_2

⊢ √2 ^ 4 = √2 ^ (2 * 2)

Proof state:
⊢ 2 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ √2 * √2 ^ 3 = √2 * (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹))

Tactic:
ring_nf

Result:
⊢ √2 ^ 4 = √2 * (√2)⁻¹ * 4

Proof state:
case h.e'_2

⊢ √2 ^ 4 = (√2 ^ 2) ^ 2

Tactic:
try simp only [← pow_mul]

Result:
case h.e'_2

⊢ √2 ^ 4 = √2 ^ (2 * 2)

Proof state:
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ √2 ^ 4 = √2 * (√2)⁻¹ * 4

Tactic:
rw [mul_inv_cancel₀ (ne_of_gt (Real.sqrt_pos.2 (show (2 : ℝ) > 0 by norm_num)))]

Result:
⊢ √2 ^ 4 = 1 * 4
-- Mathlib/NumberTheory/Ostrowski.lean
/-- The absolute value of `p` is `p ^ (-t)` for some positive real number `t`. -/
lemma exists_pos_eq_pow_neg : ∃ t : ℝ, 0 < t ∧ f p = p ^ (-t)

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
refine ⟨- logb p (f p), Left.neg_pos_iff.mpr <| logb_neg (mod_cast pprime.one_lt) hp0 hp1, ?_⟩

Result:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ f ↑p = ↑p ^ (- -logb (↑p) (f ↑p))

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ f ↑p = ↑p ^ (- -logb (↑p) (f ↑p))

Tactic:
rw [neg_neg]

Result:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ f ↑p = ↑p ^ logb (↑p) (f ↑p)

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
have pprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin

Result:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Proof state:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
pprime : Nat.Prime p
⊢ f ↑p = ↑p ^ logb (↑p) (f ↑p)

Tactic:
exact (rpow_logb (mod_cast pprime.pos) (mod_cast pprime.ne_one) hp0).symm

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_div_cancel (a b c : G) : a / b * (b / c) = a / c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / b * (b / c) = a / c

Tactic:
rw [← mul_div_assoc, div_mul_cancel]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_nonpos_iff : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
simp [division_def, mul_nonpos_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_loop_succ (as bs : Array α) (size start : Nat) (h : start < as.size) :
    extract.loop as (size+1) start bs = extract.loop as size (start+1) (bs.push as[start])

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
h : start < as.size
⊢ extract.loop as (size + 1) start bs = extract.loop as size (start + 1) (bs.push as[start])

Tactic:
rw [extract.loop, dif_pos h]

Result:
α : Type u_1
as bs : Array α
size start : Nat
h : start < as.size
⊢ (match size + 1 with
    | 0 => bs
    | i'.succ => extract.loop as i' (start + 1) (bs.push (as.get start h))) =
    extract.loop as size (start + 1) (bs.push as[start])

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
h : start < as.size
⊢ (match size + 1 with
    | 0 => bs
    | i'.succ => extract.loop as i' (start + 1) (bs.push (as.get start h))) =
    extract.loop as size (start + 1) (bs.push as[start])

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem sInf_adj_of_nonempty {s : Set G.Subgraph} (hs : s.Nonempty) :
    (sInf s).Adj a b ↔ ∀ G' ∈ s, Adj G' a b :=
  sInf_adj.trans <|
    and_iff_left_of_imp <| by
      obtain ⟨G', hG'⟩ := hs
      exact fun h => G'.adj_sub (h _ hG')

Proof state:
case intro
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
G' : G.Subgraph
hG' : G' ∈ s
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
exact fun h => G'.adj_sub (h _ hG')

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
hs : s.Nonempty
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b

Tactic:
obtain ⟨G', hG'⟩ := hs

Result:
case intro
V : Type u
G : SimpleGraph V
a b : V
s : Set G.Subgraph
G' : G.Subgraph
hG' : G' ∈ s
⊢ (∀ G' ∈ s, G'.Adj a b) → G.Adj a b
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem inv_prodComparison_map_snd [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map (snd _ _) = snd _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (snd A B) = snd (F.obj A) (F.obj B)

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals