harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
/-- Formula for `hurwitzZeta s` as a Dirichlet series in the convergence range. We
restrict to `a ∈ Icc 0 1` to simplify the statement. -/
lemma hasSum_hurwitzZeta_of_one_lt_re {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ 1 / (n + a : ℂ) ^ s) (hurwitzZeta a s)

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ y✝ : ℂ
⊢ x✝ = (x✝ + y✝) / 2 + (x✝ - y✝) / 2

Tactic:
ring

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => 1 / (↑n + ↑a) ^ s) (hurwitzZeta (↑a) s)

Tactic:
convert (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add
    (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs) using 1

Result:
case h.e'_5
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ (fun n => 1 / (↑n + ↑a) ^ s) = fun b =>
    (1 / (↑b + ↑a) ^ s + 1 / (↑b + 1 - ↑a) ^ s) / 2 + (1 / (↑b + ↑a) ^ s - 1 / (↑b + 1 - ↑a) ^ s) / 2

Proof state:
case h.e'_5.h
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 + (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2

Tactic:
apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring

Result:
no goals

Proof state:
case h.e'_5
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ (fun n => 1 / (↑n + ↑a) ^ s) = fun b =>
    (1 / (↑b + ↑a) ^ s + 1 / (↑b + 1 - ↑a) ^ s) / 2 + (1 / (↑b + ↑a) ^ s - 1 / (↑b + 1 - ↑a) ^ s) / 2

Tactic:
ext1 n

Result:
case h.e'_5.h
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 + (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2

Tactic:
intros

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ y✝ : ℂ
⊢ x✝ = (x✝ + y✝) / 2 + (x✝ - y✝) / 2
-- Mathlib/Data/List/Infix.lean
theorem tails_reverse (l : List α) : tails (reverse l) = reverse (map reverse l.inits)

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse

Tactic:
simp [reverse_involutive.comp_self, ← map_reverse]

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse l.inits).reverse

Tactic:
rw [inits_eq_tails l]

Result:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_neg (a b : α) : toIcoMod hp a (-b) = p - toIocMod hp (-a) b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIocDiv hp (-a) b • p + 1 • p) = p - (b - toIocDiv hp (-a) b • p)

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (-b) = p - toIocMod hp (-a) b

Tactic:
simp_rw [toIcoMod, toIocMod, toIcoDiv_neg, neg_smul, add_smul]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIocDiv hp (-a) b • p + 1 • p) = p - (b - toIocDiv hp (-a) b • p)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂) ↔
    ∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂) →
    ∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l

case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l) →
    ∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ t l₁_1 l₂_1, l₂ ++ l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = filterMap f l₁

Tactic:
exact ⟨_, l₂, l₁, rfl, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ l₂ <:+ filterMap f l₁ ↔ ∃ l, l <:+ l₁ ∧ l₂ = filterMap f l

Tactic:
simp only [IsSuffix, append_eq_filterMap_iff]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂) ↔
    ∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l) →
    ∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂

Tactic:
rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ t l₁_1 l₂_1, l₂ ++ l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = filterMap f l₁

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l, (∃ t, t ++ l = l₁ ++ l₂) ∧ filterMap f l₂ = filterMap f l

Tactic:
exact ⟨l₂, ⟨l₁, rfl⟩, rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = t ∧ filterMap f l₂_1 = l₂) →
    ∃ l, (∃ t, t ++ l = l₁) ∧ l₂ = filterMap f l

Tactic:
rintro ⟨_, l₁, l₂, rfl, rfl, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l, (∃ t, t ++ l = l₁ ++ l₂) ∧ filterMap f l₂ = filterMap f l
-- Mathlib/Order/Filter/Bases.lean
theorem disjoint_pure_pure {x y : α} : Disjoint (pure x : Filter α) (pure y) ↔ x ≠ y

Proof state:
α : Type u_1
x y : α
⊢ Disjoint (pure x) (pure y) ↔ x ≠ y

Tactic:
simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Basic.lean
theorem mem_restrictTotalDegree (p : MvPolynomial σ R) :
    p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m

Proof state:
σ : Type u
R : Type v
inst✝ : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m

Tactic:
rw [totalDegree, Finset.sup_le_iff]

Result:
σ : Type u
R : Type v
inst✝ : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ b ∈ p.support, (b.sum fun x e => e) ≤ m

