harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/
lemma lt_iff_transGen_covBy [Preorder α] [LocallyFiniteOrder α] {x y : α} :
    x < y ↔ TransGen (· ⋖ ·) x y

Proof state:
case tail
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ c✝ : α
a✝ : TransGen (fun x1 x2 => x1 ⋖ x2) x b✝
hb : b✝ ⋖ c✝
ih : x < b✝
⊢ x < c✝

Tactic:
exact ih.trans hb.1

Result:
no goals

Proof state:
case single
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ : α
hx : x ⋖ b✝
⊢ x < b✝

Tactic:
exact hx.1

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
h : TransGen (fun x1 x2 => x1 ⋖ x2) x y
⊢ x < y

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
h : TransGen (fun x1 x2 => x1 ⋖ x2) x y
⊢ x < y

Tactic:
induction h with
| single hx => exact hx.1
| tail _ hb ih => exact ih.trans hb.1

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix'_apply (f : (n → R) →ₗ[R] m → R) (i j) :
    LinearMap.toMatrix' f i j = f (fun j' ↦ if j' = j then 1 else 0) i

Proof state:
case h.e_6.h.h
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
⊢ Pi.single j 1 j' = if j' = j then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : j' = j
⊢ Pi.single j 1 j' = 1

case neg
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : ¬j' = j
⊢ Pi.single j 1 j' = 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ f (Pi.single j 1) = f fun j' => if j' = j then 1 else 0

Tactic:
congr

Result:
case h.e_6.h
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ Pi.single j 1 = fun j' => if j' = j then 1 else 0

Proof state:
case neg
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : ¬j' = j
⊢ Pi.single j 1 j' = 0

Tactic:
apply Pi.single_eq_of_ne h

Result:
no goals

Proof state:
case h.e_6.h
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ Pi.single j 1 = fun j' => if j' = j then 1 else 0

Tactic:
ext j'

Result:
case h.e_6.h.h
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
⊢ Pi.single j 1 j' = if j' = j then 1 else 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ f (Pi.single j 1) i = f (fun j' => if j' = j then 1 else 0) i

Tactic:
refine congr_fun ?_ _

Result:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ f (Pi.single j 1) = f fun j' => if j' = j then 1 else 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ toMatrix' f i j = f (fun j' => if j' = j then 1 else 0) i

Tactic:
simp only [LinearMap.toMatrix', LinearEquiv.coe_mk, of_apply]

Result:
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ f (Pi.single j 1) i = f (fun j' => if j' = j then 1 else 0) i

Proof state:
case pos
R : Type u_1
inst✝² : CommSemiring R
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : j' = j
⊢ Pi.single j 1 j' = 1

Tactic:
rw [h, Pi.single_eq_same]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.map [FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
a : α
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ Odd a → Odd (f a)

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ Odd (f (2 * a + 1))

Proof state:
case intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ Odd (f (2 * a + 1))

Tactic:
exact ⟨f a, by simp [two_mul]⟩

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ f (2 * a + 1) = 2 * f a + 1

Tactic:
simp [two_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma extClass_hom [HasDerivedCategory.{w'} C] : hS.extClass.hom = hS.singleδ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((SmallHom.equiv W Q)
          (SmallHom.mkInv (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯) ≫
        (SmallHom.equiv W Q)
          (SmallHom.mk W (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃)) ≫
      ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).hom =
    hS.singleδ

Tactic:
rw [SmallHom.equiv_mkInv, SmallHom.equiv_mk]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ ((isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
        Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃) ≫
      ((Q.commShiftIso 1).app ((CochainComplex.singleFunctor C 0).obj S.X₁)).hom =
    hS.singleδ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    (𝟙 ((singleFunctors C).functor 0)).app S.X₃ ≫
      inv
          (Q.map
            (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
        Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
          (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory C) 1).map
              ((𝟙 (((CochainComplex.singleFunctors C).postcomp Q).functor 0)).app S.X₁)

Tactic:
erw [Category.id_comp, Functor.map_id, Category.comp_id]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Q.commShiftIso 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁)
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem _root_.Filter.HasBasis.isVonNBounded_iff {q : ι → Prop} {s : ι → Set E} {A : Set E}
    (h : (𝓝 (0 : E)).HasBasis q s) : IsVonNBounded 𝕜 A ↔ ∀ i, q i → Absorbs 𝕜 (s i) A

Proof state:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A

Tactic:
refine ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V A

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A

Tactic:
exact (hA i hi).mono_left hV

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V A

Tactic:
rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : (𝓝 0).HasBasis q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV✝ : V ∈ 𝓝 0
i : ι
hi : q i
hV : s i ⊆ V
⊢ Absorbs 𝕜 V A
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_left_midpoint_eq_dist_right_midpoint (p₁ p₂ : P) :
    dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)

Tactic:
rw [dist_left_midpoint p₁ p₂, dist_right_midpoint p₁ p₂]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
  | 0, k₂, c, n, x, _, h => by simp [evaln] at h
  | k + 1, k₂ + 1, c, n, x, hl, h => by
    have hl' := Nat.le_of_succ_le_succ hl
    have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ }

Proof state:
case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) cf n <*> evaln (k₂ + 1) cg n

Tactic:
simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some,
  Option.map_eq_some', exists_exists_and_eq_and] at h ⊢

Result:
case pair
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a, evaln (k₂ + 1) cf n = some a ∧ ∃ a_1, evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
  | 0, k₂, c, n, x, _, h => by simp [evaln] at h
  | k + 1, k₂ + 1, c, n, x, hl, h => by
    have hl' := Nat.le_of_succ_le_succ hl
    have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ }

Proof state:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
⊢ x ∈ evaln (k₂ + 1) c n

Tactic:
simp only [Option.mem_def] at h ⊢

Result:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
h : evaln (k + 1) c n = some x
⊢ evaln (k₂ + 1) c n = some x

Proof state:
case comp
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        let x ← evaln (k + 1) cg n
        evaln (k + 1) cf x)
      n =
    some x
h :
  x ∈ do
    let x ← evaln (k + 1) cg n
    evaln (k + 1) cf x
⊢ x ∈ do
    let x ← evaln (k₂ + 1) cg n
    evaln (k₂ + 1) cf x

Tactic:
simp? [Bind.bind, Option.bind_eq_some] at h ⊢ says
  simp only [bind, Option.mem_def, Option.bind_eq_some] at h ⊢

Result:
case comp
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        let x ← evaln (k + 1) cg n
        evaln (k + 1) cf x)
      n =
    some x
h : ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ a, evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x
-- Mathlib/Computability/PartrecCode.lean
theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
  | 0, k₂, c, n, x, _, h => by simp [evaln] at h
  | k + 1, k₂ + 1, c, n, x, hl, h => by
    have hl' := Nat.le_of_succ_le_succ hl
    have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ }

Proof state:
case prec
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a n =>
              Nat.casesOn n (evaln (k + 1) cf a) fun y => do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ x ∈
      unpaired
        (fun a n =>
          Nat.casesOn n (evaln (k + 1) cf a) fun y => do
            let i ← evaln k (cf.prec cg) (Nat.pair a y)
            evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
        n →
    x ∈
      unpaired
        (fun a n =>
          Nat.casesOn n (evaln (k₂ + 1) cf a) fun y => do
            let i ← evaln k₂ (cf.prec cg) (Nat.pair a y)
            evaln (k₂ + 1) cg (Nat.pair a (Nat.pair y i)))
        n

Tactic:
simp only [unpaired, bind, Option.mem_def]

Result:
case prec
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a n =>
              Nat.casesOn n (evaln (k + 1) cf a) fun y => do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ 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)))
        (unpair n).2 =
      some x →
    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)))
        (unpair n).2 =
      some x
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp' c k) S

Proof state:
case cons.refine_2.refine_1
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHfs : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Supports (codeSupp' fs k) S
k : Cont'
H : codeSupp (f.cons fs) k ⊆ S
H' :
  trStmts₁ (trNormal (f.cons fs) k) ⊆ S ∧
    codeSupp' f (Cont'.cons₁ fs k) ∪
        (trStmts₁
            (move₂ (fun x => false) main aux
              (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
                (move₂ (fun x => false) aux stack (trNormal fs k.cons₂)))) ∪
          codeSupp fs k.cons₂) ⊆
      S
h✝ :
  codeSupp' f (Cont'.cons₁ fs k) ∪
      (trStmts₁
          (move₂ (fun x => false) main aux
            (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
              (move₂ (fun x => false) aux stack (trNormal fs k.cons₂)))) ∪
        (codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)))) ⊆
    S
h : codeSupp' fs k.cons₂ ∪ trStmts₁ (head stack (Λ'.ret k)) ⊆ S
⊢ codeSupp fs k.cons₂ ⊆ S

Tactic:
exact Finset.union_subset_right (Finset.union_subset_right H'.2)

Result:
no goals

Proof state:
case comp.refine_1
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ codeSupp f k ⊆ S

Tactic:
simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢

Result:
case comp.refine_1
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S
H :
  (trStmts₁ (trNormal (f.comp g) k) ⊆ S ∧
      codeSupp' g (Cont'.comp f k) ⊆ S ∧ trStmts₁ (trNormal f k) ⊆ S ∧ codeSupp' f k ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f k ⊆ S ∧ contSupp k ⊆ S
-- Mathlib/RingTheory/HahnSeries/PowerSeries.lean
theorem ofPowerSeries_X_pow {R} [Semiring R] (n : ℕ) :
    ofPowerSeries Γ R (PowerSeries.X ^ n) = single (n : Γ) 1

Proof state:
Γ : Type u_1
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_3
inst✝ : Semiring R
n : ℕ
⊢ (ofPowerSeries Γ R) (PowerSeries.X ^ n) = (single ↑n) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulDysonETransform_idem :
    mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x

Tactic:
ext : 1 <;> dsimp

Result:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2

case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1

Proof state:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1

Tactic:
exact inter_subset_union

Result:
no goals

Proof state:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2

Tactic:
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]

Result:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Proof state:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Tactic:
exact inter_subset_union

Result:
no goals

Proof state:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1

Tactic:
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]

Result:
case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1
-- Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
theorem compExactValue_correctness_of_stream_eq_some_aux_comp {a : K} (b c : K)
    (fract_a_ne_zero : Int.fract a ≠ 0) :
    ((⌊a⌋ : K) * b + c) / Int.fract a + b = (b * a + c) / Int.fract a

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ (↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a

Tactic:
field_simp [fract_a_ne_zero]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * Int.fract a = b * a + c

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * Int.fract a = b * a + c

Tactic:
rw [Int.fract]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c