harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem cast_cast {l : Vector α n} {w : n = m} {w' : m = k} :
    (l.cast w).cast w' = l.cast (w.trans w')

Proof state:
case mk
α : Type u_1
m k : Nat
w' : m = k
l : Array α
w : l.size = m
⊢ Vector.cast w' (Vector.cast w { toArray := l, size_toArray := ⋯ }) = Vector.cast ⋯ { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m k : Nat
l : Vector α n
w : n = m
w' : m = k
⊢ Vector.cast w' (Vector.cast w l) = Vector.cast ⋯ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m k : Nat
w' : m = k
l : Array α
w : l.size = m
⊢ Vector.cast w' (Vector.cast w { toArray := l, size_toArray := ⋯ }) = Vector.cast ⋯ { toArray := l, size_toArray := ⋯ }
-- Mathlib/Data/Matrix/Defs.lean
@[simp] lemma isAddUnit_iff [AddMonoid α] {A : Matrix m n α} :
    IsAddUnit A ↔ ∀ i j, IsAddUnit (A i j)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ IsAddUnit A ↔ ∀ (i : m) (j : n), IsAddUnit (A i j)

Tactic:
simp_rw [isAddUnit_iff_exists, Classical.skolem, forall_and,
  ← Matrix.ext_iff, add_apply, zero_apply]

Result:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, (∀ (i : m) (j : n), A i j + b i j = 0) ∧ ∀ (i : m) (j : n), b i j + A i j = 0) ↔
    ∃ f, (∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0) ∧ ∀ (x : m) (x_1 : n), f x x_1 + A x x_1 = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_yield_eq_foldl
    (l : List α) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (a : α) → a ∈ l → β → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f x.val ⋯ b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    foldl (fun b x => f x.val ⋯ b) init l'

Tactic:
induction l' generalizing init <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m b => ForInStep.yield (f a m b)) =
    foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f a h b)
      init l.attach

Tactic:
simp only [forIn'_eq_foldlM]

Result:
α : Type u_1
β : Type u_2
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f x.val ⋯ b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    foldl (fun b x => f x.val ⋯ b) init l.attach

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (a : α) → a ∈ l → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f x.val ⋯ b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    foldl (fun b x => f x.val ⋯ b) init l.attach

Tactic:
generalize l.attach = l'

Result:
α : Type u_1
β : Type u_2
l : List α
f : (a : α) → a ∈ l → β → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f x.val ⋯ b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    foldl (fun b x => f x.val ⋯ b) init l'
-- Mathlib/RingTheory/WittVector/MulP.lean
theorem mulN_isPoly (n : ℕ) : IsPoly p fun _ _Rcr x => x * n :=
  ⟨⟨wittMulN p n, fun R _Rcr x => by funext k; exact mulN_coeff n x k⟩⟩

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (x * ↑n).coeff = fun n_1 => (aeval x.coeff) (wittMulN p n n_1)

Tactic:
funext k

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)

Tactic:
exact mulN_coeff n x k

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
@[simp]
lemma inv_atBot₀ : (atBot : Filter 𝕜)⁻¹ = 𝓝[<] 0 :=
  (((atBot_basis_Iio' (0 : 𝕜)).map _).comp_surjective inv_surjective).eq_of_same_basis <|
    (nhdsLT_basis _).congr (by simp) fun a ha ↦ by simp [inv_Iio₀ (inv_neg''.2 ha)]

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
a : 𝕜
ha : a < 0
⊢ Ioo a 0 = ((fun i => Inv.inv '' Iio i) ∘ Inv.inv) a

Tactic:
simp [inv_Iio₀ (inv_neg''.2 ha)]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), i < 0 ↔ ((fun x => x < 0) ∘ Inv.inv) i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_succ (f : ℕ → Bool) :
    (fun n => cantorFunctionAux c f (n + 1)) = fun n =>
      c * cantorFunctionAux c (fun n => f (n + 1)) n

Proof state:
case h
c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n

Tactic:
cases h : f (n + 1) <;> simp [h, _root_.pow_succ']

Result:
no goals

Proof state:
c : ℝ
f : ℕ → Bool
⊢ (fun n => cantorFunctionAux c f (n + 1)) = fun n => c * cantorFunctionAux c (fun n => f (n + 1)) n

Tactic:
ext n

Result:
case h
c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
-- Mathlib/Data/List/Sort.lean
theorem sublist_orderedInsert (x : α) (xs : List α) : xs <+ xs.orderedInsert r x

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ takeWhile (fun b => decide ¬r x b) xs ++ x :: dropWhile (fun b => decide ¬r x b) xs

Tactic:
refine Sublist.trans ?_ (.append_left (.cons _ (.refl _)) _)

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ takeWhile (fun b => decide ¬r x b) xs ++ dropWhile (fun b => decide ¬r x b) xs

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ orderedInsert r x xs

Tactic:
rw [orderedInsert_eq_take_drop]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ takeWhile (fun b => decide ¬r x b) xs ++ x :: dropWhile (fun b => decide ¬r x b) xs

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
x : α
xs : List α
⊢ xs <+ takeWhile (fun b => decide ¬r x b) xs ++ dropWhile (fun b => decide ¬r x b) xs

Tactic:
rw [takeWhile_append_dropWhile]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem unpair₁ {n f} (hf : @Primrec' n f) : @Primrec' n fun v => (f v).unpair.1

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).1

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).1

Tactic:
refine (if_lt fss s fss s).of_eq fun v => ?_

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) = (unpair (f v)).1

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) = (unpair (f v)).1