Proof state:
σ : Type u
R : Type v
inst✝ : CommSemiring R
m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ b ∈ p.support, (b.sum fun x e => e) ≤ m

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_nhdsLE (h : Tendsto f l (𝓝[≤] x)) :
    Tendsto (arcsin <| f ·) l (𝓝[≤] (arcsin x))

Proof state:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
y : ℝ
hy : y ∈ Iic x
⊢ arcsin y ∈ Iic (arcsin x)

Tactic:
exact monotone_arcsin hy

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
⊢ Tendsto (fun x => arcsin (f x)) l (𝓝[≤] arcsin x)

Tactic:
refine ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h

Result:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
y : ℝ
hy : y ∈ Iic x
⊢ arcsin y ∈ Iic (arcsin x)
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma id_prod_eq : @Kernel.id (α × β) inferInstance =
    (deterministic Prod.fst measurable_fst) ×ₖ (deterministic Prod.snd measurable_snd)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Kernel.id = deterministic (fun a => (a.1, a.2)) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Kernel.id = deterministic Prod.fst ⋯ ×ₖ deterministic Prod.snd ⋯

Tactic:
rw [deterministic_prod_deterministic]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Kernel.id = deterministic (fun a => (a.1, a.2)) ⋯
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.pow {f : α → R} {g : α → 𝕜} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) :
    (fun x => f x ^ n) =o[l] fun x => g x ^ n

Proof state:
case intro.succ
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
ihn : (fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ
⊢ (fun x => f x ^ (n + 1).succ) =o[l] fun x => g x ^ (n + 1).succ

Tactic:
convert ihn.mul h <;> simp [pow_succ]

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
hn : 0 < n
⊢ (fun x => f x ^ n) =o[l] fun x => g x ^ n

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'

Result:
case intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
hn : 0 < n.succ
⊢ (fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ

Proof state:
case intro.zero
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
⊢ (fun x => f x ^ Nat.succ 0) =o[l] fun x => g x ^ Nat.succ 0

Tactic:
simpa only [pow_one]

Result:
no goals

Proof state:
case intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
⊢ (fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ

Tactic:
induction n with
| zero => simpa only [pow_one]
| succ n ihn => convert ihn.mul h <;> simp [pow_succ]

Result:
no goals

Proof state:
case intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
hn : 0 < n.succ
⊢ (fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ

Tactic:
clear hn

Result:
case intro
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f : α → R
g : α → 𝕜
h : f =o[l] g
n : ℕ
⊢ (fun x => f x ^ n.succ) =o[l] fun x => g x ^ n.succ
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_subset_Ico_self : Ioo a b ⊆ Ico a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ico]

Result:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b

Tactic:
exact Set.Ioo_subset_Ico_self

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma iInf_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) :
    (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon

Proof state:
case h.e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i => I i) = Set.range fun i => (I i).ringCon

Tactic:
ext

Result:
case h.e'_3.h
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i => I i) ↔ x✝ ∈ Set.range fun i => (I i).ringCon

Proof state:
case h.e'_3.h
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i => I i) ↔ x✝ ∈ Set.range fun i => (I i).ringCon

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon

Tactic:
simp only [iInf, sInf_ringCon]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sInf (ringCon '' Set.range fun i => I i) = sInf (Set.range fun i => (I i).ringCon)

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sInf (ringCon '' Set.range fun i => I i) = sInf (Set.range fun i => (I i).ringCon)

Tactic:
congr!

Result:
case h.e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i => I i) = Set.range fun i => (I i).ringCon
-- Mathlib/Order/Disjoint.lean
lemma Disjoint.eq_iff (hab : Disjoint a b) : a = b ↔ a = ⊥ ∧ b = ⊥

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a = b ↔ a = ⊥ ∧ b = ⊥

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_inter' (hs : s.Finite) :
    uniformOn s (t ∩ u) = uniformOn (s ∩ u) t * uniformOn s u

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ u)) t * (uniformOn s) u

Tactic:
rw [← Set.inter_comm]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (u ∩ t) = (uniformOn (s ∩ u)) t * (uniformOn s) u

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (u ∩ t) = (uniformOn (s ∩ u)) t * (uniformOn s) u

Tactic:
exact uniformOn_inter hs

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B] [Algebra R A]
    [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) :
    spectrum R (f a) = spectrum R a :=
  Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
    simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
      AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)

Proof state:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)

