harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem le_order (φ : R⟦X⟧) (n : ℕ∞) (h : ∀ i : ℕ, ↑i < n → coeff R i φ = 0) :
    n ≤ order φ

Proof state:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff R i) φ = 0
⊢ ∀ i < n, (coeff R i) φ = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff R i) φ = 0
⊢ ∀ (n : ℕ), (coeff R n) φ = (coeff R n) 0

Tactic:
simpa using h

Result:
no goals

Proof state:
case top
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff R i) φ = 0
⊢ ⊤ ≤ φ.order

Tactic:
simpa using ext (by simpa using h)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ∞
h : ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0
⊢ n ≤ φ.order

Tactic:
cases n with
| top => simpa using ext (by simpa using h)
| coe n =>
  convert nat_le_order φ n _
  simpa using h

Result:
no goals

Proof state:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff R i) φ = 0
⊢ ↑n ≤ φ.order

Tactic:
convert nat_le_order φ n _

Result:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff R i) φ = 0
⊢ ∀ i < n, (coeff R i) φ = 0
-- Mathlib/Data/Finset/Dedup.lean
theorem perm_of_nodup_nodup_toFinset_eq (hl : Nodup l) (hl' : Nodup l')
    (h : l.toFinset = l'.toFinset) : l ~ l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l ~ l'

Tactic:
rw [← Multiset.coe_eq_coe]

Result:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ ↑l = ↑l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ ↑l = ↑l'

Tactic:
exact Multiset.Nodup.toFinset_inj hl hl' h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_trans {x y z : BitVec n} : x ≤ y → y ≤ z → x ≤ z

Proof state:
n : Nat
x y z : BitVec n
⊢ x ≤ y → y ≤ z → x ≤ z

Tactic:
simp only [le_def]

Result:
n : Nat
x y z : BitVec n
⊢ x.toNat ≤ y.toNat → y.toNat ≤ z.toNat → x.toNat ≤ z.toNat

Proof state:
n : Nat
x y z : BitVec n
⊢ x.toNat ≤ y.toNat → y.toNat ≤ z.toNat → x.toNat ≤ z.toNat

Tactic:
apply Nat.le_trans

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem add_sigma (s t : Multiset α) (u : ∀ a, Multiset (σ a)) :
    (s + t).sigma u = s.sigma u + t.sigma u

Proof state:
α : Type u_1
σ : α → Type u_4
s t : Multiset α
u : (a : α) → Multiset (σ a)
⊢ (s + t).sigma u = s.sigma u + t.sigma u

Tactic:
simp [Multiset.sigma]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem transversal_nonempty (hφ : ∀ i, Injective (φ i)) : Nonempty (Transversal φ)

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range) (t i) ∧ 1 ∈ t i
⊢ Nonempty (Transversal φ)

Tactic:
apply Nonempty.intro

Result:
case val
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range) (t i) ∧ 1 ∈ t i
⊢ Transversal φ

Proof state:
case val
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range) (t i) ∧ 1 ∈ t i
⊢ Transversal φ

Tactic:
exact
  { injective := hφ
    set := t
    one_mem := fun i => (ht i).2
    compl := fun i => (ht i).1 }

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
⊢ Nonempty (Transversal φ)

Tactic:
choose t ht using fun i => (φ i).range.exists_isComplement_right 1

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range) (t i) ∧ 1 ∈ t i
⊢ Nonempty (Transversal φ)
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem dirac_caratheodory (a : α) : (dirac a).caratheodory = ⊤ :=
  top_unique fun s _ t => by
    by_cases ht : a ∈ t; swap; · simp [ht]
    by_cases hs : a ∈ s <;> simp [*]

Proof state:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
swap

Result:
case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Proof state:
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
by_cases ht : a ∈ t

Result:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Proof state:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
by_cases hs : a ∈ s <;> simp [*]

Result:
no goals

