harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a

Proof state:
case intro.h
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
x : α
h✝ : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α), r y x → Acc q y
y : α
h : q y x
⊢ Acc q y

Tactic:
exact ih y (h₁ h)

Result:
no goals

Proof state:
case intro
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
x : α
h✝ : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α), r y x → Acc q y
⊢ Acc q x

Tactic:
apply Acc.intro

Result:
case intro.h
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
x : α
h✝ : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α), r y x → Acc q y
⊢ ∀ (y : α), q y x → Acc q y

Proof state:
case intro.h
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
x : α
h✝ : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α), r y x → Acc q y
⊢ ∀ (y : α), q y x → Acc q y

Tactic:
intro y h

Result:
case intro.h
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
x : α
h✝ : ∀ (y : α), r y x → Acc r y
ih : ∀ (y : α), r y x → Acc q y
y : α
h : q y x
⊢ Acc q y

Proof state:
α : Sort u
r q : α → α → Prop
a : α
h₁ : Subrelation q r
ac : Acc r a
⊢ Acc q a

Tactic:
induction ac with
| intro x _ ih =>
  apply Acc.intro
  intro y h
  exact ih y (h₁ h)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
    (M * (listTransvecRow M).prod) (inr unit) (inl i) = 0

Proof state:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have hnr : n < r := hk

Result:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
-- Mathlib/Analysis/Normed/Field/Ultra.lean
lemma isUltrametricDist_of_forall_norm_add_one_of_norm_le_one
    (h : ∀ x : R, ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1) : IsUltrametricDist R

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ 0 < ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x + 1‖ ≤ 1

Tactic:
apply h

Result:
case inr.a
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x‖ ≤ 1

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ ‖x‖

