harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem digits_succ (b n m r l) (e : r + b * m = n) (hr : r < b)
    (h : Nat.digits b m = l ∧ 1 < b ∧ 0 < m) : (Nat.digits b n = r :: l) ∧ 1 < b ∧ 0 < n

Proof state:
case intro.intro.intro
b n : ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
exact Nat.digits_def' b2 n0

Result:
no goals

Proof state:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Tactic:
have n0 : 0 < n := by linarith [mul_pos b0 m0]

Result:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Proof state:
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
⊢ 0 < b

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Tactic:
have b0 : 0 < b := by omega

Result:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Proof state:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ b.digits n = r :: l

Tactic:
obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩

Result:
case intro.intro.intro
b n : ℕ
l : List ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
h : b.digits (n / b) = l
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ b.digits n = n % b :: l

Proof state:
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
⊢ 0 < n

Tactic:
linarith [mul_pos b0 m0]

Result:
no goals

Proof state:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Tactic:
refine ⟨?_, b2, n0⟩

Result:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
b0 : 0 < b
n0 : 0 < n
⊢ b.digits n = r :: l

Proof state:
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l ∧ 1 < b ∧ 0 < m
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Tactic:
rcases h with ⟨h, b2, m0⟩

Result:
case intro.intro
b n m r : ℕ
l : List ℕ
e : r + b * m = n
hr : r < b
h : b.digits m = l
b2 : 1 < b
m0 : 0 < m
⊢ b.digits n = r :: l ∧ 1 < b ∧ 0 < n

Proof state:
case intro.intro.intro
b n : ℕ
l : List ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
h : b.digits (n / b) = l
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ b.digits n = n % b :: l

Tactic:
subst h

Result:
case intro.intro.intro
b n : ℕ
b2 : 1 < b
b0 : 0 < b
n0 : 0 < n
m0 : 0 < n / b
hr : n % b < b
e : n % b + b * (n / b) = n
⊢ b.digits n = n % b :: b.digits (n / b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSomeRev?_push_of_isSome (l : Vector α n) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f : α → Option α✝
a : α
l : Vector α n
h : (f a).isSome = true
⊢ findSomeRev? f (l.push a) = f a

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isSome = true
l : Array α
⊢ findSomeRev? f ({ toArray := l, size_toArray := ⋯ }.push a) = f a

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
a : α
h : (f a).isSome = true
l : Array α
⊢ findSomeRev? f ({ toArray := l, size_toArray := ⋯ }.push a) = f a

Tactic:
simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isSome, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_iff_forall_isSome_getEntry? [BEq α] [ReflBEq α] :
    {l : List ((a : α) × β a)} → l.isEmpty ↔ ∀ a, (getEntry? a l).isSome = false
  | [] => by simp
  | (⟨k, v⟩::l) => ⟨by simp, fun h => have := h k; by simp at this⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : ∀ (a : α), (getEntry? a (⟨k, v⟩ :: l)).isSome = false
this : (getEntry? k (⟨k, v⟩ :: l)).isSome = false
⊢ (⟨k, v⟩ :: l).isEmpty = true

Tactic:
simp at this

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
⊢ [].isEmpty = true ↔ ∀ (a : α), (getEntry? a []).isSome = false

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
k : α
v : β k
l : List ((a : α) × β a)
⊢ (⟨k, v⟩ :: l).isEmpty = true → ∀ (a : α), (getEntry? a (⟨k, v⟩ :: l)).isSome = false

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem IsComplete.union {s t : Set α} (hs : IsComplete s) (ht : IsComplete t) :
    IsComplete (s ∪ t)

Proof state:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : IsComplete s
ht : IsComplete t
⊢ IsComplete (s ∪ t)

Tactic:
simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *

Result:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x ∈ t, ↑l ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x)

Proof state:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x ∈ t, ↑l ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x)

Tactic:
exact fun l hl =>
  ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
    (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem sum_sq_le_of_mem_box (hx : x ∈ box n d) : ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Proof state:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
  Nat.pow_le_pow_left (Nat.le_sub_one_of_lt (hx i)) _

Result:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Proof state:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [card_fin, smul_eq_mul])

Result:
no goals

Proof state:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
rw [mem_box] at hx

Result:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2

Proof state:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ #univ • (d - 1) ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
rw [card_fin, smul_eq_mul]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem bind₁_frobeniusPolyRat_wittPolynomial (n : ℕ) :
    bind₁ (frobeniusPolyRat p) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ (frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)

Tactic:
delta frobeniusPolyRat

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ fun n => (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)) (wittPolynomial p ℚ n) =
    wittPolynomial p ℚ (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ fun n => (bind₁ (wittPolynomial p ℚ ∘ fun n => n + 1)) (xInTermsOfW p ℚ n)) (wittPolynomial p ℚ n) =
    wittPolynomial p ℚ (n + 1)

Tactic:
rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]