Tactic:
simp [Nat.unpair]

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
v : List.Vector ℕ n
⊢ (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then f v - (f v).sqrt * (f v).sqrt else (f v).sqrt) =
    (if f v - (f v).sqrt * (f v).sqrt < (f v).sqrt then (f v - (f v).sqrt * (f v).sqrt, (f v).sqrt)
      else ((f v).sqrt, f v - (f v).sqrt * (f v).sqrt - (f v).sqrt)).1

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v => (unpair (f v)).1

Tactic:
have s := sqrt.comp₁ _ hf

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).1

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).1

Tactic:
have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)

Result:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
s : Primrec' fun v => (f v).sqrt
fss : Primrec' fun v => f v - (f v).sqrt * (f v).sqrt
⊢ Primrec' fun v => (unpair (f v)).1
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Infinite.exists_ne_map_eq_of_mapsTo {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite)
    (hf : MapsTo f s t) (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Proof state:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ ¬t.Finite

Tactic:
exact infinite_of_injOn_mapsTo (fun x hx y hy => not_imp_not.1 (ht x hx y hy)) hf hs

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
contrapose! ht

Result:
α : Type u
β : Type v
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ ¬t.Finite
-- Mathlib/Analysis/Analytic/CPolynomial.lean
lemma cpolynomialAt_uncurry_of_multilinear :
    CPolynomialAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x :=
  f.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear.cPolynomialAt_of_mem
    (by simp only [Metric.emetric_ball_top, Set.mem_univ])

Proof state:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
x : G × ((i : ι) → Em i)
⊢ x ∈ EMetric.ball 0 ⊤

Tactic:
simp only [Metric.emetric_ball_top, Set.mem_univ]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem nat_sub_iff : LiouvilleWith p (n - x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
lemma SubRootedTree.root_ne_bot_of_mem_subtrees (r : SubRootedTree t) (hr : r ∈ t.subtrees) :
    r.root ≠ ⊥

Proof state:
t : RootedTree
r : SubRootedTree t
hr : r ∈ t.subtrees
⊢ r.root ≠ ⊥

Tactic:
simp only [RootedTree.subtrees, Set.mem_setOf_eq] at hr

Result:
t : RootedTree
r : SubRootedTree t
hr : IsAtom r.root
⊢ r.root ≠ ⊥

Proof state:
t : RootedTree
r : SubRootedTree t
hr : IsAtom r.root
⊢ r.root ≠ ⊥

Tactic:
exact hr.1

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg {x y : ℝ*} :
    InfiniteNeg x → ¬Infinitesimal y → y < 0 → InfinitePos (x * y)

Proof state:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos

Tactic:
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos

Result:
no goals

Proof state:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos

Tactic:
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]

Result:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).Infinitesimal → 0 < -y → (-x * -y).InfinitePos
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn'_map [Monad m] [LawfulMonad m]
    (l : Array α) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
g : α → β
f : (b : β) → b ∈ map g l → γ → m (ForInStep γ)
⊢ forIn' (map g l) init f = forIn' l init fun a h y => f (g a) ⋯ y

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
toList✝ : List α
f : (b : β) → b ∈ map g { toList := toList✝ } → γ → m (ForInStep γ)
⊢ forIn' (map g { toList := toList✝ }) init f = forIn' { toList := toList✝ } init fun a h y => f (g a) ⋯ y

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
toList✝ : List α
f : (b : β) → b ∈ map g { toList := toList✝ } → γ → m (ForInStep γ)
⊢ forIn' (map g { toList := toList✝ }) init f = forIn' { toList := toList✝ } init fun a h y => f (g a) ⋯ y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivAt.le_of_lipschitzOn
    {f : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf : HasFDerivAt f f' x₀)
    {s : Set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖f'‖ ≤ C

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
refine hf.le_of_lip' C.coe_nonneg ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem filter_apply_eq_zero_of_not_mem {a : α} (ha : a ∉ s) : (p.filter s h) a = 0

Proof state:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
⊢ (p.filter s h) a = 0

Tactic:
rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem incidence_other_prop {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v) :
    G.otherVertexOfIncident h ∈ G.neighborSet v

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ G.neighborSet v

Tactic:
obtain ⟨he, hv⟩ := h

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
he : e ∈ G.edgeSet
hv : v ∈ e
⊢ G.otherVertexOfIncident ⋯ ∈ G.neighborSet v

Tactic:
rwa [← Sym2.other_spec' hv, mem_edgeSet] at he

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem counitInv_app_functor (e : C ≌ D) (X : C) :
    e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.functor.map (e.unit.app X) = e.counitInv.app (e.functor.obj X)

Tactic:
erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)

Tactic:
symm

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.functor.map (e.unit.app X) = e.counitInv.app (e.functor.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 ((𝟭 D).obj (e.functor.toPrefunctor.1 ((𝟭 C).obj X)))

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem has_iUnion {β} [Countable β] {f : β → Set α} (hd : Pairwise (Disjoint on f))
    (h : ∀ i, d.Has (f i)) : d.Has (⋃ i, f i)

Proof state:
case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)

Tactic:
exact
  d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n =>
    Encodable.iUnion_decode₂_cases d.has_empty h

Result:
no goals

Proof state:
case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, f i)

Tactic:
rw [← Encodable.iUnion_decode₂]

Result:
case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, ⋃ b ∈ Encodable.decode₂ β i, f b)