Proof state:
case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∉ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem quasiIso_forget₂_εToSingle₀ :
    QuasiIso (((forget₂ _ (ModuleCat.{u} k)).mapHomologicalComplex _).map (εToSingle₀ k G))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
rw [← εToSingle₀_comp_eq k G] at h

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h :
  QuasiIso
    (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (Rep.trivial k G k))
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h :
  QuasiIso
    (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (Rep.trivial k G k))
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
exact quasiIso_of_comp_right (hφφ' := h)

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))

Tactic:
have h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom := inferInstance

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom
⊢ QuasiIso (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G))
-- Mathlib/Algebra/Homology/Embedding/HomEquiv.lean
@[simp]
lemma homRestrict_liftExtend (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ) :
    e.homRestrict (e.liftExtend φ hφ) = φ

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
⊢ e.homRestrict (e.liftExtend φ hφ) = φ

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i : ι
⊢ (e.homRestrict (e.liftExtend φ hφ)).f i = φ.f i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i : ι
⊢ (e.homRestrict (e.liftExtend φ hφ)).f i = φ.f i

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Result:
no goals
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem Finset.exists_disjoint_union_of_even_card [DecidableEq α] {s : Finset α} (he : Even #s) :
    ∃ (t u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  let ⟨n, hn⟩ := he
  let ⟨t, ht, ht'⟩ := exists_subset_card_eq (show n ≤ #s by omega)
  ⟨t, s \ t, by simp [card_sdiff, disjoint_sdiff, *]⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
he : Even #s
n : ℕ
hn : #s = n + n
t : Finset α
ht : t ⊆ s
ht' : #t = n
⊢ t ∪ s \ t = s ∧ Disjoint t (s \ t) ∧ #t = #(s \ t)

Tactic:
simp [card_sdiff, disjoint_sdiff, *]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
he : Even #s
n : ℕ
hn : #s = n + n
⊢ n ≤ #s

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.unique_zpow_zmod (ha : ∀ x : α, x ∈ zpowers a) (x : α) :
    ∃! n : ZMod (Fintype.card α), x = a ^ n.val

Proof state:
case intro.refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : ↑n = ↑↑y.val
⊢ y = ↑n

Tactic:
simp [hy]

Result:
no goals

Proof state:
case intro.refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ a ^ n = a ^ (↑n).val

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
  Int.modEq_comm, Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n

Tactic:
rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
  Nat.card_eq_fintype_card, ← ZMod.intCast_eq_intCast_iff] at hy

Result:
case intro.refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : ↑n = ↑↑y.val
⊢ y = ↑n

Proof state:
case intro
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ ∃! n_1, (fun x => a ^ x) n = a ^ n_1.val

Tactic:
refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩

Result:
case intro.refine_1
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ a ^ n = a ^ (↑n).val

case intro.refine_2
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
y : ZMod (Fintype.card α)
hy : a ^ n = a ^ y.val
⊢ y = ↑n

Proof state:
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
x : α
⊢ ∃! n, x = a ^ n.val

Tactic:
obtain ⟨n, rfl⟩ := ha x

Result:
case intro
α : Type u_1
a : α
inst✝¹ : Group α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
n : ℤ
⊢ ∃! n_1, (fun x => a ^ x) n = a ^ n_1.val
-- Mathlib/Probability/Kernel/Proper.lean
lemma isProper_iff_restrict_eq_indicator_smul (h𝓑𝓧 : 𝓑 ≤ 𝓧) :
    IsProper π ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
      π.restrict (h𝓑𝓧 _ hB) x = B.indicator (fun _ ↦ (1 : ℝ≥0∞)) x • π x

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩ <;> simpa only [inf_eq_left.2 h𝓑𝓧] using h

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_cancel_left (n m : ℕ) : n ^^^ (n ^^^ m) = m

Proof state:
n m : ℕ
⊢ n ^^^ (n ^^^ m) = m

Tactic:
rw [← Nat.xor_assoc, Nat.xor_self, zero_xor]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
lemma measurable_of_measurable_exp (hf : Measurable (fun x ↦ exp (f x))) :
    Measurable f

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
this : f = fun x => log (rexp (f x))
⊢ Measurable fun x => log (rexp (f x))

Tactic:
exact measurable_log.comp hf

Result:
no goals

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
⊢ Measurable f

Tactic:
have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]

