harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_sumInl (φ : L.BoundedFormula α n) :
    (φ.relabel Sum.inl : L.BoundedFormula α (0 + n)) = φ.castLE (ge_of_eq (zero_add n))

Proof state:
case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) f₁✝ = castLE ⋯ f₁✝
ih2 :
  mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) f₂✝ = castLE ⋯ f₂✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) (f₁✝.imp f₂✝) =
    castLE ⋯ (f₁✝.imp f₂✝)

Tactic:
simp_all [mapTermRel]

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) φ = castLE ⋯ φ

Tactic:
induction φ with
| falsum => rfl
| equal => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]
| rel => simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]; rfl
| imp _ _ ih1 ih2 => simp_all [mapTermRel]
| all _ ih3 => simp_all [mapTermRel]

Result:
no goals

Proof state:
case falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) falsum =
    castLE ⋯ falsum

Tactic:
rfl

Result:
no goals

Proof state:
case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) f✝ = castLE ⋯ f✝
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) f✝.all =
    castLE ⋯ f✝.all

Tactic:
simp_all [mapTermRel]

Result:
no goals

Proof state:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (fun i => Term.relabel (Sum.map id (Fin.cast ⋯)) (ts✝ i)) = Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts✝

Tactic:
rfl

Result:
no goals

Proof state:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) (rel R✝ ts✝) =
    castLE ⋯ (rel R✝ ts✝)

Tactic:
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]

Result:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (fun i => Term.relabel (Sum.map id (Fin.cast ⋯)) (ts✝ i)) = Term.relabel (Sum.map id (Fin.cast ⋯)) ∘ ts✝

Proof state:
case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) (equal t₁✝ t₂✝) =
    castLE ⋯ (equal t₁✝ t₂✝)

Tactic:
simp [Fin.natAdd_zero, castLE_of_eq, mapTermRel]

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ relabel Sum.inl φ = castLE ⋯ φ

Tactic:
simp only [relabel, relabelAux_sumInl]

Result:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) φ = castLE ⋯ φ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_eq_append_iff {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l}
    (w : k + l = n + m) :
    a ++ b = (c ++ d).cast w ↔
      if h : n ≤ k then
        ∃ a' : Vector α (k - n), c = (a ++ a').cast (by omega) ∧ b = (a' ++ d).cast (by omega)
      else
        ∃ c' : Vector α (n - k), a = (c ++ c').cast (by omega) ∧ d = (c' ++ b).cast (by omega)

Proof state:
case mk.mk.mk.mk.mpr.isTrue.intro.intro
α : Type u_1
a c d : Array α
h : a.size ≤ c.size
a' : Vector α (c.size - a.size)
hc : c = ({ toArray := a, size_toArray := ⋯ } ++ a').toArray
w : c.size + d.size = a.size + (a' ++ { toArray := d, size_toArray := ⋯ }).size
⊢ (∃ a'_1, c = a ++ a'_1 ∧ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray = a'_1 ++ d) ∨
    ∃ c', a = c ++ c' ∧ d = c' ++ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray

Tactic:
left

Result:
case mk.mk.mk.mk.mpr.isTrue.intro.intro.h
α : Type u_1
a c d : Array α
h : a.size ≤ c.size
a' : Vector α (c.size - a.size)
hc : c = ({ toArray := a, size_toArray := ⋯ } ++ a').toArray
w : c.size + d.size = a.size + (a' ++ { toArray := d, size_toArray := ⋯ }).size
⊢ ∃ a'_1, c = a ++ a'_1 ∧ (a' ++ { toArray := d, size_toArray := ⋯ }).toArray = a'_1 ++ d
-- Mathlib/Topology/Compactness/Compact.lean
theorem CompactSpace.elim_nhds_subcover [CompactSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Finset X, ⋃ x ∈ t, U x = ⊤

Proof state:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Finset X
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ∃ t, ⋃ x ∈ t, U x = ⊤

Tactic:
exact ⟨t, top_unique s⟩

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ t, ⋃ x ∈ t, U x = ⊤

Tactic:
obtain ⟨t, -, s⟩ := IsCompact.elim_nhds_subcover isCompact_univ U fun x _ => hU x

Result:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
t : Finset X
s : univ ⊆ ⋃ x ∈ t, U x
⊢ ∃ t, ⋃ x ∈ t, U x = ⊤
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
/-- Another formulation of the reflection formula in terms of `Gammaℝ`. -/
lemma Gammaℝ_div_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -(2 * n + 1)) :
    Gammaℝ s / Gammaℝ (1 - s) = Gammaℂ s * cos (π * s / 2)

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (s + 1).Gammaℝ ≠ 0

Tactic:
simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
  sub_eq_add_neg, ← neg_add]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
calc Gammaℝ s / Gammaℝ (1 - s)
_ = (Gammaℝ s * Gammaℝ (s + 1)) / (Gammaℝ (1 - s) * Gammaℝ (1 + s)) := by
  rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
    mul_div_cancel_right₀ _ this]
_ = (2 * (2 * π) ^ (-s) * Gamma s) / ((cos (π * s / 2))⁻¹) := by
  rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
_ = _ := by rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)

Tactic:
rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
  mul_div_cancel_right₀ _ this]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) = 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹

Tactic:
rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]

Result:
no goals

Proof state:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
have : Gammaℝ (s + 1) ≠ 0 := by
  simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
    sub_eq_add_neg, ← neg_add]

