harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem addHaar_image_le_lintegral_abs_det_fderiv_aux1 (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) {ε : ℝ≥0} (εpos : 0 < ε) :
    μ (f '' s) ≤ (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ ENNReal.ofReal |(A n).det| + ↑ε ≤ ENNReal.ofReal |(f' x).det| + 2 * ↑ε

Tactic:
have I : |(A n).det| ≤ |(f' x).det| + ε :=
  calc
    |(A n).det| = |(f' x).det - ((f' x).det - (A n).det)| := by congr 1; abel
    _ ≤ |(f' x).det| + |(f' x).det - (A n).det| := abs_sub _ _
    _ ≤ |(f' x).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
I : |(A n).det| ≤ |(f' x).det| + ↑ε
⊢ ENNReal.ofReal |(A n).det| + ↑ε ≤ ENNReal.ofReal |(f' x).det| + 2 * ↑ε
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`). -/
lemma hasSum_int_completedSinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ Gammaℝ (s + 1) * (-I) * Int.sign n *
    cexp (2 * π * I * a * n) / (↑|n| : ℂ) ^ s / 2) (completedSinZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
let c (n : ℤ) : ℂ := -I * cexp (2 * π * I * a * n) / 2

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i => 1 / |↑i| ^ s.re / 2

Tactic:
apply Summable.div_const

Result:
case h
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i => 1 / |↑i| ^ s.re
-- Mathlib/Data/Multiset/Count.lean
theorem countP_congr {s s' : Multiset α} (hs : s = s')
    {p p' : α → Prop} [DecidablePred p] [DecidablePred p']
    (hp : ∀ x ∈ s, p x = p' x) : s.countP p = s'.countP p'

Proof state:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ x ∈ s, p x = p' x) → countP p s = countP p' s'

Tactic:
exact Quot.induction_on₂ s s'
  (fun l l' hs hp => by
    simp only [quot_mk_to_coe'', coe_eq_coe] at hs
    apply hs.countP_congr
    simpa using hp)

Result:
no goals

Proof state:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ x ∈ Quot.mk (⇑(isSetoid α)) l, p x = p' x
hs : l ~ l'
⊢ ∀ x ∈ l, decide (p x) = decide (p' x)

Tactic:
simpa using hp

Result:
no goals

Proof state:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ x ∈ Quot.mk (⇑(isSetoid α)) l, p x = p' x
hs : l ~ l'
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')

Tactic:
apply hs.countP_congr

Result:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ x ∈ Quot.mk (⇑(isSetoid α)) l, p x = p' x
hs : l ~ l'
⊢ ∀ x ∈ l, decide (p x) = decide (p' x)

Proof state:
α : Type u_1
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
hp : ∀ x ∈ s, p x = p' x
⊢ countP p s = countP p' s'

Tactic:
revert hs hp

Result:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
⊢ s = s' → (∀ x ∈ s, p x = p' x) → countP p s = countP p' s'

Proof state:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hs : Quot.mk (⇑(isSetoid α)) l = Quot.mk (⇑(isSetoid α)) l'
hp : ∀ x ∈ Quot.mk (⇑(isSetoid α)) l, p x = p' x
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')

Tactic:
simp only [quot_mk_to_coe'', coe_eq_coe] at hs

Result:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ x ∈ Quot.mk (⇑(isSetoid α)) l, p x = p' x
hs : l ~ l'
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')
-- Mathlib/Data/Finset/Basic.lean
theorem filter_union (s₁ s₂ : Finset α) : (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
  ext fun _ => by simp only [mem_filter, mem_union, or_and_right]

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ filter p (s₁ ∪ s₂) ↔ x✝ ∈ filter p s₁ ∪ filter p s₂

Tactic:
simp only [mem_filter, mem_union, or_and_right]

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem orthocenter_eq_smul_vsub_vadd_circumcenter (t : Triangle ℝ P) :
    t.orthocenter =
      (3 : ℝ) • ((univ : Finset (Fin 3)).centroid ℝ t.points -ᵥ t.circumcenter : V) +ᵥ
        t.circumcenter

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
⊢ (↑(2 + 1) / ↑(2 - 1)) • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t =
    3 • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
norm_num

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
⊢ t.orthocenter = 3 • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
⊢ (↑(2 + 1) / ↑(2 - 1)) • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t =
    3 • (centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
-- Mathlib/Order/Bounds/Basic.lean
theorem IsGreatest.insert [LinearOrder γ] (a) {b} {s : Set γ} (hs : IsGreatest s b) :
    IsGreatest (insert a s) (max a b)

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest (insert a s) (a ⊔ b)

Tactic:
rw [insert_eq]

Result:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (a ⊔ b)

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (a ⊔ b)

Tactic:
exact isGreatest_singleton.union hs

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_apply {u : Perm (Function.fixedPoints g)}
    {v : (c : g.cycleFactorsFinset) → Subgroup.zpowers c.val} {x : α} :
    kerParam g (u,v) x =
    if hx : g.cycleOf x ∈ g.cycleFactorsFinset
    then (v ⟨g.cycleOf x, hx⟩ : Perm α) x
    else ofSubtype u x

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((kerParam g) (u, v)) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply', mul_apply, ofSubtype_apply_of_not_mem u hx',
  noncommPiCoprod_apply, ← Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩),
  mul_apply, ← not_mem_support]

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i => ↑((u, v).2 i)) ⋯).support
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).getKey? k' =
      if k == k' then
        if k ∈ m then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

Tactic:
simp_to_raw using Raw₀.Const.getKey?_modify

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
    (merge le s₁ s₂).WF le n ∧ ((s₁.rankGT n ↔ s₂.rankGT n) → (merge le s₁ s₂).rankGT n)

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
s₁ s₂ : Heap α✝
n : Nat
h₁ : WF le n s₁
h₂ : WF le n s₂
⊢ WF le n (merge le s₁ s₂) ∧ ((s₁.rankGT n ↔ s₂.rankGT n) → (merge le s₁ s₂).rankGT n)

Tactic:
unfold merge

Result:
α✝ : Type u_1
le : α✝ → α✝ → Bool
s₁ s₂ : Heap α✝
n : Nat
h₁ : WF le n s₁
h₂ : WF le n s₂
⊢ WF le n
      (match s₁, s₂ with
      | Heap.nil, h => h
      | h, Heap.nil => h
      | s₁@h:(cons r₁ a₁ n₁ t₁), s₂@h_1:(cons r₂ a₂ n₂ t₂) =>
        if r₁ < r₂ then cons r₁ a₁ n₁ (merge le t₁ s₂)
        else
          if r₂ < r₁ then cons r₂ a₂ n₂ (merge le s₁ t₂)
          else
            match combine le a₁ a₂ n₁ n₂ with
            | (a, n) =>
              let r := r₁ + 1;
              if t₁.rankGT r then if t₂.rankGT r then cons r a n (merge le t₁ t₂) else merge le (cons r a n t₁) t₂
              else if t₂.rankGT r then merge le t₁ (cons r a n t₂) else cons r a n (merge le t₁ t₂)) ∧
    ((s₁.rankGT n ↔ s₂.rankGT n) →
      (match s₁, s₂ with
          | Heap.nil, h => h
          | h, Heap.nil => h
          | s₁@h:(cons r₁ a₁ n₁ t₁), s₂@h_1:(cons r₂ a₂ n₂ t₂) =>
            if r₁ < r₂ then cons r₁ a₁ n₁ (merge le t₁ s₂)
            else
              if r₂ < r₁ then cons r₂ a₂ n₂ (merge le s₁ t₂)
              else
                match combine le a₁ a₂ n₁ n₂ with
                | (a, n) =>
                  let r := r₁ + 1;
                  if t₁.rankGT r then if t₂.rankGT r then cons r a n (merge le t₁ t₂) else merge le (cons r a n t₁) t₂
                  else if t₂.rankGT r then merge le t₁ (cons r a n t₂) else cons r a n (merge le t₁ t₂)).rankGT
        n)

Proof state:
α✝ : Type u_1
le : α✝ → α✝ → Bool
n✝ : Nat
x✝² x✝¹ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
h₁ : WF le n✝ (cons r₁ a₁ n₁ t₁)
hr₁ : n✝ ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) t₁
h₂ : WF le n✝ (cons r₁ a₂ n₂ t₂)
hr₂ : n✝ ≤ r₁
hn₂ : HeapNode.WF le a₂ n₂ r₁
ht₂ : WF le (r₁ + 1) t₂
lt₁ lt₂ : ¬r₁ < r₁
x✝ : α✝ × HeapNode α✝
a : α✝
n : HeapNode α✝
eq : combine le a₁ a₂ n₁ n₂ = (a, n)
⊢ HeapNode.WF le a n (r₁ + 1)

Tactic:
unfold combine at eq

Result:
α✝ : Type u_1
le : α✝ → α✝ → Bool
n✝ : Nat
x✝² x✝¹ : Heap α✝
r₁ : Nat
a₁ : α✝
n₁ : HeapNode α✝
t₁ : Heap α✝
a₂ : α✝
n₂ : HeapNode α✝
t₂ : Heap α✝
h₁ : WF le n✝ (cons r₁ a₁ n₁ t₁)
hr₁ : n✝ ≤ r₁
hn₁ : HeapNode.WF le a₁ n₁ r₁
ht₁ : WF le (r₁ + 1) t₁
h₂ : WF le n✝ (cons r₁ a₂ n₂ t₂)
hr₂ : n✝ ≤ r₁
hn₂ : HeapNode.WF le a₂ n₂ r₁
ht₂ : WF le (r₁ + 1) t₂
lt₁ lt₂ : ¬r₁ < r₁
x✝ : α✝ × HeapNode α✝
a : α✝
n : HeapNode α✝
eq : (if le a₁ a₂ = true then (a₁, HeapNode.node a₂ n₂ n₁) else (a₂, HeapNode.node a₁ n₁ n₂)) = (a, n)
⊢ HeapNode.WF le a n (r₁ + 1)
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem AnalyticOn.iteratedFDeriv_comp_perm
    (h : AnalyticOn 𝕜 f univ) {n : ℕ} (v : Fin n → E) (σ : Perm (Fin n)) :
    iteratedFDeriv 𝕜 n f x (v ∘ σ) = iteratedFDeriv 𝕜 n f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDerivWithin 𝕜 n f univ x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f univ x) v

Tactic:
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xy_succ_succ (n) :
    xn a1 (n + 2) + xn a1 n =
      2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
this : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
unfold pellZd at this

Result:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    ↑(2 * a) * { re := ↑(xn a1 (n + 1)), im := ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
have := pellZd_succ_succ a1 n

Result:
a : ℕ
a1 : 1 < a
n : ℕ
this : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
injection this with h₁ h₂

Result:
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    ↑(2 * a) * { re := ↑(xn a1 (n + 1)), im := ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
erw [Zsqrtd.smul_val (2 * a : ℕ)] at this

Result:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
constructor <;> apply Int.ofNat.inj <;> [simpa using h₁; simpa using h₂]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma hasLift : sq.HasLift

Proof state:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j => (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
⊢ sq.HasLift

Tactic:
have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j

Result:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j => (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ sq.HasLift

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
sq : CommSq f (c.ι.app ⊥) p g✝
s : ↑(sqFunctor c p f g✝).sections
hs : (↑s (Opposite.op ⊥)).f' = f
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ (fun j => (↑s (Opposite.op j)).f') j' =
    (fun j => (↑s (Opposite.op j)).f') j ≫ ((Functor.const J).obj X).map g

Tactic:
simpa using congr_arg SqStruct.f' (s.2 g.op)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem zipWithLeft'_eq_zipWithLeft'TR : @zipWithLeft' = @zipWithLeft'TR

Proof state:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR f as bs

Tactic:
simp [zipWithLeft'TR]

Result:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]

Proof state:
⊢ @zipWithLeft' = @zipWithLeft'TR

Tactic:
funext α β γ f as bs

Result:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR f as bs

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs✝ : List β
acc : Array γ
bs : List β
⊢ zipWithLeft'TR.go f [] bs acc =
    match zipWithLeft' f [] bs with
    | (l, r) => (acc.toList ++ l, r)

Tactic:
simp [zipWithLeft'TR.go]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as✝ : List α
bs✝ : List β
acc : Array γ
a : α
as : List α
b : β
bs : List β
⊢ zipWithLeft'TR.go f (a :: as) (b :: bs) acc =
    match zipWithLeft' f (a :: as) (b :: bs) with
    | (l, r) => (acc.toList ++ l, r)

Tactic:
simp [zipWithLeft'TR.go, go _ as bs]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
acc : Array γ
head✝ : α
tail✝ : List α
⊢ zipWithLeft'TR.go f (head✝ :: tail✝) [] acc =
    match zipWithLeft' f (head✝ :: tail✝) [] with
    | (l, r) => (acc.toList ++ l, r)

Tactic:
simp [zipWithLeft'TR.go, Array.foldl_toList_eq_map]

Result:
no goals

Proof state:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft' f as bs = zipWithLeft'TR.go f as bs #[]

Tactic:
simp [zipWithLeft'TR, go]

Result:
no goals