mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((star hP G ε hU V).product (star hP G ε hV U))) -
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))|

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ 3 / 4 * ε ≤
    |(∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((star hP G ε hU V).product (star hP G ε hV U))) -
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2)) /
          ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))|
Module: Mathlib.Combinatorics.Additive.SubsetSum

Goal state before:
pp: M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
⊢ a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum

Tactic:
[

Goal state after:
M : Type u_1
inst✝¹ : DecidableEq M
inst✝ : AddCommMonoid M
A : Finset M
a : M
a_notin_A : a ∉ A
⊢ a +ᵥ A.subsetSum ⊆ (insert a A).subsetSum
Module: Mathlib.Data.Finset.Slice

Goal state before:
pp: α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ i, f i) ↔ ∀ (i : ι), Sized r (f i)

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ Sized r (⋃ i, f i) ↔ ∀ (i : ι), Sized r (f i)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
key : 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
[

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
key : 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))
⊢ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ #P.parts) ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit.false
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit false n).bitIndices).sum = bit false n

pp: case bit.true
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit true n).bitIndices).sum = bit true n

Tactic:
· simpa [hrw, List.sum_map_mul_left]

Goal state after:
case bit.true
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit true n).bitIndices).sum = bit true n
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L

Tactic:
[

Goal state after:
case cons
a : ℕ
L : List ℕ
hL✝ : (a :: L).SortedLT
haL : ∀ (a' : ℕ), a' ∈ L → a < a'
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) L
⊢ (map (fun i ↦ 2 ^ i) (a :: L)).sum.bitIndices = a :: L
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1, m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2, m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0] +
      ![m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1, m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2, m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0]

