harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem reverse_comp_involute :
    reverse.comp involute.toLinearMap =
      (involute.toLinearMap.comp reverse : _ →ₗ[R] CliffordAlgebra Q)

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ (reverse ∘ₗ involute.toLinearMap) x = (involute.toLinearMap ∘ₗ reverse) x

Tactic:
simp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply]

Result:
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ reverse (involute x) = involute (reverse x)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ reverse ∘ₗ involute.toLinearMap = involute.toLinearMap ∘ₗ reverse

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ (reverse ∘ₗ involute.toLinearMap) x = (involute.toLinearMap ∘ₗ reverse) x

Proof state:
case h.add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : reverse (involute a) = involute (reverse a)
hb : reverse (involute b) = involute (reverse b)
⊢ reverse (involute (a + b)) = involute (reverse (a + b))

Tactic:
simp only [ha, hb, reverse.map_add, map_add]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ reverse (involute x) = involute (reverse x)

Tactic:
induction x using CliffordAlgebra.induction with
| algebraMap => simp
| ι => simp
| mul a b ha hb => simp only [ha, hb, reverse.map_mul, map_mul]
| add a b ha hb => simp only [ha, hb, reverse.map_add, map_add]

Result:
no goals

Proof state:
case h.ι
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : M
⊢ reverse (involute ((ι Q) x✝)) = involute (reverse ((ι Q) x✝))

Tactic:
simp

Result:
no goals

Proof state:
case h.algebraMap
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r✝ : R
⊢ reverse (involute ((algebraMap R (CliffordAlgebra Q)) r✝)) =
    involute (reverse ((algebraMap R (CliffordAlgebra Q)) r✝))

Tactic:
simp

Result:
no goals

Proof state:
case h.mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : reverse (involute a) = involute (reverse a)
hb : reverse (involute b) = involute (reverse b)
⊢ reverse (involute (a * b)) = involute (reverse (a * b))

Tactic:
simp only [ha, hb, reverse.map_mul, map_mul]

Result:
no goals
-- Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
@[to_additive]
lemma pow_ssubset_pow_succ_of_pow_ne_closure (hX₁ : (1 : G) ∈ X) (hX : X.Nontrivial)
    (hXclosure : (X ^ n : Set G) ≠ closure (X : Set G)) : X ^ n ⊂ X ^ (n + 1)

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
⊢ x⁻¹ ∈ X

Tactic:
have : x • X ⊆ X := by
  simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this : x • X ⊆ X
⊢ x⁻¹ ∈ X

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ 1 = 1

Tactic:
simp [hXn, ← pow_mul, mul_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
    (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]?

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
h : ¬i < l₁.length
⊢ l₁.length ≤ i

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < l₁.length
⊢ (l₁ ++ l₂)[i]? = l₁[i]?

Tactic:
exact getElem?_append_left h

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
⊢ (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
l₁ l₂ : List α
i : Nat
h : i < l₁.length
⊢ (l₁ ++ l₂)[i]? = l₁[i]?

case isFalse
α : Type u_1
l₁ l₂ : List α
i : Nat
h : ¬i < l₁.length
⊢ (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?

Proof state:
case isFalse
α : Type u_1
l₁ l₂ : List α
i : Nat
h : ¬i < l₁.length
⊢ (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?

Tactic:
exact getElem?_append_right (by simpa using h)

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem prod_snd_mk {α β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :
    TypeVec.prod.snd i (prod.mk i a b) = b

Proof state:
case fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.snd Fin2.fz (prod.mk Fin2.fz a b) = b

Tactic:
simp_all [prod.snd, prod.mk]

Result:
no goals

Proof state:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.snd a✝ (prod.mk a✝ a b) = b
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.snd a✝.fs (prod.mk a✝.fs a b) = b

Tactic:
apply i_ih

Result:
no goals

Proof state:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd i (prod.mk i a b) = b

Tactic:
induction i with
| fz => simp_all [prod.snd, prod.mk]
| fs _ i_ih => apply i_ih

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem foldrIdx_start :
    (xs : List α).foldrIdx f i s = (xs : List α).foldrIdx (fun i => f (i + s)) i

Proof state:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx (fun i => f (i + (s + 1))) i t) = f (0 + s) h (foldrIdx (fun i => f (i + 1 + s)) i t)

Tactic:
simp [Nat.add_assoc, Nat.add_comm 1 s]

Result:
no goals

Proof state:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx f i t (s + 1)) = f (0 + s) h (foldrIdx (fun i => f (i + s)) i t 1)

Tactic:
simp only [@ih f]

Result:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx (fun i => f (i + (s + 1))) i t) = f (0 + s) h (foldrIdx (fun i => f (i + s)) i t 1)

Proof state:
case nil
α : Type u_1
α✝ : Sort u_2
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ foldrIdx f i [] s = foldrIdx (fun i => f (i + s)) i []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
xs : List α
α✝ : Sort u_2
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ foldrIdx f i xs s = foldrIdx (fun i => f (i + s)) i xs

Tactic:
induction xs generalizing f i s with
| nil => rfl
| cons h t ih =>
  dsimp [foldrIdx]
  simp only [@ih f]
  simp only [@ih (fun i => f (i + s))]
  simp [Nat.add_assoc, Nat.add_comm 1 s]

Result:
no goals

Proof state:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx (fun i => f (i + (s + 1))) i t) = f (0 + s) h (foldrIdx (fun i => f (i + s)) i t 1)

Tactic:
simp only [@ih (fun i => f (i + s))]

Result:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx (fun i => f (i + (s + 1))) i t) = f (0 + s) h (foldrIdx (fun i => f (i + 1 + s)) i t)