Result:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iInter_Iio_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) : ⋂ i, Iio (f i) = ∅

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ∅

Tactic:
rw [← iInter_Iic_eq_empty_iff.mpr hf]

Result:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ⋂ i, Iic (f i)

Proof state:
case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
i✝ : ι
⊢ Iio (f i✝) ⊆ Iic (f i✝)

Tactic:
exact Iio_subset_Iic_self

Result:
no goals

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) = ∅

Tactic:
refine eq_empty_of_subset_empty ?_

Result:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ∅

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ ⋂ i, Iio (f i) ⊆ ⋂ i, Iic (f i)

Tactic:
gcongr

Result:
case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
i✝ : ι
⊢ Iio (f i✝) ⊆ Iic (f i✝)
-- Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean
theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
    {f f' : E → F} {g g' : E → G} {v : E} {B : F →L[ℝ] G →L[ℝ] W}
    (hf'g : Integrable (fun x ↦ B (f' x) (g x)) μ) (hfg' : Integrable (fun x ↦ B (f x) (g' x)) μ)
    (hfg : Integrable (fun x ↦ B (f x) (g x)) μ)
    (hf : ∀ x, HasLineDerivAt ℝ f (f' x) x v) (hg : ∀ x, HasLineDerivAt ℝ g (g' x) x v) :
    ∫ x, B (f x) (g' x) ∂μ = - ∫ x, B (f' x) (g x) ∂μ

Proof state:
case pos.inr
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ

Tactic:
have : Nontrivial E := nontrivial_iff.2 ⟨v, 0, hv⟩

Result:
case pos.inr
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevAt_go (xs : List α) (n : Nat) (acc : List α) :
    splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)

Proof state:
case cons.succ
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat) (acc : List α), splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)
acc : List α
n : Nat
⊢ splitRevAt.go (x :: xs) (n + 1) acc = ((take (n + 1) (x :: xs)).reverse ++ acc, drop (n + 1) (x :: xs))

Tactic:
rw [splitRevAt.go, ih n (x :: acc), take_succ_cons, reverse_cons, drop_succ_cons,
  append_assoc, singleton_append]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat) (acc : List α), splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)
acc : List α
⊢ splitRevAt.go (x :: xs) 0 acc = ((take 0 (x :: xs)).reverse ++ acc, drop 0 (x :: xs))

Tactic:
simp [splitRevAt.go]

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
acc : List α
⊢ splitRevAt.go [] n acc = ((take n []).reverse ++ acc, drop n [])

Tactic:
simp [splitRevAt.go]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
n : Nat
acc : List α
⊢ splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)

Tactic:
induction xs generalizing n acc with
| nil => simp [splitRevAt.go]
| cons x xs ih =>
  cases n with
  | zero => simp [splitRevAt.go]
  | succ n =>
    rw [splitRevAt.go, ih n (x :: acc), take_succ_cons, reverse_cons, drop_succ_cons,
      append_assoc, singleton_append]

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (n : Nat) (acc : List α), splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)
n : Nat
acc : List α
⊢ splitRevAt.go (x :: xs) n acc = ((take n (x :: xs)).reverse ++ acc, drop n (x :: xs))

Tactic:
cases n with
| zero => simp [splitRevAt.go]
| succ n =>
  rw [splitRevAt.go, ih n (x :: acc), take_succ_cons, reverse_cons, drop_succ_cons,
    append_assoc, singleton_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_modify (as : Array α) (f : α → α) :
    (as.modify x f).toList = as.toList.modify f x

Proof state:
case h
α : Type u_1
x : Nat
as : Array α
f : α → α
⊢ ∀ (i : Nat) (h₁ : i < (as.modify x f).toList.length) (h₂ : i < (List.modify f x as.toList).length),
    (as.modify x f).toList[i] = (List.modify f x as.toList)[i]

Tactic:
simp [getElem_modify, List.getElem_modify]

Result:
no goals

Proof state:
case hl
α : Type u_1
x : Nat
as : Array α
f : α → α
⊢ (as.modify x f).toList.length = (List.modify f x as.toList).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
x : Nat
as : Array α
f : α → α
⊢ (as.modify x f).toList = List.modify f x as.toList

Tactic:
apply List.ext_getElem

Result:
case hl
α : Type u_1
x : Nat
as : Array α
f : α → α
⊢ (as.modify x f).toList.length = (List.modify f x as.toList).length

case h
α : Type u_1
x : Nat
as : Array α
f : α → α
⊢ ∀ (i : Nat) (h₁ : i < (as.modify x f).toList.length) (h₂ : i < (List.modify f x as.toList).length),
    (as.modify x f).toList[i] = (List.modify f x as.toList)[i]
-- Mathlib/Data/List/Sublists.lean
theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l.sublists → l₁ ++ l₂ ~ l

Proof state:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
  zip_map_left] at *

Result:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun x => x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]

