harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Mul.lean
theorem two_mul_expl {R : Type*} [CommRing R] (A B : Matrix (Fin 2) (Fin 2) R) :
    (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
    (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧
    (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Proof state:
case refine_4
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 1 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
simp

Result:
no goals

Proof state:
case refine_4
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]

Result:
case refine_4
R : Type u_10
inst✝ : CommRing R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 1 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma krullDim_WithTop [Nonempty α] : krullDim (WithTop α) = krullDim α + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ x, height ↑x + 1 = ⨆ i, height i + 1

Tactic:
symm

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ i, height i + 1 = ⨆ x, height ↑x + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y ≠ ⊤), height y + 1 = (⨆ a, height a) + 1

Tactic:
rw [ENat.iSup_add, iSup_subtype']

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ x, height ↑x + 1 = ⨆ i, height i + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithTop α) = krullDim α + 1

Tactic:
rw [← height_top_eq_krullDim, krullDim_eq_iSup_height_of_nonempty, height_eq_iSup_lt_height]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ y, ⨆ (_ : y < ⊤), height y + 1) = ↑(⨆ a, height a) + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ y, ⨆ (_ : y < ⊤), height y + 1) = ↑(⨆ a, height a) + 1

Tactic:
norm_cast

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y < ⊤), height y + 1 = (⨆ a, height a) + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ i, height i + 1 = ⨆ x, height ↑x + 1

Tactic:
apply Equiv.withTopSubtypeNe.symm.iSup_congr

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (x : α), height ↑(Equiv.withTopSubtypeNe.symm x) + 1 = height x + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ∀ (x : α), height ↑(Equiv.withTopSubtypeNe.symm x) + 1 = height x + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y < ⊤), height y + 1 = (⨆ a, height a) + 1

Tactic:
simp_rw [WithTop.lt_top_iff_ne_top]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y ≠ ⊤), height y + 1 = (⨆ a, height a) + 1
-- Mathlib/SetTheory/Game/Basic.lean
theorem leftMoves_mul_cases {x y : PGame} (k) {P : (x * y).LeftMoves → Prop}
    (hl : ∀ ix iy, P <| toLeftMovesMul (Sum.inl ⟨ix, iy⟩))
    (hr : ∀ jx jy, P <| toLeftMovesMul (Sum.inr ⟨jx, jy⟩)) : P k

Proof state:
case inr.mk
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
jx : x.RightMoves
jy : y.RightMoves
⊢ P (toLeftMovesMul (Sum.inr (jx, jy)))

Tactic:
apply hr

Result:
no goals

Proof state:
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
⊢ P (toLeftMovesMul (toLeftMovesMul.symm k))

Tactic:
rcases toLeftMovesMul.symm k with (⟨ix, iy⟩ | ⟨jx, jy⟩)

Result:
case inl.mk
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
ix : x.LeftMoves
iy : y.LeftMoves
⊢ P (toLeftMovesMul (Sum.inl (ix, iy)))

case inr.mk
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
jx : x.RightMoves
jy : y.RightMoves
⊢ P (toLeftMovesMul (Sum.inr (jx, jy)))

Proof state:
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
⊢ P k

Tactic:
rw [← toLeftMovesMul.apply_symm_apply k]

Result:
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
⊢ P (toLeftMovesMul (toLeftMovesMul.symm k))

Proof state:
case inl.mk
x y : PGame
k : (x * y).LeftMoves
P : (x * y).LeftMoves → Prop
hl : ∀ (ix : x.LeftMoves) (iy : y.LeftMoves), P (toLeftMovesMul (Sum.inl (ix, iy)))
hr : ∀ (jx : x.RightMoves) (jy : y.RightMoves), P (toLeftMovesMul (Sum.inr (jx, jy)))
ix : x.LeftMoves
iy : y.LeftMoves
⊢ P (toLeftMovesMul (Sum.inl (ix, iy)))

Tactic:
apply hl

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) :
    Splits (algebraMap K L) (X ^ (n : ℕ) - 1)

Proof state:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)

Tactic:
obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS

Result:
case intro
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z ↑n
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)

Proof state:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (algebraMap K L) (X ^ ↑n - 1)

Tactic:
rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
  Polynomial.map_X]

Result:
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)

Proof state:
case intro
n : ℕ+
S : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z ↑n
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)

Tactic:
exact X_pow_sub_one_splits hz

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂)
    (ce : V₁ →ₗ[K] V₃) (hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb) (hgd : ker cd = ⊥)
    (eq : db.comp cd = eb.comp ce) (eq₂ : ∀ d e, db d = eb e → ∃ c, cd c = d ∧ ce c = e) :
    Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Proof state:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb
hgd : ker cd = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
c : V₁
⊢ db (cd c) = eb (ce c)

Tactic:
exact LinearMap.ext_iff.1 eq c