Result:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
this : f = fun x => log (rexp (f x))
⊢ Measurable f

Proof state:
case h
α : Type u_1
x✝¹ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
x✝ : α
⊢ f x✝ = log (rexp (f x✝))

Tactic:
rw [log_exp]

Result:
no goals

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
this : f = fun x => log (rexp (f x))
⊢ Measurable f

Tactic:
rw [this]

Result:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
this : f = fun x => log (rexp (f x))
⊢ Measurable fun x => log (rexp (f x))

Proof state:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
⊢ f = fun x => log (rexp (f x))

Tactic:
ext

Result:
case h
α : Type u_1
x✝¹ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x => rexp (f x)
x✝ : α
⊢ f x✝ = log (rexp (f x✝))
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem balanced_empty : Balanced 𝕜 (∅ : Set E) := fun _ _ => by rw [smul_set_empty]

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ x✝¹ • ∅ ⊆ ∅

Tactic:
rw [smul_set_empty]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem of_part : ∀ {n f}, _root_.Partrec f → @Partrec' n f :=
  @(suffices ∀ f, Nat.Partrec f → @Partrec' 1 fun v => f v.head from fun {n f} hf => by
      let g := fun n₁ =>
        (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
      exact
        (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by
          dsimp only [g]; simp [encodek, Part.map_id']
    fun f hf => by
    obtain ⟨c, rfl⟩ := exists_code.1 hf
    simpa [eval_eq_rfindOpt] using
      rfindOpt <|
        of_prim <|
          Primrec.encode_iff.2 <|
            evaln_prim.comp <|
              (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
                Primrec.vector_head.comp Primrec.vector_tail)

Proof state:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
⊢ Partrec' f

Tactic:
let g := fun n₁ =>
  (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))

Result:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)
⊢ Partrec' f

Proof state:
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec' fun v => f v.head

Tactic:
obtain ⟨c, rfl⟩ := exists_code.1 hf

Result:
case intro
c : Code
hf : Partrec c.eval
⊢ Partrec' fun v => c.eval v.head

Proof state:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)
i : List.Vector ℕ n
⊢ g (encode i) = f i

Tactic:
dsimp only [g]

Result:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a => Part.map encode (f a)) = f i

Proof state:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)
⊢ Partrec' f