Proof state:
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
⊢ d.Has (⋃ i, f i)

Tactic:
cases nonempty_encodable β

Result:
case intro
α : Type u_3
d : DynkinSystem α
β : Type u_4
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), d.Has (f i)
val✝ : Encodable β
⊢ d.Has (⋃ i, f i)
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_one : eval f a 1 = 1

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
⊢ eval f a 1 = 1

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Logic/Equiv/List.lean
theorem decode_list_succ (v : ℕ) :
    decode (α := List α) (succ v) =
      (· :: ·) <$> decode (α := α) v.unpair.1 <*> decode (α := List α) v.unpair.2 :=
  show decodeList (succ v) = _ by
    rcases e : unpair v with ⟨v₁, v₂⟩
    simp [decodeList, e]; rfl

Proof state:
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Option.map (fun x1 x2 => x1 :: x2) (decode v₁) <*> decodeList v₂ =
    Option.map (fun x1 x2 => x1 :: x2) (decode v₁) <*> decode v₂

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = (fun x1 x2 => x1 :: x2) <$> decode (v₁, v₂).1 <*> decode (v₁, v₂).2

Tactic:
simp [decodeList, e]

Result:
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Option.map (fun x1 x2 => x1 :: x2) (decode v₁) <*> decodeList v₂ =
    Option.map (fun x1 x2 => x1 :: x2) (decode v₁) <*> decode v₂

Proof state:
α : Type u_1
inst✝ : Encodable α
v : ℕ
⊢ decodeList v.succ = (fun x1 x2 => x1 :: x2) <$> decode (unpair v).1 <*> decode (unpair v).2

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Result:
case mk
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = (fun x1 x2 => x1 :: x2) <$> decode (v₁, v₂).1 <*> decode (v₁, v₂).2
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem isClosed_upperClosure (h : s.Finite) : IsClosed (upperClosure s : Set α)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed ↑(upperClosure s)

Tactic:
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed (⋃ i ∈ s, ↑(UpperSet.Ici i))

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed (⋃ i ∈ s, ↑(UpperSet.Ici i))

Tactic:
exact h.isClosed_biUnion fun _ _ => isClosed_Ici

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_self_sub_left {m n : ℕ} (h : m ≤ n) : gcd (n - m) n = gcd m n

Proof state:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m).gcd (m + (n - m)) = (n - m).gcd m

Tactic:
rw [gcd_add_self_right, gcd_comm]

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m).gcd n = (n - m).gcd m

Tactic:
nth_rw 2 [← Nat.add_sub_cancel' h]

Result:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m).gcd (m + (n - m)) = (n - m).gcd m

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd n = m.gcd n

Tactic:
have := Nat.sub_add_cancel h

Result:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m).gcd n = m.gcd n

Proof state:
m n : ℕ
h : m ≤ n
this✝ : n - m + m = n
this : (n - m).gcd n = (n - m).gcd m
⊢ (n - m + m - m).gcd (n - m + m) = (n - m).gcd m

Tactic:
convert this

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m + m - m).gcd (n - m + m) = (n - m).gcd m

Tactic:
have : gcd (n - m) n = gcd (n - m) m := by
  nth_rw 2 [← Nat.add_sub_cancel' h]
  rw [gcd_add_self_right, gcd_comm]

Result:
m n : ℕ
h : m ≤ n
this✝ : n - m + m = n
this : (n - m).gcd n = (n - m).gcd m
⊢ (n - m + m - m).gcd (n - m + m) = (n - m).gcd m

Proof state:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m).gcd n = m.gcd n

Tactic:
rw [gcd_comm m n, ← this, gcd_add_self_left (n - m) m]

Result:
m n : ℕ
h : m ≤ n
this : n - m + m = n
⊢ (n - m + m - m).gcd (n - m + m) = (n - m).gcd m