Result:
no goals

Proof state:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb
hgd : ker cd = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
c : V₁
⊢ (cd.prod (-ce)) c ∈ ker (db.coprod eb)

Tactic:
simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker, Pi.prod, coprod_apply,
  neg_neg, map_neg, neg_apply]

Result:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb
hgd : ker cd = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
c : V₁
⊢ db (cd c) = eb (ce c)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem head_takeWhile (p : α → Bool) (l : List α) (w) :
    (l.takeWhile p).head w = l.head (by rintro rfl; simp_all)

Proof state:
α : Type u_1
p : α → Bool
l : List α
w : takeWhile p l ≠ []
⊢ (takeWhile p l).head w = l.head ⋯

Tactic:
cases l with
| nil => rfl
| cons x xs =>
  simp only [takeWhile_cons, head_cons]
  simp only [takeWhile_cons] at w
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
w : takeWhile p (x :: xs) ≠ []
⊢ (if p x = true then x :: takeWhile p xs else []).head ⋯ = x

Tactic:
simp only [takeWhile_cons] at w

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
w✝ : takeWhile p (x :: xs) ≠ []
w : (if p x = true then x :: takeWhile p xs else []) ≠ []
⊢ (if p x = true then x :: takeWhile p xs else []).head ⋯ = x

Proof state:
α : Type ?u.22849
p : α → Bool
l : List α
w : takeWhile p l ≠ []
⊢ l ≠ []

Tactic:
rintro rfl

Result:
α : Type ?u.22849
p : α → Bool
w : takeWhile p [] ≠ []
⊢ False

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
w✝ : takeWhile p (x :: xs) ≠ []
w : (if p x = true then x :: takeWhile p xs else []) ≠ []
⊢ (if p x = true then x :: takeWhile p xs else []).head ⋯ = x

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type ?u.22849
p : α → Bool
w : takeWhile p [] ≠ []
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
w : takeWhile p (x :: xs) ≠ []
⊢ (takeWhile p (x :: xs)).head w = (x :: xs).head ⋯

Tactic:
simp only [takeWhile_cons, head_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
w : takeWhile p (x :: xs) ≠ []
⊢ (if p x = true then x :: takeWhile p xs else []).head ⋯ = x

Proof state:
case nil
α : Type u_1
p : α → Bool
w : takeWhile p [] ≠ []
⊢ (takeWhile p []).head w = [].head ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem map_id : ∀ s : Computation α, map id s = s
  | ⟨f, al⟩ => by
    apply Subtype.eq; simp only [map, comp_apply, id_eq]
    have e : @Option.rec α (fun _ => Option α) none some = id

Proof state:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Tactic:
have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl

Result:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
e : Option.rec none some = id
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Proof state:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ map id ⟨f, al⟩ = ⟨f, al⟩

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(map id ⟨f, al⟩) = ↑⟨f, al⟩

Proof state:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(map id ⟨f, al⟩) = ↑⟨f, al⟩

Tactic:
simp only [map, comp_apply, id_eq]

Result:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Proof state:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
e : Option.rec none some = id
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Tactic:
have h : ((fun x : Option α => x) = id) := rfl

Result:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
e : Option.rec none some = id
h : (fun x => x) = id
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Proof state:
case a
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
e : Option.rec none some = id
h : (fun x => x) = id
⊢ Stream'.map (fun o => Option.rec none (fun val => some val) o) f = f

Tactic:
simp [e, h, Stream'.map_id]

Result:
no goals

Proof state:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Option.rec none some = id

Tactic:
ext ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem subsingleton_quotient_top : Subsingleton (G ⧸ (⊤ : Subgroup G))

Proof state:
G : Type u
inst✝ : Group G
⊢ Subsingleton (G ⧸ ⊤)

Tactic:
dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]

Result:
G : Type u
inst✝ : Group G
⊢ Subsingleton (Quot ⇑(leftRel ⊤))

Proof state:
G : Type u
inst✝ : Group G
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)

Tactic:
exact Trunc.instSubsingletonTrunc

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ Subsingleton (Quot ⇑(leftRel ⊤))

Tactic:
rw [leftRel_eq]

Result:
G : Type u
inst✝ : Group G
⊢ Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
-- Mathlib/Data/List/Dedup.lean
theorem Perm.dedup {l₁ l₂ : List α} (p : l₁ ~ l₂) : dedup l₁ ~ dedup l₂ :=
  perm_iff_count.2 fun a =>
    if h : a ∈ l₁ then by
      simp [h, nodup_dedup, p.subset h]
    else by
      simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ count a l₁.dedup = count a l₂.dedup