Proof state:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ foldrIdx f i (h :: t) s = foldrIdx (fun i => f (i + s)) i (h :: t)

Tactic:
dsimp [foldrIdx]

Result:
case cons
α : Type u_1
α✝ : Sort u_2
h : α
t : List α
ih : ∀ {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat}, foldrIdx f i t s = foldrIdx (fun i => f (i + s)) i t
f : Nat → α → α✝ → α✝
i : α✝
s : Nat
⊢ f s h (foldrIdx f i t (s + 1)) = f (0 + s) h (foldrIdx (fun i => f (i + s)) i t 1)
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem Submonoid.equivMapOfInjective_coe_mulEquiv (e : M ≃* N) :
    S.equivMapOfInjective (e : M →* N) (EquivLike.injective e) = e.submonoidMap S

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Tactic:
ext

Result:
case h.a
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
x✝ : ↥S
⊢ ↑((S.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.submonoidMap S) x✝)

Proof state:
case h.a
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
x✝ : ↥S
⊢ ↑((S.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.submonoidMap S) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem subtypeEquiv_symm {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a : α, p a ↔ q (e a)) :
    (e.subtypeEquiv h).symm =
      e.symm.subtypeEquiv fun a => by
        convert (h <| e.symm a).symm
        exact (e.apply_symm_apply a).symm :=
  rfl

Proof state:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
a : β
⊢ q a ↔ p (e.symm a)

Tactic:
convert (h <| e.symm a).symm

Result:
case h.e'_1.h.e'_1
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
a : β
⊢ a = e (e.symm a)

Proof state:
case h.e'_1.h.e'_1
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
a : β
⊢ a = e (e.symm a)

Tactic:
exact (e.apply_symm_apply a).symm

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem convexHull_eq (s : Set E) : convexHull R s =
    { x : E | ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E), (∀ i ∈ t, 0 ≤ w i) ∧
      ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x }

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
hi : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
⊢ 0 ≤ Sum.elim (fun i => a * wx i) (fun j => b * wy j) i

Tactic:
rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩) <;> simp only [Sum.elim_inl, Sum.elim_inr] <;>
  apply_rules [mul_nonneg, hwx₀, hwy₀]

Result:
no goals

Proof state:
case refine_3.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ (convexHull R) s

Tactic:
exact t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem isOpen_iff_isOpen_ball_subset {s : Set α} :
    IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Proof state:
case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
obtain ⟨V, hV, -, hV'⟩ := h x hx

Result:
case mpr.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
case mp.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Tactic:
exact
  ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
    (ball_mono interior_subset x).trans hV'⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, hV, hV'⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Tactic:
constructor <;> intro h x hx

Result:
case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

case mpr
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
case mp
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
⊢ ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Tactic:
obtain ⟨V, hV, hV'⟩ := h x hx

Result:
case mp.intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s

Tactic:
rw [isOpen_iff_ball_subset]

Result:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen V ∧ ball x V ⊆ s
-- Mathlib/Data/Nat/Nth.lean
theorem nth_of_card_le (hf : (setOf p).Finite) {n : ℕ} (hn : #hf.toFinset ≤ n) :
    nth p n = 0

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ nth p n = 0

Tactic:
rw [nth, dif_pos hf, List.getD_eq_default]

Result:
case hn
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (sort (fun x1 x2 => x1 ≤ x2) hf.toFinset).length ≤ n

Proof state:
case hn
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (sort (fun x1 x2 => x1 ≤ x2) hf.toFinset).length ≤ n

Tactic:
rwa [Finset.length_sort]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_X_pow : divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)

Tactic:
ext n

Result:
case succ.a
R : Type u
inst✝ : Semiring R
n✝ n : ℕ
⊢ (X ^ (n✝ + 1)).divX.coeff n = (if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)).coeff n

Proof state:
case succ.a
R : Type u
inst✝ : Semiring R
n✝ n : ℕ
⊢ (X ^ (n✝ + 1)).divX.coeff n = (if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)).coeff n

Tactic:
simp [coeff_X_pow]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
⊢ (X ^ 0).divX = if 0 = 0 then 0 else X ^ (0 - 1)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
⊢ (X ^ n).divX = if n = 0 then 0 else X ^ (n - 1)

Tactic:
cases n

Result:
case zero
R : Type u
inst✝ : Semiring R
⊢ (X ^ 0).divX = if 0 = 0 then 0 else X ^ (0 - 1)