Tactic:
rw [← div_le_one (by positivity), ← norm_div, add_div,
  div_self (by simpa using H.trans' zero_lt_one), add_comm]

Result:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x + 1‖ ≤ 1

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ x ≠ 0

Tactic:
simpa using H.trans' zero_lt_one

Result:
no goals

Proof state:
case inr.a
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x‖ ≤ 1

Tactic:
simp [inv_le_one_iff₀, H.le]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Tactic:
exact (h _ H).trans (le_max_right _ _)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_one_le_max_norm_one fun x ↦ ?_

Result:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Proof state:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Tactic:
rcases le_or_lt ‖x‖ 1 with H|H

Result:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Proof state:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Tactic:
suffices ‖x + 1‖ ≤ ‖x‖ from this.trans (le_max_left _ _)

Result:
case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ ‖x‖
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_mul {I I' : FractionalIdeal R⁰ K} (hI : I ≠ 0) (hI' : I' ≠ 0) :
    count K v (I * I') = count K v I + count K v I'

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
rw [haJ, haJ', mul_assoc, mul_comm (J : FractionalIdeal R⁰ K), mul_assoc, ← mul_assoc,
  spanSingleton_mul_spanSingleton, coeIdeal_mul, RingHom.map_mul, mul_inv,
  mul_comm (J : FractionalIdeal R⁰ K)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) :
    (L.findSome? fun l => l[0]?).isSome

Proof state:
α : Type u_1
xss✝ : List (List α)
xs : List α
m : xs ∈ xss✝
h : 0 < xs.length
⊢ 0 < xs.length

Tactic:
simpa using h

Result:
no goals

Proof state:
case of.intro.intro.intro.intro
α : Type u_1
xss✝ : List (List α)
xs : List α
m : xs ∈ xss✝
h : 0 < xs.length
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length

Tactic:
exact ⟨xs, m, by simpa using h⟩

Result:
no goals

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
h : ∃ x, (∃ a, a ∈ xss✝ ∧ a.length = x) ∧ 0 < x
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length

Tactic:
obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h

Result:
case of.intro.intro.intro.intro
α : Type u_1
xss✝ : List (List α)
xs : List α
m : xs ∈ xss✝
h : 0 < xs.length
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
h : 0 < (List.map List.toArray xss✝).toArray.flatten.size
⊢ (findSome? (fun l => l[0]?) (List.map List.toArray xss✝).toArray).isSome = true

Tactic:
simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
  List.findSome?_isSome_iff, isSome_getElem?]

Result:
case of
α : Type u_1
xss✝ : List (List α)
h : 0 < (List.map List.toArray xss✝).toArray.flatten.size
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length

Proof state:
α : Type u_1
L : Array (Array α)
h : 0 < L.flatten.size
⊢ (findSome? (fun l => l[0]?) L).isSome = true

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
h : 0 < (List.map List.toArray xss✝).toArray.flatten.size
⊢ (findSome? (fun l => l[0]?) (List.map List.toArray xss✝).toArray).isSome = true

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
h : 0 < (List.map List.toArray xss✝).toArray.flatten.size
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length

Tactic:
simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
  Nat.sum_pos_iff_exists_pos, List.mem_map] at h

Result:
case of
α : Type u_1
xss✝ : List (List α)
h : ∃ x, (∃ a, a ∈ xss✝ ∧ a.length = x) ∧ 0 < x
⊢ ∃ x, x ∈ xss✝ ∧ 0 < x.length
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem hasFDerivWithinAt_iff_hasGradientWithinAt {frechet : F →L[𝕜] 𝕜} {s : Set F} :
    HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((toDual 𝕜 F).symm frechet) s x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
frechet : F →L[𝕜] 𝕜
s : Set F
⊢ HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((toDual 𝕜 F).symm frechet) s x

Tactic:
rw [hasGradientWithinAt_iff_hasFDerivWithinAt, (toDual 𝕜 F).apply_symm_apply frechet]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem nndist_self_conj (z : ℂ) : nndist z (conj z) = 2 * Real.nnabs z.im

Proof state:
z : ℂ
⊢ nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im

Tactic:
rw [nndist_comm, nndist_conj_self]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma inf_imp_right (φ ψ : L.BoundedFormula α n) : φ ⊓ ψ ⟹[T] ψ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact And.right

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs

Tactic:
exact And.right

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ψ ⟹ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs
-- Mathlib/SetTheory/Cardinal/CountableCover.lean
/-- If a space is eventually covered by a countable family of sets, all with cardinality at
most `a`, then the cardinality of the space is also bounded by `a`. -/
lemma mk_le_of_countable_eventually_mem {α : Type u} {ι : Type v} {a : Cardinal}
    [Countable ι] {f : ι → Set α} {l : Filter ι} [NeBot l] (ht : ∀ x, ∀ᶠ i in l, x ∈ f i)
    (h'f : ∀ i, #(f i) ≤ a) : #α ≤ a

Proof state:
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑Set.univ ≤ a

Tactic:
exact mk_subtype_le_of_countable_eventually_mem (l := l) (fun x _ ↦ ht x) h'f

Result:
no goals

Proof state:
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #α ≤ a

Tactic:
rw [← mk_univ]

Result:
α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑Set.univ ≤ a
-- Mathlib/Data/Nat/Factorial/BigOperators.lean
/-- `k!` divides the product of any `k` consecutive integers. -/
lemma factorial_coe_dvd_prod (k : ℕ) (n : ℤ) : (k ! : ℤ) ∣ ∏ i ∈ range k, (n + i)

Proof state:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
have hdivk := x.factorial_dvd_ascFactorial k

Result:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : k ! ∣ x.ascFactorial k
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Proof state:
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
obtain ⟨x, hx⟩ := Int.eq_ofNat_of_zero_le hn

Result:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Proof state:
k : ℕ
n : ℤ
⊢ ↑k ! ∣ ∏ i ∈ range k, (n + ↑i)

Tactic:
rw [Int.dvd_iff_emod_eq_zero, Finset.prod_int_mod]

Result:
k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0

Proof state:
k : ℕ
n : ℤ
⊢ (∏ i ∈ range k, (n + ↑i) % ↑k !) % ↑k ! = 0

Tactic:
simp_rw [← Int.emod_add_emod n]

Result:
k : ℕ
n : ℤ
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Proof state:
k : ℕ
n : ℤ
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
have hn : 0 ≤ n % k ! := Int.emod_nonneg n <| Int.natCast_ne_zero.mpr k.factorial_ne_zero

Result:
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Proof state:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
rwa [← Finset.prod_int_mod, ← Int.dvd_iff_emod_eq_zero, hx]

Result:
no goals

Proof state:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : k ! ∣ x.ascFactorial k
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0

Tactic:
zify [x.ascFactorial_eq_prod_range k] at hdivk

Result:
case intro
k : ℕ
n : ℤ
hn : 0 ≤ n % ↑k !
x : ℕ
hx : n % ↑k ! = ↑x
hdivk : ↑k ! ∣ ∏ x_1 ∈ range k, (↑x + ↑x_1)
⊢ (∏ x ∈ range k, (n % ↑k ! + ↑x) % ↑k !) % ↑k ! = 0
-- Mathlib/Data/Bool/Basic.lean
theorem false_eq_true_eq_False : ¬false = true

Proof state:
⊢ ¬false = true

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
lemma finite_hasEigenvalue : Set.Finite f.HasEigenvalue

Proof state:
case h.e'_2
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
⊢ f.HasEigenvalue = (minpoly K f).rootSet K

Tactic:
ext μ

Result:
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ μ ∈ f.HasEigenvalue ↔ μ ∈ (minpoly K f).rootSet K

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
⊢ Set.Finite f.HasEigenvalue

Tactic:
have h : minpoly K f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := K) f)

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
⊢ Set.Finite f.HasEigenvalue

Proof state:
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ f.HasEigenvalue μ ↔ μ ∈ (minpoly K f).rootSet K

Tactic:
rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
⊢ Set.Finite f.HasEigenvalue

Tactic:
convert (minpoly K f).rootSet_finite K

Result:
case h.e'_2
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
⊢ f.HasEigenvalue = (minpoly K f).rootSet K

Proof state:
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ μ ∈ f.HasEigenvalue ↔ μ ∈ (minpoly K f).rootSet K

Tactic:
change f.HasEigenvalue μ ↔ _

Result:
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ f.HasEigenvalue μ ↔ μ ∈ (minpoly K f).rootSet K
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma zeroLocus_map_of_eq {U V : X.Opens} (i : U = V) (s : Set Γ(X, V)) :
    X.zeroLocus ((X.presheaf.map (eqToHom i).op).hom '' s) = X.zeroLocus s

Proof state:
X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) = X.zeroLocus s

