harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Maps/Proper/UniversallyClosed.lean
theorem isProperMap_iff_isClosedMap_ultrafilter {X : Type u} {Y : Type v} [TopologicalSpace X]
    [TopologicalSpace Y] {f : X → Y} :
    IsProperMap f ↔ Continuous f ∧ IsClosedMap
      (Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X)

Proof state:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
⊢ False

Tactic:
rw [mem_closure_iff_nhds] at hx

Result:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd✝), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
⊢ False
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_add_right {s t u : Multiset α} :
    Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u

Proof state:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint s (t + u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
rw [_root_.disjoint_comm, disjoint_add_left]

Result:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma one_fromRows_isTotallyUnimodular_iff [DecidableEq n] (A : Matrix m n R) :
    (fromRows (1 : Matrix n n R) A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
⊢ fromRows 1 A = (reindex (Equiv.sumComm m n) (Equiv.refl n)) (A.fromRows 1)

Tactic:
aesop

Result:
no goals

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
⊢ (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
have hA :
  fromRows (1 : Matrix n n R) A =
    (fromRows A (1 : Matrix n n R)).reindex (Equiv.sumComm m n) (Equiv.refl n) := by
  aesop

Result:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
hA : fromRows 1 A = (reindex (Equiv.sumComm m n) (Equiv.refl n)) (A.fromRows 1)
⊢ (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
hA : fromRows 1 A = (reindex (Equiv.sumComm m n) (Equiv.refl n)) (A.fromRows 1)
⊢ (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
rw [hA, reindex_isTotallyUnimodular, fromRows_one_isTotallyUnimodular_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem odd_card_odd_degree_vertices_ne [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V)
    (h : Odd (G.degree v)) : Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Tactic:
have hk : 0 < k := by
  have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
    use v
    simp only [true_and, mem_filter, mem_univ]
    exact h
  rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
  exact zero_lt_two

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Tactic:
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v := by
  ext w
  rw [and_comm]

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ 0 < k

Tactic:
have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
  use v
  simp only [true_and, mem_filter, mem_univ]
  exact h

Result:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hh : (filter (fun v => Odd (G.degree v)) univ).Nonempty
⊢ 0 < k

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Tactic:
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ Odd #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SFinite ν] ⦃f : α → β → E⦄
    (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

case neg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν
-- Mathlib/Algebra/Module/Injective.lean
theorem injective (h : Module.Baer R Q) : Module.Injective R Q where
  out X Y _ _ _ _ i hi f

Proof state:
case intro
R : Type u
inst✝² : Ring R
Q : Type v
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
h✝ : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
exact ⟨h, DFunLike.congr_fun H⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
Q : Type v
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
h : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), h (i x) = f x

Tactic:
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f

Result:
case intro
R : Type u
inst✝² : Ring R
Q : Type v
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
h✝ : Baer R Q
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
i : X →ₗ[R] Y
hi : Function.Injective ⇑i
f : X →ₗ[R] Q
h : Y →ₗ[R] Q
H : h ∘ₗ i = f
⊢ ∃ h, ∀ (x : X), h (i x) = f x
-- Mathlib/Topology/Basic.lean
theorem TopologicalSpace.ext_iff {t t' : TopologicalSpace X} :
    t = t' ↔ ∀ s, IsOpen[t] s ↔ IsOpen[t'] s :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

Proof state:
case a.h.a
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen s ↔ IsOpen s
x✝ : Set X
⊢ IsOpen x✝ ↔ IsOpen x✝

Tactic:
exact h _

Result:
no goals

Proof state:
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen s ↔ IsOpen s
⊢ t = t'

Tactic:
ext

Result:
case a.h.a
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen s ↔ IsOpen s
x✝ : Set X
⊢ IsOpen x✝ ↔ IsOpen x✝
-- Mathlib/Data/Multiset/DershowitzManna.lean
/-- If all elements of a multiset `M` are accessible with `<`, then the multiset `M` is
accessible given the `OneStep` relation. -/
private lemma acc_oneStep_of_acc_lt (hM : ∀ x ∈ M, Acc LT.lt x) : Acc OneStep M

Proof state:
case empty
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ x ∈ 0, Acc LT.lt x
⊢ Acc Multiset.OneStep 0

Tactic:
constructor

Result:
case empty.h
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), Multiset.OneStep y 0 → Acc Multiset.OneStep y

Proof state:
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ x ∈ M, Acc LT.lt x
⊢ Acc Multiset.OneStep M

Tactic:
induction M using Multiset.induction_on with
| empty =>
  constructor
  simp [OneStep, eq_comm (b := _ + _)]
| cons a M ih =>
  exact acc_oneStep_cons_of_acc_lt (hM _ <| mem_cons_self ..) <| ih fun x hx ↦
    hM _ <| mem_cons_of_mem hx

Result:
no goals

Proof state:
case empty.h
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ x ∈ 0, Acc LT.lt x
⊢ ∀ (y : Multiset α), Multiset.OneStep y 0 → Acc Multiset.OneStep y

Tactic:
simp [OneStep, eq_comm (b := _ + _)]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : Preorder α
M✝ : Multiset α
a : α
M : Multiset α
ih : (∀ x ∈ M, Acc LT.lt x) → Acc Multiset.OneStep M
hM : ∀ x ∈ a ::ₘ M, Acc LT.lt x
⊢ Acc Multiset.OneStep (a ::ₘ M)

Tactic:
exact acc_oneStep_cons_of_acc_lt (hM _ <| mem_cons_self ..) <| ih fun x hx ↦
  hM _ <| mem_cons_of_mem hx

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem singleton_one_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) :
    IsCyclotomicExtension {1} A B

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
⊢ IsCyclotomicExtension {1} A B

Tactic:
convert (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h)

Result:
case h.e'_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
⊢ {1} = ∅ ∪ {1}

Proof state:
case h.e'_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ⊥ = ⊤
⊢ {1} = ∅ ∪ {1}

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/OrderIso.lean
theorem isLUB_preimage' {s : Set β} {x : β} : IsLUB (f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Tactic:
rw [isLUB_preimage, f.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/List/TFAE.lean
theorem tfae_not_iff {l : List Prop} : TFAE (l.map Not) ↔ TFAE l

Proof state:
l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  Decidable.not_iff_not]

Result:
no goals

Proof state:
l : List Prop
⊢ (map Not l).TFAE ↔ l.TFAE

Tactic:
classical
simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  Decidable.not_iff_not]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_sub {x y : EReal} (hy : 0 ≤ y) :
    (x - y).toENNReal = x.toENNReal - y.toENNReal

Proof state:
case h_top.h_top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Result:
no goals

Proof state:
case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ 0 = (↑x).toENNReal - (↑y).toENNReal

Tactic:
exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm

Result:
no goals

Proof state:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe,
  ofReal_sub x (EReal.coe_nonneg.mp hy)]

Result:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal x - ENNReal.ofReal y = (↑x).toENNReal - (↑y).toENNReal

Proof state:
case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]

Result:
case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ 0 = (↑x).toENNReal - (↑y).toENNReal

Proof state:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal x - ENNReal.ofReal y = (↑x).toENNReal - (↑y).toENNReal

Tactic:
simp

Result:
no goals

Proof state:
case h_real.h_real
x y : ℝ
hy : 0 ≤ ↑y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
by_cases hxy : x ≤ y

Result:
case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal

Tactic:
rename_i x y

Result:
case h_real.h_real
x y : ℝ
hy : 0 ≤ ↑y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- If `s` is σ-compact and `f` is continuous on `s`, `f(s)` is σ-compact. -/
lemma IsSigmaCompact.image_of_continuousOn {f : X → Y} {s : Set X} (hs : IsSigmaCompact s)
    (hf : ContinuousOn f s) : IsSigmaCompact (f '' s)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ ∀ (n : ℕ), IsCompact ((fun n => f '' K n) n)

Tactic:
exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsSigmaCompact s
hf : ContinuousOn f s
⊢ IsSigmaCompact (f '' s)

Tactic:
rcases hs with ⟨K, hcompact, hcov⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ IsSigmaCompact (f '' s)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ IsSigmaCompact (f '' s)

Tactic:
refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : ContinuousOn f s
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = s
⊢ ∀ (n : ℕ), IsCompact ((fun n => f '' K n) n)
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a.2 :=
  have :
    Primrec₂ fun (_ : Unit) (n : ℕ) =>
      let a := ofNat (ℕ × Code) n
      (List.range a.1).map (evaln a.1 a.2) :=
    Primrec.nat_strong_rec _ (hG.comp Primrec.snd).to₂ fun _ p => by
      simp only [G, prod_ofNat_val, ofNat_nat, List.length_map, List.length_range,
        Nat.pair_unpair, Option.some_inj]
      refine List.map_congr_left fun n => ?_
      have : List.range p = List.range (Nat.pair p.unpair.1 (encode (ofNat Code p.unpair.2)))

Proof state:
case succ.prec.intro.zero
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      Nat.Partrec.Code.lup
          (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
⊢ Nat.rec (evaln k cf (unpair n).1)
      (fun n_1 n_ih =>
        (Nat.Partrec.Code.lup
              (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
                (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
              (k', cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind
          fun i =>
          Nat.Partrec.Code.lup
            (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
            (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0 =
    Nat.rec (evaln (k' + 1) cf (unpair n).1)
      (fun n_1 n_ih =>
        (evaln k' (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
          evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      0

Tactic:
rfl

Result:
no goals

Proof state:
case succ.prec.intro.succ.none
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf cg : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode (cf.prec cg)) →
      Nat.Partrec.Code.lup
          (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode (cf.prec cg)))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode (cf.prec cg)
lg : encode cg < encode (cf.prec cg)
n✝ : ℕ
⊢ (Option.none.bind fun i =>
      Nat.Partrec.Code.lup
        (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
          (List.range (Nat.pair (k' + 1) (encode (cf.prec cg)))))
        (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n✝ i))) =
    Option.none.bind fun i => evaln (k' + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ i))

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_prim : Primrec fun a : (ℕ × Code) × ℕ => evaln a.1.1 a.1.2 a.2 :=
  have :
    Primrec₂ fun (_ : Unit) (n : ℕ) =>
      let a := ofNat (ℕ × Code) n
      (List.range a.1).map (evaln a.1 a.2) :=
    Primrec.nat_strong_rec _ (hG.comp Primrec.snd).to₂ fun _ p => by
      simp only [G, prod_ofNat_val, ofNat_nat, List.length_map, List.length_range,
        Nat.pair_unpair, Option.some_inj]
      refine List.map_congr_left fun n => ?_
      have : List.range p = List.range (Nat.pair p.unpair.1 (encode (ofNat Code p.unpair.2)))

Proof state:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      Nat.Partrec.Code.lup
          (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((Nat.Partrec.Code.lup
          (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
          (k' + 1, cf) n).bind
      fun x =>
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih =>
          Nat.Partrec.Code.lup
            (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a =>
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))

Tactic:
rw [hg (Nat.pair_lt_pair_right _ lf)]

Result:
case succ.rfind'
x✝ : Unit
p n : ℕ
this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))
k' : ℕ
k : ℕ := k' + 1
nk : n ≤ k'
cf : Code
hg :
  ∀ {k' : ℕ} {c' : Code} {n : ℕ},
    Nat.pair k' (encode c') < Nat.pair k (encode cf.rfind') →
      Nat.Partrec.Code.lup
          (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
            (List.range (Nat.pair k (encode cf.rfind'))))
          (k', c') n =
        evaln k' c' n
lf : encode cf < encode cf.rfind'
⊢ ((evaln k cf n).bind fun x =>
      Nat.rec (some (unpair n).2)
        (fun n_1 n_ih =>
          Nat.Partrec.Code.lup
            (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1))
              (List.range (Nat.pair (k' + 1) (encode cf.rfind'))))
            (k', cf.rfind') (Nat.pair (unpair n).1 ((unpair n).2 + 1)))
        x) =
    (evaln (k' + 1) cf n).bind fun a =>
      if a = 0 then some (unpair n).2 else evaln k' cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem Path.reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (p : Path a b) :
    p.reverse.reverse = p

Proof state:
case nil
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
⊢ nil.reverse.reverse = nil

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
p : Path a b
⊢ p.reverse.reverse = p

Tactic:
induction p with
| nil => simp
| cons _ _ h =>
  rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
  rfl

Result:
no goals

Proof state:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp a✝.toPath = a✝¹.cons a✝

Tactic:
rfl

Result:
no goals

Proof state:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ (a✝¹.cons a✝).reverse.reverse = a✝¹.cons a✝

Tactic:
rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]

Result:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp a✝.toPath = a✝¹.cons a✝