harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_interpolate_le (hvs : Set.InjOn v s) :
    (interpolate s v r).degree ≤ ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ (C (r i) * Lagrange.basis s v i).degree ≤ ↑(#s - 1)

Tactic:
rw [degree_mul, degree_basis hvs hi]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
by_cases hr : r i = 0

Result:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Proof state:
case neg
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : ¬r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
rw [degree_C hr, zero_add]

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
hr : r i = 0
⊢ (C (r i)).degree + ↑(#s - 1) ≤ ↑(#s - 1)

Tactic:
simpa only [hr, map_zero, degree_zero, WithBot.bot_add] using bot_le

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ((interpolate s v) r).degree ≤ ↑(#s - 1)

Tactic:
refine (degree_sum_le _ _).trans ?_

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ (s.sup fun b => (C (r b) * Lagrange.basis s v b).degree) ≤ ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(#s - 1)

Tactic:
intro i hi

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
i : ι
hi : i ∈ s
⊢ (C (r i) * Lagrange.basis s v i).degree ≤ ↑(#s - 1)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ (s.sup fun b => (C (r b) * Lagrange.basis s v b).degree) ≤ ↑(#s - 1)

Tactic:
rw [Finset.sup_le_iff]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ∀ b ∈ s, (C (r b) * Lagrange.basis s v b).degree ≤ ↑(#s - 1)
-- Mathlib/Data/Set/Accumulate.lean
theorem biUnion_accumulate [Preorder α] (x : α) : ⋃ y ≤ x, Accumulate s y = ⋃ y ≤ x, s y

Proof state:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), s y

Tactic:
exact iUnion₂_subset fun y hy => monotone_accumulate hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y = ⋃ y, ⋃ (_ : y ≤ x), s y

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), s y

case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y

Proof state:
case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), Accumulate s y

Tactic:
exact iUnion₂_mono fun y _ => subset_accumulate

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem zero {f : ∀ b < (0 : Ordinal), Ordinal} : IsFundamentalSequence 0 0 f :=
  ⟨by rw [cof_zero, ord_zero], @fun i _ hi => (Ordinal.not_lt_zero i hi).elim, blsub_zero f⟩

Proof state:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord

Tactic:
rw [cof_zero, ord_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem iteratedFDerivWithin_eq_iteratedFDeriv {n : ℕ}
    (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 n f x) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Proof state:
case 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f univ x

Tactic:
rw [← iteratedFDerivWithin_inter_open u_open xu,
  ← iteratedFDerivWithin_inter_open u_open xu (s := univ)]

Result:
case 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
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f (univ ∩ u) x
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem cons_copy {u v w v' w'} (h : G.Adj u v) (p : G.Walk v' w') (hv : v' = v) (hw : w' = w) :
    Walk.cons h (p.copy hv hw) = (Walk.cons (hv ▸ h) p).copy rfl hw

Proof state:
V : Type u
G : SimpleGraph V
u v w v' w' : V
h : G.Adj u v
p : G.Walk v' w'
hv : v' = v
hw : w' = w
⊢ cons h (p.copy hv hw) = (cons ⋯ p).copy ⋯ hw

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u v' w' : V
p : G.Walk v' w'
h : G.Adj u v'
⊢ cons h (p.copy ⋯ ⋯) = (cons ⋯ p).copy ⋯ ⋯

Proof state:
V : Type u
G : SimpleGraph V
u v' w' : V
p : G.Walk v' w'
h : G.Adj u v'
⊢ cons h (p.copy ⋯ ⋯) = (cons ⋯ p).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insertIfNew_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
    m.insertIfNew a b = (Raw₀.insertIfNew ⟨m, h.size_buckets_pos⟩ a b).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ m.insertIfNew a b = (Raw₀.insertIfNew ⟨m, ⋯⟩ a b).val

Tactic:
simp [Raw.insertIfNew, h.size_buckets_pos]

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_eq_sum_C_mul_X_pow (n : ℕ) :
    wittPolynomial p R n = ∑ i ∈ range (n + 1), C ((p : R) ^ i) * X i ^ p ^ (n - i)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ wittPolynomial p R n = ∑ i ∈ range (n + 1), C (↑p ^ i) * X i ^ p ^ (n - i)

Tactic:
apply sum_congr rfl

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∀ x ∈ range (n + 1), (monomial (single x (p ^ (n - x)))) (↑p ^ x) = C (↑p ^ x) * X x ^ p ^ (n - x)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1

Tactic:
rw [pow_zero]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ (monomial (single i (p ^ (n - i)))) (↑p ^ i) = C (↑p ^ i) * X i ^ p ^ (n - i)

Tactic:
rw [monomial_eq, Finsupp.prod_single_index]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ X i ^ 0 = 1

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ ∀ x ∈ range (n + 1), (monomial (single x (p ^ (n - x)))) (↑p ^ x) = C (↑p ^ x) * X x ^ p ^ (n - x)

Tactic:
rintro i -

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
n i : ℕ
⊢ (monomial (single i (p ^ (n - i)))) (↑p ^ i) = C (↑p ^ i) * X i ^ p ^ (n - i)
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma CotangentSpace.map_sub_map (f g : Hom P P') :
    CotangentSpace.map f - CotangentSpace.map g =
      P'.cotangentComplex.restrictScalars S ∘ₗ (f.sub g)

Proof state:
case h
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : P.CotangentSpace
⊢ (CotangentSpace.map f - CotangentSpace.map g) x = (↑S P'.cotangentComplex ∘ₗ f.sub g) x

Tactic:
induction x using TensorProduct.induction_on with
| zero =>
  simp only [map_zero, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply]
| add =>
  simp only [map_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]
| tmul x y =>
  obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y
  induction y with
  | zero => simp only [map_zero, tmul_zero, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply]
  | add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply, *]
  | tmul =>
    simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply,
      map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
      Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Result:
no goals

Proof state:
case h.add
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x✝ y✝ : S ⊗[P.Ring] Ω[P.Ring⁄R]
a✝¹ : (CotangentSpace.map f - CotangentSpace.map g) x✝ = (↑S P'.cotangentComplex ∘ₗ f.sub g) x✝
a✝ : (CotangentSpace.map f - CotangentSpace.map g) y✝ = (↑S P'.cotangentComplex ∘ₗ f.sub g) y✝
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x✝ + y✝) = (↑S P'.cotangentComplex ∘ₗ f.sub g) (x✝ + y✝)

Tactic:
simp only [map_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem iUnion_nat_of_monotone_of_tsum_ne_top (m : OuterMeasure α) {s : ℕ → Set α}
    (h_mono : ∀ n, s n ⊆ s (n + 1)) (h0 : (∑' k, m (s (k + 1) \ s k)) ≠ ∞) :
    m (⋃ n, s n) = ⨆ n, m (s n)

Proof state:
case mk.intro.inr
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)

Tactic:
refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)

Result:
case mk.intro.inr.refine_1
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ x ∈ s (j - (n + 1) + n + 1)

case mk.intro.inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n < j
-- Mathlib/Data/Nat/Init.lean
lemma two_mul_odd_div_two (hn : n % 2 = 1) : 2 * (n / 2) = n - 1

Proof state:
n : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1

Tactic:
conv => rhs; rw [← Nat.mod_add_div n 2, hn, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey? k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany empty l).val.getKey? k' = some k

Tactic:
rw [getKey?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem mono {m m' : MeasurableSpace α} [TopologicalSpace β]
    (hf : StronglyMeasurable[m'] f) (h_mono : m' ≤ m) : StronglyMeasurable[m] f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
⊢ StronglyMeasurable f

Tactic:
let f_approx : ℕ → @SimpleFunc α m β := fun n =>
  @SimpleFunc.mk α m β
    (hf.approx n)
    (fun x => h_mono _ (SimpleFunc.measurableSet_fiber' _ x))
    (SimpleFunc.finite_range (hf.approx n))

Result:
α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β := fun n => { toFun := ⇑(hf.approx n), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β := fun n => { toFun := ⇑(hf.approx n), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨f_approx, hf.tendsto_approx⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩

Proof state:
a : Nat
⊢ 0 = a * 0

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
@[simp]
lemma δ_zero_mkOfSucc {n : ℕ} (i : Fin n) :
    δ 0 ≫ mkOfSucc i = SimplexCategory.const _ ⦋n⦌ i.succ

Proof state:
n : ℕ
i : Fin n
⊢ δ 0 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.succ

Tactic:
ext x

Result:
case a.h.h.h
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) x)

Proof state:
case a.h.h.h
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) x) = ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) x)

Tactic:
fin_cases x

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) ((fun i => i) ⟨0, ⋯⟩))

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ)) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem orderedInsert_eq_take_drop (a : α) :
    ∀ l : List α,
      l.orderedInsert r a = (l.takeWhile fun b => ¬a ≼ b) ++ a :: l.dropWhile fun b => ¬a ≼ b
  | [] => rfl
  | b :: l => by
    dsimp only [orderedInsert]
    split_ifs with h <;> simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)

Tactic:
dsimp only [orderedInsert]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ (if r a b then a :: b :: l else b :: orderedInsert r a l) =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ (if r a b then a :: b :: l else b :: orderedInsert r a l) =
    takeWhile (fun b => decide ¬r a b) (b :: l) ++ a :: dropWhile (fun b => decide ¬r a b) (b :: l)

Tactic:
split_ifs with h <;> simp [takeWhile, dropWhile, *, orderedInsert_eq_take_drop a l]

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma dirSupClosed_of_isClosed [IsScottHausdorff α univ] (h : IsClosed s) : DirSupClosed s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α univ
h : IsClosed s
⊢ DirSupClosed s

Tactic:
apply DirSupInacc.of_compl

Result:
case a
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α univ
h : IsClosed s
⊢ DirSupInacc sᶜ

Proof state:
case a
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α univ
h : IsClosed s
⊢ DirSupInaccOn univ sᶜ

Tactic:
exact (dirSupInaccOn_of_isOpen h.isOpen_compl)

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α univ
h : IsClosed s
⊢ DirSupInacc sᶜ

Tactic:
rw [← dirSupInaccOn_univ]

Result:
case a
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α univ
h : IsClosed s
⊢ DirSupInaccOn univ sᶜ
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem inv_left_mul_aux (hA : A ∈ symplecticGroup l R) : -(J l R * Aᵀ * J l R * A) = 1 :=
  calc
    -(J l R * Aᵀ * J l R * A) = (-J l R) * (Aᵀ * J l R * A)

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * J l R = -1 • (J l R * J l R)

Tactic:
simp only [Matrix.neg_mul, neg_smul, one_smul]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • -1 = 1

Tactic:
simp only [neg_smul_neg, one_smul]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • (J l R * J l R) = -1 • -1

Tactic:
rw [J_squared]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [mem_iff'] at hA

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [hA]

Result:
no goals

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)

Tactic:
simp only [Matrix.mul_assoc, Matrix.neg_mul]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_leftMoves (o : Ordinal) : o.toPGame.LeftMoves = o.toType

Proof state:
o : Ordinal.{u_1}
⊢ o.toPGame.LeftMoves = o.toType

Tactic:
rw [toPGame, LeftMoves]

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem tendsto_sum_mul_atTop_nhds_one_sub_integral
    (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t)
    (hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0)) {l : 𝕜}
    (h_lim : Tendsto (fun n : ℕ ↦ f n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l))
    {g : ℝ → 𝕜} (hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g)
    (hg_int : IntegrableAtFilter g atTop) :
    Tendsto (fun n : ℕ ↦ ∑ k ∈ Icc 0 n, f k * c k) atTop
      (𝓝 (l - ∫ t in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
⊢ IntegrableOn (fun x => deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) (Set.Ioi 0) volume

Tactic:
exact integrableOn_Ici_iff_integrableOn_Ioi.mp
  <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
    hg_dom hg_int

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun n => f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : (fun t => deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
x✝ : ℕ
⊢ ?m.88418 x✝ = ∫ (t : ℝ) in Set.Ioc 0 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [← integral_of_le (Nat.cast_nonneg _)]

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
@[simp] lemma Definable.himp {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.Definable L t) :
    A.Definable L (s ⇨ t)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)

Tactic:
exact ht.union hs.compl

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (s ⇨ t)

Tactic:
rw [himp_eq]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)
-- Mathlib/GroupTheory/Perm/List.lean
theorem support_formPerm_le [Fintype α] : support (formPerm l) ≤ l.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
simpa using hx

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l.toFinset

Tactic:
simpa using support_formPerm_le' _ hx'

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
⊢ l.formPerm.support ≤ l.toFinset

Tactic:
intro x hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset

Tactic:
have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx

Result:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l.toFinset