Tactic:
ext

Result:
case h
X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) ↔ x✝ ∈ X.zeroLocus s

Proof state:
case h
X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) ↔ x✝ ∈ X.zeroLocus s

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem insertRight_insertLeft {x x' x'' : PGame} :
    insertRight (insertLeft x x') x'' = insertLeft (insertRight x x'') x'

Proof state:
case mk.mk.mk
α✝² β✝² : Type u_1
a✝⁵ : α✝² → PGame
a✝⁴ : β✝² → PGame
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝² β✝² a✝⁵ a✝⁴).insertLeft (mk α✝¹ β✝¹ a✝³ a✝²)).insertRight (mk α✝ β✝ a✝¹ a✝) =
    ((mk α✝² β✝² a✝⁵ a✝⁴).insertRight (mk α✝ β✝ a✝¹ a✝)).insertLeft (mk α✝¹ β✝¹ a✝³ a✝²)

Tactic:
dsimp [insertLeft, insertRight]

Result:
no goals

Proof state:
case mk.mk
x'' : PGame
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝¹ β✝¹ a✝³ a✝²).insertLeft (mk α✝ β✝ a✝¹ a✝)).insertRight x'' =
    ((mk α✝¹ β✝¹ a✝³ a✝²).insertRight x'').insertLeft (mk α✝ β✝ a✝¹ a✝)

Tactic:
cases x''

Result:
case mk.mk.mk
α✝² β✝² : Type u_1
a✝⁵ : α✝² → PGame
a✝⁴ : β✝² → PGame
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝² β✝² a✝⁵ a✝⁴).insertLeft (mk α✝¹ β✝¹ a✝³ a✝²)).insertRight (mk α✝ β✝ a✝¹ a✝) =
    ((mk α✝² β✝² a✝⁵ a✝⁴).insertRight (mk α✝ β✝ a✝¹ a✝)).insertLeft (mk α✝¹ β✝¹ a✝³ a✝²)

Proof state:
case mk
x' x'' : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝ β✝ a✝¹ a✝).insertLeft x').insertRight x'' = ((mk α✝ β✝ a✝¹ a✝).insertRight x'').insertLeft x'

Tactic:
cases x'

Result:
case mk.mk
x'' : PGame
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝¹ β✝¹ a✝³ a✝²).insertLeft (mk α✝ β✝ a✝¹ a✝)).insertRight x'' =
    ((mk α✝¹ β✝¹ a✝³ a✝²).insertRight x'').insertLeft (mk α✝ β✝ a✝¹ a✝)