Tactic:
simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
  AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_triangle8 (a b c d e f g h : α) : dist a h ≤ dist a b + dist b c + dist c d
    + dist d e + dist e f + dist f g + dist g h

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d ≤ dist a b + dist b c + dist c d

Tactic:
exact dist_triangle4 a b c d

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
apply le_trans (dist_triangle4 a f g h)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f + dist f g + dist g h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f + dist f g + dist g h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
apply add_le_add_right (add_le_add_right _ (dist f g)) (dist g h)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Tactic:
apply add_le_add_right (add_le_add_right _ (dist d e)) (dist e f)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d ≤ dist a b + dist b c + dist c d

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Tactic:
apply le_trans (dist_triangle4 a d e f)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
-- Mathlib/Data/Fintype/Pi.lean
lemma piFinset_filter_const [DecidableEq ι] [Fintype ι] :
    {f ∈ Fintype.piFinset fun _ : ι ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ filter (fun f => ∃ a ∈ s, const ι a = f) (Fintype.piFinset fun x => s) = s.piDiag ι

Tactic:
aesop

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
lemma not_isCyclic (h1 : n ≠ 1) : ¬ IsCyclic (DihedralGroup n) := fun h => by
  by_cases h2 : n = 2
  · simpa [exponent, card, h2] using h.exponent_eq_card
  · exact not_commutative h1 h2 h.commutative

Proof state:
case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

Tactic:
simpa [exponent, card, h2] using h.exponent_eq_card

Result:
no goals

Proof state:
case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
exact not_commutative h1 h2 h.commutative

Result:
no goals

Proof state:
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
⊢ False

Tactic:
by_cases h2 : n = 2

Result:
case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False
-- Mathlib/Order/Interval/Finset/Box.lean
lemma box_succ_disjUnion (n : ℕ) :
    (box (n + 1)).disjUnion (Icc (-n : α) n) (disjoint_box_succ_prod _) =
      Icc (-n.succ : α) n.succ

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ (box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ

Tactic:
rw [disjUnion_eq_union, box_succ_union_prod]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq {f : α → β} (hf : IsOpenEmbedding f)
    (s : Set β) (x : α) : map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x

Tactic:
apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f

Tactic:
rw [inter_assoc, inter_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Tactic:
rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem sum_map_count_dedup_eq_length (l : List α) :
    (l.dedup.map fun x => l.count x).sum = l.length

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x => count x l) l.dedup).sum = l.length

Tactic:
simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem sum_neg (xs : IntList) : (-xs).sum = -(xs.sum)

Proof state:
case nil

⊢ (-[]).sum = -sum []

Tactic:
simp

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : (-xs).sum = -sum xs
⊢ (-(x :: xs)).sum = -sum (x :: xs)

Tactic:
simp_all [Int.neg_add]

Result:
no goals

Proof state:
xs : IntList
⊢ (-xs).sum = -xs.sum

Tactic:
induction xs with
| nil => simp
| cons x xs ih => simp_all [Int.neg_add]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma neg_dotProduct_neg : -v ⬝ᵥ -w = v ⬝ᵥ w

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ -w = v ⬝ᵥ w

Tactic:
rw [neg_dotProduct, dotProduct_neg, neg_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.isClopenable [PolishSpace α] [MeasurableSpace α] [BorelSpace α]
    {s : Set α} (hs : MeasurableSet s) : IsClopenable s

Proof state:
case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
exact fun f _ _ hf => IsClopenable.iUnion hf

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ {s : Set α}, MeasurableSet s → IsClopenable s

Tactic:
apply MeasurableSet.induction_on_open

Result:
case isOpen
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (U : Set α), IsOpen U → IsClopenable U

case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
⊢ IsClopenable s

Tactic:
revert s

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ {s : Set α}, MeasurableSet s → IsClopenable s

Proof state:
case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

Tactic:
exact fun u _ h'u => h'u.compl

Result:
no goals

Proof state:
case isOpen
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (U : Set α), IsOpen U → IsClopenable U

Tactic:
exact fun u hu => hu.isClopenable

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `castSucc` commutes with `succAbove`. -/
@[simp]
lemma castSucc_succAbove_castSucc {n : ℕ} {i : Fin (n + 1)} {j : Fin n} :
    i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Proof state:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rcases i.le_or_lt (castSucc j) with (h | h)

Result:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Proof state:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]

Result:
no goals