Proof state:
case nil
α : Type u
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse → l₁ ++ l₂ ~ []

Tactic:
intro l₁ l₂ h

Result:
case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ ++ l₂ ~ []
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_ofFinsupp {f : R →+* S} {x : S} {p : R[ℕ]} :
    eval₂ f x (⟨p⟩ : R[X]) = liftNC (↑f) (powersHom S x) p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[ℕ]
⊢ ∑ x_1 ∈ p.support, f (p x_1) * x ^ x_1 = (liftNC ↑f ⇑((powersHom S) x)) p

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[ℕ]
⊢ eval₂ f x { toFinsupp := p } = (liftNC ↑f ⇑((powersHom S) x)) p

Tactic:
simp only [eval₂_eq_sum, sum, toFinsupp_sum, support, coeff]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[ℕ]
⊢ ∑ x_1 ∈ p.support, f (p x_1) * x ^ x_1 = (liftNC ↑f ⇑((powersHom S) x)) p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem insertIdx_eraseIdx_of_ge :
    ∀ n m as,
      n < length as → n ≤ m → insertIdx m a (as.eraseIdx n) = (as.insertIdx (m + 1) a).eraseIdx n
  | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
  | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
  | 0, _ + 1, _ :: _, _, _ => rfl
  | n + 1, m + 1, a :: as, has, hmn =>
    congrArg (cons a) <|
      insertIdx_eraseIdx_of_ge n m as (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)

Proof state:
α : Type u
a head✝ : α
as : List α
x✝¹ : 0 < (head✝ :: as).length
x✝ : 0 ≤ 0
⊢ insertIdx 0 a ((head✝ :: as).eraseIdx 0) = (insertIdx (0 + 1) a (head✝ :: as)).eraseIdx 0

Tactic:
simp [eraseIdx, insertIdx]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
/-- In a non-trivial series `p`, the last element of `p.eraseLast` is related to `p.last` -/
lemma eraseLast_last_rel_last (p : RelSeries r) (h : p.length ≠ 0) :
    r p.eraseLast.last p.last

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ r (p.toFun ⟨p.length - 1, ⋯⟩) (p.toFun ⟨p.length, ⋯⟩)

Tactic:
convert p.step ⟨p.length - 1, by omega⟩

Result:
case h.e'_2.h.e'_4.h.e'_2
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = ↑⟨p.length - 1, ⋯⟩.succ

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ r p.eraseLast.last p.last

Tactic:
simp only [last, Fin.last, eraseLast_length, eraseLast_toFun]

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ r (p.toFun ⟨p.length - 1, ⋯⟩) (p.toFun ⟨p.length, ⋯⟩)

Proof state:
case h.e'_2.h.e'_4.h.e'_2
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length - 1 < p.length

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h.e'_2
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = ↑⟨p.length - 1, ⋯⟩.succ

Tactic:
simp only [Nat.succ_eq_add_one, Fin.succ_mk]

Result:
case h.e'_2.h.e'_4.h.e'_2
α : Type u_1
r : Rel α α
p : RelSeries r
h : p.length ≠ 0
⊢ p.length = p.length - 1 + 1
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma mono_f₁₃ [Mono sq.f₂₄] : Mono sq.f₁₃ :=
  (MorphismProperty.monomorphisms C).of_isPullback h (by assumption)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₂₄
⊢ MorphismProperty.monomorphisms C sq.f₂₄

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma covariant_sequence_exact₃ {n₀ : ℕ} (x₃ : Ext X S.X₃ n₀) {n₁ : ℕ} (hn₁ : n₀ + 1 = n₁)
    (hx₃ : x₃.comp hS.extClass hn₁ = 0) :
    ∃ (x₂ : Ext X S.X₂ n₀), x₂.comp (mk₀ S.g) (add_zero n₀) = x₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                  (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁)) ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
exact this x₃ hx₃

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
have := covariant_sequence_exact₃' X hS n₀ n₁ hn₁

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁)) ⋯).Exact
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁)) ⋯).Exact
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁))
            ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯)) (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁))
                ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).postcomp X ⋯))
                  (AddCommGrp.ofHom (hS.extClass.postcomp X hn₁)) ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃
-- Mathlib/Order/Interval/Set/SurjOn.lean
theorem surjOn_Ioo_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f)
    (a b : α) : SurjOn f (Ioo a b) (Ioo (f a) (f b))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
p : β
hp : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ioo a b

Tactic:
rcases h_surj p with ⟨x, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ f x ∈ f '' Ioo a b

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : a < x → b ≤ x
⊢ f x ∉ Ioo (f a) (f b)

Tactic:
exact fun h => h.2.not_le (h_mono <| hp <| h_mono.reflect_lt h.1)

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ f x ∈ f '' Ioo a b

Tactic:
refine ⟨x, mem_Ioo.2 ?_, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ a < x ∧ x < b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioo a b) (Ioo (f a) (f b))

Tactic:
intro p hp

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
p : β
hp : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ioo a b

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ a < x ∧ x < b

Tactic:
contrapose! hp

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : a < x → b ≤ x
⊢ f x ∉ Ioo (f a) (f b)