Tactic:
simp [h, nodup_dedup, p.subset h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∉ l₁
⊢ count a l₁.dedup = count a l₂.dedup

Tactic:
simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem dot_self_cross (v w : Fin 3 → R) : v ⬝ᵥ v ×₃ w = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v 0 * (v 1 * w 2 - v 2 * w 1) + v 1 * (v 2 * w 0 - v 0 * w 2) + v 2 * (v 0 * w 1 - v 1 * w 0) = 0

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v ⬝ᵥ (crossProduct v) w = 0

Tactic:
rw [cross_apply, vec3_dotProduct]

Result:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        v 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      v 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    0

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        v 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      v 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    0

Tactic:
norm_num

Result:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ v 0 * (v 1 * w 2 - v 2 * w 1) + v 1 * (v 2 * w 0 - v 0 * w 2) + v 2 * (v 0 * w 1 - v 1 * w 0) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_max_left (a b : Int) : a ≤ max a b

Proof state:
a b : Int
⊢ a ≤ max a b

Tactic:
rw [Int.max_def]

Result:
a b : Int
⊢ a ≤ if a ≤ b then b else a

Proof state:
a b : Int
⊢ a ≤ if a ≤ b then b else a

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.image_succAbove_univ {n : ℕ} (i : Fin (n + 1)) : univ.image i.succAbove = {i}ᶜ

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ image i.succAbove univ = {i}ᶜ

Tactic:
ext m

Result:
case h
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image i.succAbove univ ↔ m ∈ {i}ᶜ

Proof state:
case h
n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image i.succAbove univ ↔ m ∈ {i}ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/ArrayMap.lean
theorem toArrayMap_eq_toArray_map (l : List α) (f : α → β) : l.toArrayMap f = (l.map f).toArray :=
  Array.ext' (by simpa using toArrayMap_toList l f)

Proof state:
α : Type u
β : Type v
l : List α
f : α → β
⊢ (l.toArrayMap f).toList = (map f l).toArray.toList

Tactic:
simpa using toArrayMap_toList l f

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem Parallel.vectorSpan_eq {s₁ s₂ : Set P} (h : affineSpan k s₁ ∥ affineSpan k s₂) :
    vectorSpan k s₁ = vectorSpan k s₂

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₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ vectorSpan k s₁ = vectorSpan k s₂

Tactic:
simp_rw [← direction_affineSpan]

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₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ (affineSpan k s₁).direction = (affineSpan k s₂).direction

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₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ (affineSpan k s₁).direction = (affineSpan k s₂).direction

Tactic:
exact h.direction_eq

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma height_le_height_apply_of_strictMono (f : α → β) (hf : StrictMono f) (x : α) :
    height x ≤ height (f x)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
intro p hlast

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ RelSeries.last (p.map f hf) = f x

Tactic:
simp [hlast]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ height x ≤ height (f x)

Tactic:
simp only [height_eq_iSup_last_eq]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ↑(p.map f hf).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
apply le_iSup₂_of_le (p.map f hf) (by simp [hlast]) (by simp)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length

Tactic:
apply iSup₂_le

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p = f x), ↑p.length
-- Mathlib/RingTheory/Artinian/Module.lean
theorem exists_pow_succ_smul_dvd (r : R) (x : M) :
    ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ n.succ • y = r ^ n • x

Tactic:
exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
⊢ ∃ n y, r ^ n.succ • y = r ^ n • x

Tactic:
obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ n.succ • y = r ^ n • x

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ n.succ • y = r ^ n • x

Tactic:
simp_rw [SetLike.ext_iff] at hn

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ n y, r ^ n.succ • y = r ^ n • x

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)
⊢ ∃ y, r ^ n.succ • y = r ^ n • x

Tactic:
simpa using hn n.succ n.le_succ (r ^ n • x)

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem ofFunction_le (s : Set α) : OuterMeasure.ofFunction m m_empty s ≤ m s :=
  let f : ℕ → Set α := fun i => Nat.casesOn i s fun _ => ∅
  iInf_le_of_le f <|
    iInf_le_of_le (subset_iUnion f 0) <|
      le_of_eq <| tsum_eq_single 0 <| by
        rintro (_ | i)
        · simp
        · simp [f, m_empty]

Proof state:
case zero
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i => Nat.casesOn i s fun x => ∅
⊢ 0 ≠ 0 → m (f 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i => Nat.casesOn i s fun x => ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0

Tactic:
simp [f, m_empty]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i => Nat.casesOn i s fun x => ∅
⊢ ∀ (b' : ℕ), b' ≠ 0 → m (f b') = 0

Tactic:
rintro (_ | i)

Result:
case zero
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i => Nat.casesOn i s fun x => ∅
⊢ 0 ≠ 0 → m (f 0) = 0

case succ
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
f : ℕ → Set α := fun i => Nat.casesOn i s fun x => ∅
i : ℕ
⊢ i + 1 ≠ 0 → m (f (i + 1)) = 0