case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)
-- Mathlib/LinearAlgebra/CrossProduct.lean
lemma crossProduct_ne_zero_iff_linearIndependent {F : Type*} [Field F] {v w : Fin 3 → F} :
    crossProduct v w ≠ 0 ↔ LinearIndependent F ![v, w]

Proof state:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (∃ x, x • v = w) → (crossProduct v) w = 0

Tactic:
rintro ⟨a, rfl⟩

Result:
case neg.mp.intro
F : Type u_2
inst✝ : Field F
v : Fin 3 → F
hv : ¬v = 0
a : F
⊢ (crossProduct v) (a • v) = 0

Proof state:
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Tactic:
by_cases hv : v = 0

Result:
case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

case neg
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Proof state:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
⊢ (crossProduct v) w = 0 → ¬LinearIndependent F ![v, w]

Tactic:
intro h1 h2

Result:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h1 : (crossProduct v) w = 0
h2 : LinearIndependent F ![v, w]
⊢ False

Proof state:
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ v = ![v 0, v 1, v 2]

Tactic:
simp [← List.ofFn_inj]

Result:
no goals

Proof state:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
⊢ False

Tactic:
have h21 := LinearIndependent.pair_iff.mp h2 (- w 1) (v 1)

Result:
case neg.mpr
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
hv' : v = ![v 0, v 1, v 2]
hw' : w = ![w 0, w 1, w 2]
h2 : LinearIndependent F ![v, w]
h1 : v 1 * w 2 = v 2 * w 1 ∧ v 2 * w 0 = v 0 * w 2 ∧ v 0 * w 1 = v 1 * w 0
h20 : -w 0 • v + v 0 • w = 0 → -w 0 = 0 ∧ v 0 = 0
h21 : -w 1 • v + v 1 • w = 0 → -w 1 = 0 ∧ v 1 = 0
⊢ False

Proof state:
case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![v, w] ↔ (crossProduct v) w = 0

Tactic:
rw [hv, map_zero, LinearMap.zero_apply, eq_self, iff_true]

Result:
case pos
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : v = 0
⊢ ¬LinearIndependent F ![0, w]
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_comp {f : α → β} {g : β → γ} :
    mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂

Tactic:
intro

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β), single (g a) 0 = 0

Tactic:
intro

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0

Tactic:
exact single_zero _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)

Tactic:
refine ((sum_sum_index ?_ ?_).trans ?_).symm

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β), single (g a) 0 = 0

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = single (g a) b₁ + single (g a) b₂

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ (v.sum fun a b => (single (f a) b).sum fun a => single (g a)) = mapDomain (g ∘ f) v

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
x✝¹ : α
x✝ : x✝¹ ∈ v.support
⊢ single (g (f x✝¹)) 0 = 0

Tactic:
exact single_zero _

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ (v.sum fun a b => (single (f a) b).sum fun a => single (g a)) = mapDomain (g ∘ f) v

Tactic:
refine sum_congr fun _ _ => sum_single_index ?_

Result:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
x✝¹ : α
x✝ : x✝¹ ∈ v.support
⊢ single (g (f x✝¹)) 0 = 0

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ ∀ (b₁ b₂ : M), single (g a✝) (b₁ + b₂) = single (g a✝) b₁ + single (g a✝) b₂

Tactic:
exact single_add _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.of_sublist_append_left (w : ∀ a, a ∈ l → a ∉ l₂) (h : l <+ l₁ ++ l₂) : l <+ l₁

Proof state:
α✝ : Type u_1
l l₂ l₁ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₂
h : l <+ l₁ ++ l₂
⊢ l <+ l₁

Tactic:
rw [sublist_append_iff] at h

Result:
α✝ : Type u_1
l l₂ l₁ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₂
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
⊢ l <+ l₁

Proof state:
α✝ : Type u_1
l l₂ l₁ : List α✝
w : ∀ (a : α✝), a ∈ l → ¬a ∈ l₂
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
⊢ l <+ l₁

Tactic:
obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h

Result:
case intro.intro.intro.intro
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₁

Proof state:
case intro.intro.intro.intro
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
this : l₂' = []
⊢ l₁' ++ l₂' <+ l₁

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.intro.intro.intro
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₁

Tactic:
have : l₂' = [] := by
  rw [eq_nil_iff_forall_not_mem]
  exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)

Result:
case intro.intro.intro.intro
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
this : l₂' = []
⊢ l₁' ++ l₂' <+ l₁

Proof state:
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ ∀ (a : α✝), ¬a ∈ l₂'

Tactic:
exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)

Result:
no goals

Proof state:
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₂' = []

Tactic:
rw [eq_nil_iff_forall_not_mem]

Result:
α✝ : Type u_1
l₂ l₁ l₁' l₂' : List α✝
w : ∀ (a : α✝), a ∈ l₁' ++ l₂' → ¬a ∈ l₂
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ ∀ (a : α✝), ¬a ∈ l₂'