Result:
no goals
-- Mathlib/Algebra/CharZero/Quotient.lean
theorem nsmul_mem_zmultiples_iff_exists_sub_div {r : R} {n : ℕ} (hn : n ≠ 0) :
    n • r ∈ AddSubgroup.zmultiples p ↔
      ∃ k : Fin n, r - (k : ℕ) • (p / n : R) ∈ AddSubgroup.zmultiples p

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
  Int.cast_natCast]

Result:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ (∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p) ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b

Proof state:
n : Nat
α✝ : Type u_1
a b : α✝
⊢ mkVector n a = mkVector n b ↔ n = 0 ∨ a = b

Tactic:
simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma _root_.Real.spectralRadius_mem_spectrum_or {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
    [CompleteSpace A] {a : A} (ha : (spectrum ℝ a).Nonempty) :
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Proof state:
case intro.intro
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs]

Result:
case intro.intro
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a

Proof state:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
h : |x| = -x
⊢ -|x| ∈ spectrum ℝ a

Tactic:
simpa [h]

Result:
no goals

Proof state:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
h : |x| = x
⊢ |x| ∈ spectrum ℝ a

Tactic:
rwa [h]

Result:
no goals

Proof state:
case intro.intro
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a

Tactic:
exact abs_choice x |>.imp (fun h ↦ by rwa [h]) (fun h ↦ by simpa [h])

Result:
no goals

Proof state:
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha

Result:
case intro.intro
A : Type u_4
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : ↑‖x‖₊ = spectralRadius ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem pointwise_smul_toAddSubGroup {R : Type*} [Ring R] [MulSemiringAction M R]
    (a : M) (S : Ideal R) (ha : Function.Surjective fun r : R => a • r)  :
    (a • S).toAddSubgroup = a • S.toAddSubgroup

Proof state:
M : Type u_1
inst✝² : Monoid M
R : Type u_3
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
⊢ Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S

Tactic:
ext

Result:
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_3
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ x✝ ∈ Submodule.toAddSubgroup (a • S) ↔ x✝ ∈ a • Submodule.toAddSubgroup S

Proof state:
M : Type u_1
inst✝² : Monoid M
R : Type u_3
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
exact ha

Result:
no goals

Proof state:
case h
M : Type u_1
inst✝² : Monoid M
R : Type u_3
inst✝¹ : Ring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ x✝ ∈ Submodule.toAddSubgroup (a • S) ↔ x✝ ∈ a • Submodule.toAddSubgroup S

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem CG.map_of_surjective {N : Type*} [L.Structure N] (h : CG L M) (f : M →[L] N)
    (hs : Function.Surjective f) : CG L N

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : Function.Surjective ⇑f
⊢ CG L N

Tactic:
rw [← Hom.range_eq_top] at hs

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ CG L N

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG

Tactic:
exact h.range f

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ CG L N