Tactic:
[

Goal state after:
case H1
R : Type u_1
inst✝ : CommRing R
m₁✝ m₂✝ n✝ : Fin 3 → R
⊢ ![(m₁✝ + m₂✝) 1 * n✝ 2 - (m₁✝ + m₂✝) 2 * n✝ 1, (m₁✝ + m₂✝) 2 * n✝ 0 - (m₁✝ + m₂✝) 0 * n✝ 2,
      (m₁✝ + m₂✝) 0 * n✝ 1 - (m₁✝ + m₂✝) 1 * n✝ 0] =
    ![m₁✝ 1 * n✝ 2 - m₁✝ 2 * n✝ 1, m₁✝ 2 * n✝ 0 - m₁✝ 0 * n✝ 2, m₁✝ 0 * n✝ 1 - m₁✝ 1 * n✝ 0] +
      ![m₂✝ 1 * n✝ 2 - m₂✝ 2 * n✝ 1, m₂✝ 2 * n✝ 0 - m₂✝ 0 * n✝ 2, m₂✝ 0 * n✝ 1 - m₂✝ 1 * n✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![(c✝ • m✝) 1 * n✝ 2 - (c✝ • m✝) 2 * n✝ 1, (c✝ • m✝) 2 * n✝ 0 - (c✝ • m✝) 0 * n✝ 2,
      (c✝ • m✝) 0 * n✝ 1 - (c✝ • m✝) 1 * n✝ 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]

Tactic:
[

Goal state after:
case H2
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![(c✝ • m✝) 1 * n✝ 2 - (c✝ • m✝) 2 * n✝ 1, (c✝ • m✝) 2 * n✝ 0 - (c✝ • m✝) 0 * n✝ 2,
      (c✝ • m✝) 0 * n✝ 1 - (c✝ • m✝) 1 * n✝ 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1, m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2, m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0] +
      ![m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1, m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2, m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0]

Tactic:
[

Goal state after:
case H3
R : Type u_1
inst✝ : CommRing R
m✝ n₁✝ n₂✝ : Fin 3 → R
⊢ ![m✝ 1 * (n₁✝ + n₂✝) 2 - m✝ 2 * (n₁✝ + n₂✝) 1, m✝ 2 * (n₁✝ + n₂✝) 0 - m✝ 0 * (n₁✝ + n₂✝) 2,
      m✝ 0 * (n₁✝ + n₂✝) 1 - m✝ 1 * (n₁✝ + n₂✝) 0] =
    ![m✝ 1 * n₁✝ 2 - m✝ 2 * n₁✝ 1, m✝ 2 * n₁✝ 0 - m✝ 0 * n₁✝ 2, m✝ 0 * n₁✝ 1 - m✝ 1 * n₁✝ 0] +
      ![m✝ 1 * n₂✝ 2 - m✝ 2 * n₂✝ 1, m✝ 2 * n₂✝ 0 - m✝ 0 * n₂✝ 2, m✝ 0 * n₂✝ 1 - m✝ 1 * n₂✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * (c✝ • n✝) 2 - m✝ 2 * (c✝ • n✝) 1, m✝ 2 * (c✝ • n✝) 0 - m✝ 0 * (c✝ • n✝) 2,
      m✝ 0 * (c✝ • n✝) 1 - m✝ 1 * (c✝ • n✝) 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]

Tactic:
[

Goal state after:
case H4
R : Type u_1
inst✝ : CommRing R
c✝ : R
m✝ n✝ : Fin 3 → R
⊢ ![m✝ 1 * (c✝ • n✝) 2 - m✝ 2 * (c✝ • n✝) 1, m✝ 2 * (c✝ • n✝) 0 - m✝ 0 * (c✝ • n✝) 2,
      m✝ 0 * (c✝ • n✝) 1 - m✝ 1 * (c✝ • n✝) 0] =
    c✝ • ![m✝ 1 * n✝ 2 - m✝ 2 * n✝ 1, m✝ 2 * n✝ 0 - m✝ 0 * n✝ 2, m✝ 0 * n✝ 1 - m✝ 1 * n✝ 0]
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w x : Fin 3 → R
⊢ (crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
s t u : Finset α
inst✝ : DecidableEq α
hus : u ⊆ s
hut : u ⊆ t
⊢ toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u : Finset α
a✝ b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha : a ∈ symmDiff (ofColex t) (ofColex s)
hamax : ∀ x' ∈ symmDiff (ofColex t) (ofColex s), id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s

Tactic:
[

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t✝ u : Finset α
a✝ b : α
r : ℕ
s t : Colex (Finset α)
hts : t ≠ s
a : α
ha : a ∈ symmDiff (ofColex t) (ofColex s)
hamax : ∀ x' ∈ symmDiff (ofColex t) (ofColex s), id x' ≤ id a
⊢ s ≤ t ∨ t ≤ s
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K ↥v.submodule = 1

Tactic:
by
  rw [submodule_eq]
  exact finrank_span_singleton v.rep_nonzero

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: 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

Tactic:
[

Goal state after:
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
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (↑x✝⁵ ⬝ᵥ ↑x✝⁴ = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)

Tactic:
[

Goal state after:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
x✝⁵ x✝⁴ x✝³ x✝² : { v // v ≠ 0 }
x✝¹ : x✝⁵ ≈ x✝³
x✝ : x✝⁴ ≈ x✝²
w✝¹ : Fˣ
h1 : (fun m_1 ↦ m_1 • ↑x✝³) w✝¹ = ↑x✝⁵
w✝ : Fˣ
h2 : (fun m_1 ↦ m_1 • ↑x✝²) w✝ = ↑x✝⁴
⊢ (↑x✝⁵ ⬝ᵥ ↑x✝⁴ = 0) = (↑x✝³ ⬝ᵥ ↑x✝² = 0)
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: 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
h22 : -w 2 • v + v 2 • w = 0 → -w 2 = 0 ∧ v 2 = 0
⊢ False

Tactic:
rw [neg_smul, neg_add_eq_zero, hv', hw', smul_vec3, smul_vec3, ← hv', ← hw'] at h20 h21 h22

Goal state after:
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 0, w 0 • v 1, w 0 • v 2] = ![v 0 • w 0, v 0 • w 1, v 0 • w 2] → -w 0 = 0 ∧ v 0 = 0
h21 : ![w 1 • v 0, w 1 • v 1, w 1 • v 2] = ![v 1 • w 0, v 1 • w 1, v 1 • w 2] → -w 1 = 0 ∧ v 1 = 0
h22 : ![w 2 • v 0, w 2 • v 1, w 2 • v 2] = ![v 2 • w 0, v 2 • w 1, v 2 • w 2] → -w 2 = 0 ∧ v 2 = 0
⊢ False
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u
Module: Mathlib.LinearAlgebra.Projectivization.Constructions

Goal state before:
pp: F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (crossProduct ↑x✝⁵) ↑x✝² = 0 then x✝⁵ else ⟨(crossProduct ↑x✝⁵) ↑x✝², h⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩

Tactic:
[

Goal state after:
F : Type u_1
inst✝² : Field F
m : Type u_2
inst✝¹ : Fintype m
inst✝ : DecidableEq F
x✝⁵ x✝⁴ : { v // v ≠ 0 }
x✝³ : x✝⁵ ≈ x✝⁴
x✝² x✝¹ : { v // v ≠ 0 }
x✝ : x✝² ≈ x✝¹
a : Fˣ
ha : (fun m ↦ m • ↑x✝⁴) a = ↑x✝⁵
b : Fˣ
hb : (fun m ↦ m • ↑x✝¹) b = ↑x✝²
⊢ (if h : (crossProduct ↑x✝⁵) ↑x✝² = 0 then x✝⁵ else ⟨(crossProduct ↑x✝⁵) ↑x✝², h⟩) ≈
    if h : (crossProduct ↑x✝⁴) ↑x✝¹ = 0 then x✝⁴ else ⟨(crossProduct ↑x✝⁴) ↑x✝¹, h⟩
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
⊢ 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ (crossProduct u) ((crossProduct v) w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : #s = 0
⊢ #s ≤ #(s.biUnion t)

Tactic:
[

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : #s = 0
⊢ #s ≤ #(s.biUnion t)
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩

Tactic:
[

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ (Perm.ofSubtype f) a = a

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : ∀ a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f), ¬p a
a : α
ha : p a
hfa : f ⟨a, ha⟩ = ⟨a, ha⟩
⊢ (Perm.ofSubtype f) a = a
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ (_ : ∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f), ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
⊢ (∃ (_ : ∀ (a : α), ¬p a → a ∈ fixedPoints ⇑f), ∀ a ∈ fixedPoints ⇑f, ¬p a) ↔ ∀ (a : α), ¬p a ↔ a ∈ fixedPoints ⇑f
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : p₁ ∈ (s.biUnion t)ᶜ
hp₂ : p₂ ∈ (s.biUnion t)ᶜ
⊢ p₁ = p₂

Tactic:
[

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
p₁ p₂ : P
hp₁ : p₁ ∈ (s.biUnion t)ᶜ
hp₂ : p₂ ∈ (s.biUnion t)ᶜ
⊢ p₁ = p₂
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
x : Perm α
⊢ (∀ (a_1 : α), a_1 ∉ {a}ᶜ ↔ a_1 ∈ fixedPoints ⇑x) ↔ ∀ (x_1 : α), x_1 ∈ {a} ↔ x_1 ∈ fixedPoints ⇑x
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
fiber_none_is_false : ∀ (a : ↑(Equiv.RemoveNone.fiber none)), False
⊢ (a : α) × ↑(Equiv.RemoveNone.fiber (some a)) ≃ (a : α) × ↑{f | fixedPoints ⇑f ⊆ {a}}
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ x, ∑ x, lineCount L x = ∑ x, ∑ x, pointCount P x

Tactic:
[

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
⊢ ∑ x, ∑ x, lineCount L x = ∑ x, ∑ x, pointCount P x
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
[

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))

Tactic:
this

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
⊢ Tendsto (fun n ↦ s (n + 1)) atTop (𝓝 (Real.exp (-1)))
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ ∑ x ∈ {p | p ∈ l}.toFinset, pointCount P l = ∑ x ∈ {l_1 | f l ∈ l_1}.toFinset, lineCount L (f l)

Tactic:
[

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l✝ : L
hpl : p ∉ l✝
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
l : L
x✝ : l ∈ univ
⊢ ∑ x ∈ {p | p ∈ l}.toFinset, pointCount P l = ∑ x ∈ {l_1 | f l ∈ l_1}.toFinset, lineCount L (f l)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset

Tactic:
[

Goal state after:
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.2 ∈ univ ∧ p.1 ∈ {p_1 | p_1 ∈ p.2}.toFinset
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset

Tactic:
[

Goal state after:
case h
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
s : Finset (P × L) := {i | i.1 ∈ i.2}.toFinset
step1 : ∑ i, lineCount L i.1 = ∑ i, pointCount P i.2
⊢ ∀ (p : P × L), p ∈ s ↔ p.1 ∈ univ ∧ p.2 ∈ {l | p.1 ∈ l}.toFinset
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
⊢ { Adj := fun v w ↦ adj v w = true } = { Adj := fun v w ↦ adj' v w = true } → adj = adj'

Tactic:
[

Goal state after:
V : Type u_1
adj adj' : V → V → Bool
⊢ { Adj := fun v w ↦ adj v w = true } = { Adj := fun v w ↦ adj' v w = true } → adj = adj'
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ 1 ≤ Fintype.card { l // q ∈ l }

Tactic:
exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Goal state after: