harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem mem_affineSpan_insert_iff {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) :
    p ∈ affineSpan k (insert p₂ (s : Set P)) ↔
      ∃ r : k, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁ : V) +ᵥ p0

Proof state:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁) → ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rintro ⟨v₁, hv₁, v₂, hv₂, hp⟩

Result:
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₁ : V
hv₁ : v₁ ∈ Submodule.span k {p₂ -ᵥ p₁}
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [← mem_coe] at hp₁

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
    a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h])

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
⊢ a[i] = a[i]?.get ⋯

Tactic:
simp [getElem_eq_iff]

Result:
no goals

Proof state:
α : Type ?u.15874
a : Array α
i : Nat
h : i < a.size
⊢ a[i]?.isSome = true

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_flatMap {α} [BEq β] (l : Vector α n) (f : α → Vector β m) (x : β) :
    count x (l.flatMap f) = (map (count x ∘ f) l).sum

Proof state:
β : Type u_1
n m : Nat
α : Type u_2
inst✝ : BEq β
l : Vector α n
f : α → Vector β m
x : β
⊢ count x (l.flatMap f) = (map (count x ∘ f) l).sum

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
m : Nat
α : Type u_2
inst✝ : BEq β
f : α → Vector β m
x : β
l : Array α
⊢ count x ({ toArray := l, size_toArray := ⋯ }.flatMap f) = (map (count x ∘ f) { toArray := l, size_toArray := ⋯ }).sum

Proof state:
case mk
β : Type u_1
m : Nat
α : Type u_2
inst✝ : BEq β
f : α → Vector β m
x : β
l : Array α
⊢ count x ({ toArray := l, size_toArray := ⋯ }.flatMap f) = (map (count x ∘ f) { toArray := l, size_toArray := ⋯ }).sum

Tactic:
simp [Array.count_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem mul_of'_divOf (x : k[G]) (a : G) : x * of' k G a /ᵒᶠ a = x

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ : G
⊢ (x * of' k G a /ᵒᶠ a) x✝ = x x✝

Tactic:
rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]

Result:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ : G
⊢ ∀ a_1 ∈ x.support, a_1 + a = a + x✝ ↔ a_1 = x✝

Proof state:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ c : G
hc : c ∈ x.support
⊢ c + a = a + x✝ ↔ c = x✝

Tactic:
rw [add_comm]

Result:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ c : G
hc : c ∈ x.support
⊢ a + c = a + x✝ ↔ c = x✝

Proof state:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ c : G
hc : c ∈ x.support
⊢ a + c = a + x✝ ↔ c = x✝

Tactic:
exact add_right_inj _

Result:
no goals

Proof state:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ : G
⊢ ∀ a_1 ∈ x.support, a_1 + a = a + x✝ ↔ a_1 = x✝

Tactic:
intro c hc

Result:
case H.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ c : G
hc : c ∈ x.support
⊢ c + a = a + x✝ ↔ c = x✝

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a : G
⊢ x * of' k G a /ᵒᶠ a = x

Tactic:
ext

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
a x✝ : G
⊢ (x * of' k G a /ᵒᶠ a) x✝ = x x✝
-- Mathlib/LinearAlgebra/Determinant.lean
theorem AlternatingMap.eq_smul_basis_det (f : M [⋀^ι]→ₗ[R] R) : f = f e • e.det

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ f (⇑e ∘ ⇑σ) = (f ⇑e • e.det) (⇑e ∘ ⇑σ)

Tactic:
simp [AlternatingMap.map_perm, Basis.det_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
⊢ (f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)

Tactic:
let σ : Equiv.Perm ι := Equiv.ofBijective i (Finite.injective_iff_bijective.1 h)

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ (f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
⊢ f = f ⇑e • e.det

Tactic:
refine Basis.ext_alternating e fun i h => ?_

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
⊢ (f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ (f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)

Tactic:
change f (e ∘ σ) = (f e • e.det) (e ∘ σ)

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ f (⇑e ∘ ⇑σ) = (f ⇑e • e.det) (⇑e ∘ ⇑σ)
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
/-- A version of `QuadraticMap.associated_left_inverse` for general targets. -/
lemma associated_left_inverse' {B₁ : BilinMap R M N} (hB₁ : B₁.flip = B₁) :
    associatedHom S B₁.toQuadraticMap = B₁

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
⊢ (associatedHom S) B₁.toQuadraticMap = B₁

Tactic:
ext _ y

Result:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ (((associatedHom S) B₁.toQuadraticMap) x✝) y = (B₁ x✝) y

Proof state:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ (((associatedHom S) B₁.toQuadraticMap) x✝) y = (B₁ x✝) y

Tactic:
rw [associated_toQuadraticMap, ← LinearMap.flip_apply _ y, hB₁, invOf_smul_eq_iff, two_smul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ (σ * τ * σ⁻¹).support = map (Equiv.toEmbedding σ) τ.support

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
a✝ : α
⊢ a✝ ∈ (σ * τ * σ⁻¹).support ↔ a✝ ∈ map (Equiv.toEmbedding σ) τ.support

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
a✝ : α
⊢ a✝ ∈ (σ * τ * σ⁻¹).support ↔ a✝ ∈ map (Equiv.toEmbedding σ) τ.support

Tactic:
simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support,
  Equiv.eq_symm_apply, inv_def]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_left {g : α ≃*o β} {f₁ f₂ : β ≃*o γ} (hg : Function.Surjective g) :
    g.trans f₁ = g.trans f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g : α ≃*o β
f₁ f₂ : β ≃*o γ
hg : Surjective ⇑g
x✝ : f₁ = f₂
⊢ g.trans f₁ = g.trans f₂

Tactic:
congr

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_cast_zmod_lt {m : ℕ} [NeZero m] (n : ℕ) [NeZero n] (a : ZMod m) :
    (a.cast : ZMod n).val < m

Proof state:
case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.cast.val < m + 1

Tactic:
rw [← natCast_val, val_cast_of_lt]

Result:
case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1

Proof state:
m : ℕ
inst✝¹ : NeZero m
n : ℕ
inst✝ : NeZero n
a : ZMod m
⊢ a.cast.val < m

Tactic:
rcases m with (⟨⟩|⟨m⟩)

Result:
case zero
n : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast.val < 0

case succ
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
⊢ a.cast.val < m + 1

Proof state:
case pos
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : m < n
⊢ a.cast.val < m + 1

Tactic:
rcases n with (⟨⟩|⟨n⟩)

Result:
case pos.zero
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
inst✝ : NeZero 0
h : m < 0
⊢ a.cast.val < m + 1

case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.cast.val < m + 1

Proof state:
case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

Tactic:
apply a.val_lt

Result:
no goals

Proof state:
case pos.zero
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
inst✝ : NeZero 0
h : m < 0
⊢ a.cast.val < m + 1

Tactic:
simp at h

Result:
no goals

Proof state:
case pos.succ
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1

Tactic:
apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h

Result:
no goals

Proof state:
case zero
n : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero 0
a : ZMod 0
⊢ a.cast.val < 0

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : ¬m < n
⊢ a.cast.val < m + 1

Tactic:
rw [not_lt] at h

Result:
case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1

Proof state:
case succ
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
⊢ a.cast.val < m + 1

Tactic:
by_cases h : m < n

Result:
case pos
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : m < n
⊢ a.cast.val < m + 1

case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : ¬m < n
⊢ a.cast.val < m + 1

Proof state:
case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1

Tactic:
apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem isometry_pos_mul (a : { x : ℝ // 0 < x }) : Isometry (a • · : ℍ → ℍ)

Proof state:
case e_a.e_x
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Tactic:
exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')

Result:
no goals

Proof state:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (a • y₁) (a • y₂) = dist y₁ y₂

Tactic:
simp only [dist_eq, coe_pos_real_smul, pos_real_im]

Result:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ 2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Proof state:
a : { x // 0 < x }
⊢ Isometry fun x => a • x

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_

Result:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (a • y₁) (a • y₂) = dist y₁ y₂

Proof state:
case e_a.e_x
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Tactic:
rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs,
  Real.norm_eq_abs, mul_left_comm]

Result:
case e_a.e_x
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Proof state:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ 2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
congr 2

Result:
case e_a.e_x
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
-- Mathlib/Data/Set/Accumulate.lean
@[simp]
lemma accumulate_zero_nat (s : ℕ → Set β) : Accumulate s 0 = s 0

Proof state:
β : Type u_2
s : ℕ → Set β
⊢ Accumulate s 0 = s 0

Tactic:
simp [accumulate_def]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_of_fg_map_injective (hf : Function.Injective f) {N : Submodule R M}
    (hfn : (N.map f).FG) : N.FG :=
  let ⟨t, ht⟩ := hfn
  ⟨t.preimage f fun _ _ _ _ h => hf h,
    Submodule.map_injective_of_injective hf <| by
      rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
        Set.inter_eq_self_of_subset_left, ht]
      rw [← LinearMap.range_coe, ← span_le, ht, ← map_top]
      exact map_mono le_top⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f (span R ↑(t.preimage ⇑f ⋯)) = map f N

Tactic:
rw [map_span, Finset.coe_preimage, Set.image_preimage_eq_inter_range,
  Set.inter_eq_self_of_subset_left, ht]

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ ↑t ⊆ range ⇑f

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ map f ⊤

Tactic:
exact map_mono le_top

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ ↑t ⊆ range ⇑f

Tactic:
rw [← LinearMap.range_coe, ← span_le, ht, ← map_top]

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ map f ⊤
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem exists_minimal_degree_vertex [DecidableRel G.Adj] [Nonempty V] :
    ∃ v, G.minDegree = G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : v ∈ univ
ht : (image (fun v => G.degree v) univ).min = ↑(G.degree v)
⊢ G.minDegree = G.degree v

Tactic:
simp [minDegree, ht]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ ∃ v, G.minDegree = G.degree v

Tactic:
obtain ⟨t, ht : _ = _⟩ := min_of_nonempty (univ_nonempty.image fun v => G.degree v)

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
⊢ ∃ v, G.minDegree = G.degree v

Proof state:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : v ∈ univ
ht : (image (fun v => G.degree v) univ).min = ↑(G.degree v)
⊢ ∃ v, G.minDegree = G.degree v

Tactic:
exact ⟨v, by simp [minDegree, ht]⟩

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
⊢ ∃ v, G.minDegree = G.degree v

Tactic:
obtain ⟨v, _, rfl⟩ := mem_image.mp (mem_of_min ht)

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : v ∈ univ
ht : (image (fun v => G.degree v) univ).min = ↑(G.degree v)
⊢ ∃ v, G.minDegree = G.degree v
-- Mathlib/RingTheory/FiniteType.lean
theorem finiteType_iff_group_fg {G : Type*} [Group G] [CommRing R] [Nontrivial R] :
    FiniteType R (MonoidAlgebra R G) ↔ Group.FG G

Proof state:
R : Type u_1
G : Type u_3
inst✝² : Group G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (MonoidAlgebra R G) ↔ Group.FG G

Tactic:
simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem one_zpow : ∀ n : ℤ, (1 : M) ^ n = 1
  | (n : ℕ) => by rw [zpow_natCast, one_pow]
  | -[n+1] => by rw [zpow_negSucc, one_pow, inv_one]

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ -[n+1] = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ ↑n = 1

Tactic:
rw [zpow_natCast, one_pow]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma map_lift {i : J} (hij : i < j) :
    (lift hj s).map (homOfLE hij.le) = s.1 ⟨⟨i, hij⟩⟩

Proof state:
case f'
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
i : J
hij : i < j
⊢ (SqStruct.map (lift hj s) (homOfLE ⋯)).f' = (↑s (Opposite.op ⟨i, hij⟩)).f'

Tactic:
apply liftHom_fac

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
i : J
hij : i < j
⊢ SqStruct.map (lift hj s) (homOfLE ⋯) = ↑s (Opposite.op ⟨i, hij⟩)

Tactic:
ext

Result:
case f'
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
i : J
hij : i < j
⊢ (SqStruct.map (lift hj s) (homOfLE ⋯)).f' = (↑s (Opposite.op ⟨i, hij⟩)).f'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_eq_true_of_le (u v : Nat) : u ≤ v → (u ≤ v) = True :=
  by simp

Proof state:
u v : Nat
⊢ u ≤ v → (u ≤ v) = True

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem π_comp_cokernelIsoOfEq_hom {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.π f ≫ (cokernelIsoOfEq h).hom = cokernel.π g

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).hom = cokernel.π f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ cokernel.π f ≫ (cokernelIsoOfEq h).hom = cokernel.π g

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasCokernel f
⊢ cokernel.π f ≫ (cokernelIsoOfEq ⋯).hom = cokernel.π f