Tactic:
rw [cg_def, ← hs]

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma norm_fourierSMulRight (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) :
    ‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ ‖fourierSMulRight L f v‖ = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
  norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
  Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_reverse {p : α → Prop} {l : Vector { x // p x } n} :
    l.reverse.unattach = l.unattach.reverse

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector { x // p x } n
⊢ l.reverse.unattach = l.unattach.reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ { toArray := l, size_toArray := ⋯ }.reverse.unattach = { toArray := l, size_toArray := ⋯ }.unattach.reverse

Proof state:
case mk
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ { toArray := l, size_toArray := ⋯ }.reverse.unattach = { toArray := l, size_toArray := ⋯ }.unattach.reverse

Tactic:
simp [Array.unattach_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
  (range_loop_range' n 0).trans <| by rw [Nat.zero_add]

Proof state:
n : Nat
⊢ range' 0 (0 + n) = range' 0 n

Tactic:
rw [Nat.zero_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem cardinal_lift_le_rank {ι : Type w} {v : ι → M}
    (hv : LinearIndependent R v) :
    Cardinal.lift.{v} #ι ≤ Cardinal.lift.{w} (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} #↑↑⟨range v, ⋯⟩

Tactic:
exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ ι, #↑↑ι)

Tactic:
refine le_trans ?_ (lift_le.mpr <| le_ciSup (bddAbove_range _) ⟨_, hv.linearIndepOn_id⟩)

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} #↑↑⟨range v, ⋯⟩

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
rw [Module.rank]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (⨆ ι, #↑↑ι)
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem det_toBlock (M : Matrix m m R) (p : m → Prop) [DecidablePred p] :
    M.det =
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p) <|
          toBlock M (fun j => ¬p j) fun j => ¬p j).det

Proof state:
case e_f.h.e_a.e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x y : { a // p a } ⊕ { a // ¬p a }
hy : σ x = y
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y x =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) y x

Tactic:
cases x <;> cases y <;>
  simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr,
    Equiv.sumCompl_apply_inl, fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁,
    fromBlocks_apply₂₂, Matrix.submatrix_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem subtypePerm_on_cycleFactorsFinset [DecidableEq α] [Fintype α]
    {g c : Perm α} (hc : c ∈ g.cycleFactorsFinset) :
    g.subtypePerm (mem_cycleFactorsFinset_support hc) = c.subtypePermOfSupport

Proof state:
case H.mk.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ ↑((g.subtypePerm ⋯) ⟨x, hx⟩) = ↑(c.subtypePermOfSupport ⟨x, hx⟩)

Tactic:
simp only [subtypePerm_apply, Subtype.coe_mk, subtypePermOfSupport]

Result:
case H.mk.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g x = c x

Proof state:
case H.mk.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ g x = c x

Tactic:
exact ((mem_cycleFactorsFinset_iff.mp hc).2 x hx).symm

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.subtypePerm ⋯ = c.subtypePermOfSupport

Tactic:
ext ⟨x, hx⟩

Result:
case H.mk.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
x : α
hx : x ∈ c.support
⊢ ↑((g.subtypePerm ⋯) ⟨x, hx⟩) = ↑(c.subtypePermOfSupport ⟨x, hx⟩)
-- Mathlib/Data/Sigma/Lex.lean
theorem Lex.mono {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : ∀ i, α i → α i → Prop}
    (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ i a b, s₁ i a b → s₂ i a b) {a b : Σ' i, α i}
    (h : Lex r₁ s₁ a b) : Lex r₂ s₂ a b

Proof state:
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a b : (i : ι) ×' α i
h : Lex r₁ s₁ a b
⊢ Lex r₂ s₂ a b

Tactic:
obtain ⟨a, b, hij⟩ | ⟨i, hab⟩ := h

Result:
case left
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ ⟨a₁✝, a⟩ ⟨a₂✝, b⟩

case right
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ ⟨i, b₁✝⟩ ⟨i, b₂✝⟩

Proof state:
case right
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i : ι
b₁✝ b₂✝ : α i
hab : s₁ i b₁✝ b₂✝
⊢ Lex r₂ s₂ ⟨i, b₁✝⟩ ⟨i, b₂✝⟩

Tactic:
exact Lex.right _ (hs _ _ _ hab)

Result:
no goals

Proof state:
case left
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ ⟨a₁✝, a⟩ ⟨a₂✝, b⟩

Tactic:
exact Lex.left _ _ (hr _ _ hij)

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_two : primeFactorsList 2 = [2]

Proof state:
⊢ primeFactorsList 2 = [2]

Tactic:
simp [primeFactorsList]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp] lemma nnnorm_eq (x : ℝ≥0) : ‖(x : ℝ)‖₊ = x

Proof state:
case a
x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x

Tactic:
simp [nnnorm]

Result:
no goals

Proof state:
x : ℝ≥0
⊢ ‖↑x‖₊ = x

Tactic:
ext

Result:
case a
x : ℝ≥0
⊢ ↑‖↑x‖₊ = ↑x
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem isCoatom_map_of_ker_le {f : F} (hf : Surjective f) {p : Submodule R M}
    (le : LinearMap.ker f ≤ p) (hp : IsCoatom p) : IsCoatom (map f p) :=
  (isCoatom_comap_iff hf).mp <| by rwa [comap_map_eq_self le]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Surjective ⇑f
p : Submodule R M
le : LinearMap.ker f ≤ p
hp : IsCoatom p
⊢ IsCoatom (comap f (map f p))

Tactic:
rwa [comap_map_eq_self le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_concat (as : List α) (a : α) : (concat as a).length = as.length + 1

Proof state:
case nil
α : Type u
a : α
⊢ (nil.concat a).length = nil.length + 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
as : List α
a : α
⊢ (as.concat a).length = as.length + 1

Tactic:
induction as with
| nil => rfl
| cons _ xs ih => simp [concat, ih]

Result:
no goals

Proof state:
case cons
α : Type u
a head✝ : α
xs : List α
ih : (xs.concat a).length = xs.length + 1
⊢ ((head✝ :: xs).concat a).length = (head✝ :: xs).length + 1

Tactic:
simp [concat, ih]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_nodal {x : R} : (nodal s v).eval x = ∏ i ∈ s, (x - v i)

Proof state:
R : Type u_1
inst✝ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
x : R
⊢ eval x (nodal s v) = ∏ i ∈ s, (x - v i)

Tactic:
simp_rw [nodal, eval_prod, eval_sub, eval_X, eval_C]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
/-- An `IsRkFinite` set has a finset basis' -/
lemma IsRkFinite.exists_finset_isBasis' (h : M.IsRkFinite X) : ∃ (I : Finset α), M.IsBasis' I X :=
  let ⟨I, hI, hIfin⟩ := h.exists_finite_isBasis'
  ⟨hIfin.toFinset, by simpa⟩

Proof state:
α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite X
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
⊢ M.IsBasis' (↑hIfin.toFinset) X

Tactic:
simpa

Result:
no goals