Proof state:
x x' x'' : PGame
⊢ (x.insertLeft x').insertRight x'' = (x.insertRight x'').insertLeft x'

Tactic:
cases x

Result:
case mk
x' x'' : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ ((mk α✝ β✝ a✝¹ a✝).insertLeft x').insertRight x'' = ((mk α✝ β✝ a✝¹ a✝).insertRight x'').insertLeft x'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_snd_zip (l₁ : Array α) (l₂ : Array β) (h : l₂.size ≤ l₁.size) :
    map Prod.snd (zip l₁ l₂) = l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝ }.size ≤ { toList := toList✝¹ }.size
⊢ map Prod.snd ({ toList := toList✝¹ }.zip { toList := toList✝ }) = { toList := toList✝ }

Tactic:
simp_all [List.map_snd_zip]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : l₂.size ≤ { toList := toList✝ }.size
⊢ map Prod.snd ({ toList := toList✝ }.zip l₂) = l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝ }.size ≤ { toList := toList✝¹ }.size
⊢ map Prod.snd ({ toList := toList✝¹ }.zip { toList := toList✝ }) = { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size ≤ l₁.size
⊢ map Prod.snd (l₁.zip l₂) = l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : l₂.size ≤ { toList := toList✝ }.size
⊢ map Prod.snd ({ toList := toList✝ }.zip l₂) = l₂
-- Mathlib/FieldTheory/Separable.lean
theorem nodup_roots {p : R[X]} (hsep : Separable p) : p.roots.Nodup

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
classical
exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra.lean
theorem continuous_algebraMap_iff_smul [IsTopologicalSemiring A] :
    Continuous (algebraMap R A) ↔ Continuous fun p : R × A => p.1 • p.2

Proof state:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalSemiring A
h : Continuous ⇑(algebraMap R A)
⊢ Continuous fun p => p.1 • p.2

Tactic:
simp only [Algebra.smul_def]

Result:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalSemiring A
h : Continuous ⇑(algebraMap R A)
⊢ Continuous fun p => (algebraMap R A) p.1 * p.2

Proof state:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalSemiring A
⊢ Continuous ⇑(algebraMap R A) ↔ Continuous fun p => p.1 • p.2

Tactic:
refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩

Result:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalSemiring A
h : Continuous ⇑(algebraMap R A)
⊢ Continuous fun p => p.1 • p.2

Proof state:
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalSemiring A
h : Continuous ⇑(algebraMap R A)
⊢ Continuous fun p => (algebraMap R A) p.1 * p.2

Tactic:
exact (h.comp continuous_fst).mul continuous_snd

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem zero_powerlt {a : Cardinal} (h : a ≠ 0) : 0 ^< a = 1

Proof state:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.277419 ^ 0 ≤ 0 ^< a

a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}

Tactic:
exact le_powerlt 0 (pos_iff_ne_zero.2 h)

Result:
no goals

Proof state:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1

Tactic:
apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm

Result:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 1 ≤ 0 ^< a

Proof state:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ 1 ≤ 0 ^< a

Tactic:
rw [← power_zero]

Result:
a : Cardinal.{u_1}
h : a ≠ 0
⊢ ?m.277419 ^ 0 ≤ 0 ^< a

a : Cardinal.{u_1}
h : a ≠ 0
⊢ Cardinal.{u_1}
-- Mathlib/Analysis/Convex/Basic.lean
theorem single_mem_stdSimplex (i : ι) : Pi.single i 1 ∈ stdSimplex 𝕜 ι :=
  ⟨le_update_iff.2 ⟨zero_le_one, fun _ _ ↦ le_rfl⟩, by simp⟩

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ ∑ x : ι, Pi.single i 1 x = 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem isLimitEquivSections_symm_apply {c : Cone F} (t : IsLimit c)
    (x : F.sections) (j : J) :
    c.π.app j ((isLimitEquivSections t).symm x) = (x : ∀ j, F.obj j) j

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ c.π.app j ((isLimitEquivSections t).symm x) = ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j

Tactic:
rfl

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ c.π.app j ((isLimitEquivSections t).symm x) = ↑x j

Tactic:
conv_rhs => rw [← (isLimitEquivSections t).right_inv x]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ c.π.app j ((isLimitEquivSections t).symm x) = ↑((isLimitEquivSections t).toFun ((isLimitEquivSections t).invFun x)) j