Tactic:
exact
  (comp₁ g (this g hf) (prim Nat.Primrec'.encode)).of_eq fun i => by
    dsimp only [g]; simp [encodek, Part.map_id']

Result:
no goals

Proof state:
case intro
c : Code
hf : Partrec c.eval
⊢ Partrec' fun v => c.eval v.head

Tactic:
simpa [eval_eq_rfindOpt] using
  rfindOpt <|
    of_prim <|
      Primrec.encode_iff.2 <|
        evaln_prim.comp <|
          (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
            Primrec.vector_head.comp Primrec.vector_tail

Result:
no goals

Proof state:
this : ∀ (f : ℕ →. ℕ), Partrec f → Partrec' fun v => f v.head
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : _root_.Partrec f
g : ℕ → Part ℕ := fun n₁ => (↑(decode n₁)).bind fun a => Part.map encode (f a)
i : List.Vector ℕ n
⊢ ((↑(decode (encode i))).bind fun a => Part.map encode (f a)) = f i

Tactic:
simp [encodek, Part.map_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
    l₁.filter p <:+ l₂.filter p

Proof state:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p (xs ++ l₁)

Tactic:
rw [filter_append]

Result:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p xs ++ List.filter p l₁

Proof state:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p xs ++ List.filter p l₁

Tactic:
apply suffix_append

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <:+ l₂
⊢ List.filter p l₁ <:+ List.filter p l₂

Tactic:
obtain ⟨xs, rfl⟩ := h

Result:
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p (xs ++ l₁)
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq

Proof state:
p q : Prop
hp : p
hq : q
⊢ HEq hp hq

Tactic:
cases propext (iff_of_true hp hq)

Result:
case refl
p : Prop
hp hq : p
⊢ HEq hp hq

Proof state:
case refl
p : Prop
hp hq : p
⊢ HEq hp hq

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma lt_or_gt_of_ne (h : a ≠ b) : a < b ∨ a > b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≠ b
⊢ a < b ∨ a > b

Tactic:
simpa [h] using lt_trichotomy a b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_concat (L : List (List α)) (l : List α) : flatten (L ++ [l]) = flatten L ++ l

Proof state:
α : Type u_1
L : List (List α)
l : List α
⊢ (L ++ [l]).flatten = L.flatten ++ l

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toLeft_image_swap : (u.image Sum.swap).toLeft = u.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_append : ∀ s m n step : Nat,
    range' s m step ++ range' (s + step * m) n step = range' s (m + n) step
  | _, 0, _, _ => by simp
  | s, m + 1, n, step => by
    simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
      using range'_append (s + step) m n step

Proof state:
s m n step : Nat
⊢ range' s (m + 1) step ++ range' (s + step * (m + 1)) n step = range' s (m + 1 + n) step

Tactic:
simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
  using range'_append (s + step) m n step

Result:
no goals

Proof state:
x✝² x✝¹ x✝ : Nat
⊢ range' x✝² 0 x✝ ++ range' (x✝² + x✝ * 0) x✝¹ x✝ = range' x✝² (0 + x✝¹) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Nonempty.ciSup_mem_image {s : Set ι} (h : s.Nonempty) (hs : s.Finite) :
    ⨆ i ∈ s, f i ∈ f '' s :=
  hs.ciSup_mem_image _ (h.imp (by simp))

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Set ι
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem idealOfLE_ofPrime (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
    idealOfLE A (ofPrime A P) (le_ofPrime A P) = P

Proof state:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P

Tactic:
refine Ideal.ext (fun x => ?_)

Result:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P

Proof state:
case h
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ optParam (IsLocalRing ↥(A.ofPrime P)) ⋯

Tactic:
exact isLocalRing (ofPrime A P)

Result:
no goals

Proof state:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ x ∈ A.idealOfLE (A.ofPrime P) ⋯ ↔ x ∈ P

Tactic:
apply IsLocalization.AtPrime.to_map_mem_maximal_iff

Result:
case h
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ optParam (IsLocalRing ↥(A.ofPrime P)) ⋯
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_single (x : HahnSeries Γ R) : (single x).hsum = x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x : HahnSeries Γ R
⊢ (single x).hsum = x

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x : HahnSeries Γ R
g : Γ
⊢ (single x).hsum.coeff g = x.coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x : HahnSeries Γ R
g : Γ
⊢ (single x).hsum.coeff g = x.coeff g

Tactic:
simp only [coeff_hsum, single_toFun, finsum_unique]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem one_gcd {n : ℕ+} : gcd 1 n = 1

Proof state:
n : ℕ+
⊢ gcd 1 n = 1

Tactic:
rw [← gcd_eq_left_iff_dvd]

Result:
n : ℕ+
⊢ 1 ∣ n

Proof state:
n : ℕ+
⊢ 1 ∣ n

Tactic:
apply one_dvd

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem Tendsto.atBot_mul_atTop₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
have : Tendsto (fun x => -f x * g x) l atTop :=
  (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg

Result:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x => -f x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x => -f x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_neg_mul, neg_neg] using
  tendsto_neg_atTop_atBot.comp this

Result:
no goals