awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h :
  LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![a, b])) ∧
    LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![c, d]))
A : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![a, b]
B : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![c, d]
⊢ (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h :
  LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![a, b])) ∧
    LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![c, d]))
A : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![a, b]
B : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![c, d]
⊢ A * Bᵀ = 0

Tactic:
have hAB : A * B.transpose = 0 := by
    ext i j
    fin_cases i <;> fin_cases j <;> assumption
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h :
  LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![a, b])) ∧
    LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![c, d]))
A : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![a, b]
B : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![c, d]
hAB : A * Bᵀ = 0
⊢ A.rank + Bᵀ.rank ≤ Fintype.card (Fin 3)

Tactic:
replace hAB := rank_add_rank_le_card_of_mul_eq_zero hAB
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h :
  LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![a, b])) ∧
    LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![c, d]))
A : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![a, b]
B : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![c, d]
hAB : A.rank + Bᵀ.rank ≤ Fintype.card (Fin 3)
⊢ (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3

Tactic:
rw [rank_transpose, h.1.rank_matrix, h.2.rank_matrix, Fintype.card_fin, Fintype.card_fin] at hAB

Premises used: Matrix.rank_transpose, Fintype.card_fin, LinearIndependent.rank_matrix, And.right, And.left
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
h :
  LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![a, b])) ∧
    LinearIndependent (ι := Fin (Nat.succ 0).succ) K (M := Fin 3 → K)
      (row ((of : (a : Fin (Nat.succ 0).succ → Fin 3 → K) → Matrix (Fin (Nat.succ 0).succ) (Fin 3) K) ![c, d]))
A : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![a, b]
B : Matrix (Fin 2) (Fin 3) K := (of : (a : Fin 2 → Fin 3 → K) → Matrix (Fin 2) (Fin 3) K) ![c, d]
hAB : (Nat.succ 0).succ + (Nat.succ 0).succ ≤ 3
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K c hc)
hbc : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K d hd)
hbd : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K d hd)
h :
  Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) a : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          b :
        Fin 3 → K)
      (0 : Fin 3 → K) ∨
    Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) c : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          d :
        Fin 3 → K)
      (0 : Fin 3 → K)
⊢ Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨
    Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K c hc) (Projectivization.mk K d hd)

Tactic:
rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K c hc)
hbc : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K d hd)
hbd : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K d hd)
⊢ Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) a : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          b :
        Fin 3 → K)
      (0 : Fin 3 → K) ∨
    Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) c : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          d :
        Fin 3 → K)
      (0 : Fin 3 → K)

Tactic:
crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a : Fin 3 → K
ha : a ≠ 0
b : Fin 3 → K
hb : b ≠ 0
c : Fin 3 → K
hc : c ≠ 0
hac : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K c hc)
hbc : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K c hc)
d : Fin 3 → K
hd : d ≠ 0
had : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K d hd)
hbd : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K d hd)
⊢ Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) a : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          b :
        Fin 3 → K)
      (0 : Fin 3 → K) ∨
    Eq (α := Fin 3 → K)
      ((((crossProduct : (a : Fin 3 → K) → (Fin 3 → K) →ₗ[K] Fin 3 → K) c : (Fin 3 → K) →ₗ[K] Fin 3 → K) :
            (a : Fin 3 → K) → Fin 3 → K)
          d :
        Fin 3 → K)
      (0 : Fin 3 → K)

Tactic:
exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
had : orthogonal (Projectivization.mk K a ha) d
b : Fin 3 → K
hb : b ≠ 0
hbd : orthogonal (Projectivization.mk K b hb) d
c : Fin 3 → K
hc : c ≠ 0
hac : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K c hc)
hbc : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K c hc)
h :
  ∀ (d : Fin 3 → K) (hd : d ≠ 0) (had : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K d hd))
    (hbd : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K d hd)),
    Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨
      Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K c hc) (Projectivization.mk K d hd)
⊢ Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨ Projectivization.mk K c hc = d

Tactic:
induction d with | h d hd =>
  rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
  exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
c d : ℙ K (Fin 3 → K)
a : Fin 3 → K
ha : a ≠ 0
hac : orthogonal (Projectivization.mk K a ha) c
had : orthogonal (Projectivization.mk K a ha) d
b : Fin 3 → K
hb : b ≠ 0
hbc : orthogonal (Projectivization.mk K b hb) c
hbd : orthogonal (Projectivization.mk K b hb) d
h :
  ∀ (c : Fin 3 → K) (hc : c ≠ 0) (hac : orthogonal (Projectivization.mk K a ha) (Projectivization.mk K c hc))
    (hbc : orthogonal (Projectivization.mk K b hb) (Projectivization.mk K c hc)),
    Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨ Projectivization.mk K c hc = d
⊢ Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨ c = d

Tactic:
induction c with | h c hc =>
  induction d with | h d hd =>
  rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
  exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
b c d : ℙ K (Fin 3 → K)
hbc : b.orthogonal c
hbd : b.orthogonal d
a : Fin 3 → K
ha : a ≠ 0
hac : orthogonal (Projectivization.mk K a ha) c
had : orthogonal (Projectivization.mk K a ha) d
h :
  ∀ (b : Fin 3 → K) (hb : b ≠ 0) (hbc : orthogonal (Projectivization.mk K b hb) c)
    (hbd : orthogonal (Projectivization.mk K b hb) d),
    Eq (α := ℙ K (Fin 3 → K)) (Projectivization.mk K a ha) (Projectivization.mk K b hb) ∨ c = d
⊢ Projectivization.mk K a ha = b ∨ c = d

Tactic:
induction b with | h b hb =>
  induction c with | h c hc =>
  induction d with | h d hd =>
  rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
  exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
a b c d : ℙ K (Fin 3 → K)
hac : a.orthogonal c
hbc : b.orthogonal c
had : a.orthogonal d
hbd : b.orthogonal d
h :
  ∀ (a : Fin 3 → K) (ha : a ≠ 0) (hac : orthogonal (Projectivization.mk K a ha) c)
    (had : orthogonal (Projectivization.mk K a ha) d), Projectivization.mk K a ha = b ∨ c = d
⊢ a = b ∨ c = d

Tactic:
induction a with | h a ha =>
  induction b with | h b hb =>
  induction c with | h c hc =>
  induction d with | h d hd =>
  rw [mk_eq_mk_iff_crossProduct_eq_zero, mk_eq_mk_iff_crossProduct_eq_zero]
  exact crossProduct_eq_zero_of_dotProduct_eq_zero hac hbc had hbd

Premises used: Projectivization.mk_eq_mk_iff_crossProduct_eq_zero
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
⊢ Nondegenerate (ℙ K (Fin 3 → K)) (ℙ K (Fin 3 → K))

Tactic:
{ exists_point := exists_not_orthogonal_self
    exists_line := exists_not_self_orthogonal
    eq_or_eq := eq_or_eq_of_orthogonal }

Premises used: Configuration.ofField.eq_or_eq_of_orthogonal, Projectivization.exists_not_orthogonal_self, Projectivization.exists_not_self_orthogonal, Configuration.Nondegenerate.mk
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
v w : ℙ K (Fin 3 → K)
_ : v ≠ w → ℙ K (Fin 3 → K)
⊢ v ≠ w → ℙ K (Fin 3 → K)

Tactic:
_
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
v w : ℙ K (Fin 3 → K)
h : v ≠ w
⊢ ℙ K (Fin 3 → K)

Tactic:
exact cross v w

Premises used: Projectivization.cross
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ ∃ (p₁ : ℙ K (Fin 3 → K)) (p₂ : ℙ K (Fin 3 → K)) (p₃ : ℙ K (Fin 3 → K)) (l₁ : ℙ K (Fin 3 → K)) (l₂ : ℙ K (Fin 3 → K))
    (l₃ : ℙ K (Fin 3 → K)), p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃

Tactic:
⟨mk K ![0, 1, 1] ?_, mk K ![1, 0, 0] ?_, mk K ![1, 0, 1] ?_, mk K ![1, 0, 0] ?_,
        mk K ![0, 1, 0] ?_, mk K ![0, 0, 1] ?_, ?_⟩

Premises used: Projectivization.mk, Exists.intro, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
refine_1 : Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 1, 1] 0
refine_2 : Ne.{u_3 + 1} (α := Fin 3 → K) ![1, 0, 0] 0
refine_3 : Ne.{u_3 + 1} (α := Fin 3 → K) ![1, 0, 1] 0
refine_4 : Ne.{u_3 + 1} (α := Fin 3 → K) ![1, 0, 0] 0
refine_5 : Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 1, 0] 0
refine_6 : Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 0, 1] 0
refine_7 :
  Projectivization.mk K ![0, 1, 1] ⋯ ∉ Projectivization.mk K ![0, 1, 0] ⋯ ∧
    Projectivization.mk K ![0, 1, 1] ⋯ ∉ Projectivization.mk K ![0, 0, 1] ⋯ ∧
      Projectivization.mk K ![1, 0, 0] ⋯ ∉ Projectivization.mk K ![1, 0, 0] ⋯ ∧
        Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 1, 0] ⋯)
            (Projectivization.mk K ![1, 0, 0] ⋯) ∧
          Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 0, 1] ⋯)
              (Projectivization.mk K ![1, 0, 0] ⋯) ∧
            Projectivization.mk K ![1, 0, 1] ⋯ ∉ Projectivization.mk K ![1, 0, 0] ⋯ ∧
              Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 1, 0] ⋯)
                  (Projectivization.mk K ![1, 0, 1] ⋯) ∧
                Projectivization.mk K ![1, 0, 1] ⋯ ∉ Projectivization.mk K ![0, 0, 1] ⋯
⊢ ∃ (p₁ : ℙ K (Fin 3 → K)) (p₂ : ℙ K (Fin 3 → K)) (p₃ : ℙ K (Fin 3 → K)) (l₁ : ℙ K (Fin 3 → K)) (l₂ : ℙ K (Fin 3 → K))
    (l₃ : ℙ K (Fin 3 → K)), p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃

Tactic:
refine ⟨mk K ![0, 1, 1] ?_, mk K ![1, 0, 0] ?_, mk K ![1, 0, 1] ?_, mk K ![1, 0, 0] ?_,
        mk K ![0, 1, 0] ?_, mk K ![0, 0, 1] ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 1, 1] 0

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Ne.{u_3 + 1} (α := Fin 3 → K) ![1, 0, 0] 0

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Ne.{u_3 + 1} (α := Fin 3 → K) ![1, 0, 1] 0

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 1, 0] 0

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Ne.{u_3 + 1} (α := Fin 3 → K) ![0, 0, 1] 0

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
K : Type u_3
inst_1 : Field K
inst_2 : DecidableEq K
⊢ Projectivization.mk K ![0, 1, 1] ⋯ ∉ Projectivization.mk K ![0, 1, 0] ⋯ ∧
    Projectivization.mk K ![0, 1, 1] ⋯ ∉ Projectivization.mk K ![0, 0, 1] ⋯ ∧
      Projectivization.mk K ![1, 0, 0] ⋯ ∉ Projectivization.mk K ![1, 0, 0] ⋯ ∧
        Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 1, 0] ⋯)
            (Projectivization.mk K ![1, 0, 0] ⋯) ∧
          Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 0, 1] ⋯)
              (Projectivization.mk K ![1, 0, 0] ⋯) ∧
            Projectivization.mk K ![1, 0, 1] ⋯ ∉ Projectivization.mk K ![1, 0, 0] ⋯ ∧
              Membership.mem (γ := ℙ K (Fin 3 → K)) (Projectivization.mk K ![0, 1, 0] ⋯)
                  (Projectivization.mk K ![1, 0, 1] ⋯) ∧
                Projectivization.mk K ![1, 0, 1] ⋯ ∉ Projectivization.mk K ![0, 0, 1] ⋯

Tactic:
simp [mem_iff, orthogonal_mk]

Premises used: Projectivization.orthogonal_mk, Configuration.ofField.mem_iff
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
f : Perm α
⊢ f ∈ derangements α ↔ Eq (α := Set α) (fixedPoints (⇑f : (a : α) → α)) ∅

Tactic:
Set.eq_empty_iff_forall_notMem.symm

Premises used: Set.Mem, setOf, Function.fixedPoints, Set.eq_empty_iff_forall_notMem, Function.IsFixedPt, derangements, Iff.symm
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
f : Perm α
b : α
⊢ (f : (a : α) → α) b ≠ b ↔
    Ne.{u_2 + 1} (α := β)
      ((((e.permCongr : (a : Perm α) → Perm β) f : Perm β) : (a : β) → β) ((e : (a : α) → β) b : β) : β)
      ((e : (a : α) → β) b : β)

Tactic:
simp only [ne_eq, permCongr_apply, symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: Equiv.symm_apply_apply, EmbeddingLike.apply_eq_iff_eq, ne_eq, Equiv.permCongr_apply
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
refine_1 :
  ∀ (f : Perm (Subtype p)) (hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f) (a : α)
    (hfa :
      Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a)
    (ha : p a), False
refine_2 :
  ∀ (f : Perm (Subtype p)),
    (∀ (a : α),
        Membership.mem (γ := Set α)
            (fixedPoints
              (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                          (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                        f) :
                    Perm α) :
                (a : α) → α))
            a →
          ¬p a) →
      Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
⊢ (↑(derangements (Subtype p)) : Type u_1) ≃
    { f : { f : Perm α // ∀ (a : α), ¬p a → Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a } //
      ∀ (a : α), Membership.mem (γ := Set α) (fixedPoints (⇑(↑f : Perm α) : (a : α) → α)) a → ¬p a }

Tactic:
refine (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => ?_, ?_⟩

Premises used: Equiv.subtypeEquiv, Iff.intro, Equiv.Perm.subtypeEquivSubtypePerm
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
hfa :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
ha : p a
⊢ False

Tactic:
hf ⟨a, ha⟩ (Subtype.ext ?_)

Premises used: Subtype.mk, Subtype.ext
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
hfa :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
ha : p a
refine_1 : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = (↑(Subtype.mk (p := p) a ha) : α)
⊢ False

Tactic:
refine hf ⟨a, ha⟩ (Subtype.ext ?_)

Premises used: Subtype.mk, Subtype.ext
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
hfa :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
ha : p a
⊢ (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = a

Tactic:
simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
        Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Function.mem_fixedPoints, Equiv.coe_fn_mk, Function.IsFixedPt, Equiv.Perm.subtypeEquivSubtypePerm
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf : Membership.mem (γ := Set (Perm (Subtype p))) (derangements (Subtype p)) f
a : α
ha : p a
hfa : (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = a
⊢ (↑((f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha)) : α) = (↑(Subtype.mk (p := p) a ha) : α)

Tactic:
assumption
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a →
      ¬p a
a : α
ha : p a
hfa : (f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha) = Subtype.mk (p := p) a ha
⊢ False

Tactic:
hf _ ?_ ha
-- Module: Mathlib.Combinatorics.Derangements.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : Perm (Subtype p)
hf :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (fixedPoints
          (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                      (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                    f) :
                Perm α) :
            (a : α) → α))
        a →
      ¬p a
a : α
ha : p a
hfa : (f : (a : Subtype p) → Subtype p) (Subtype.mk (p := p) a ha) = Subtype.mk (p := p) a ha
refine_2 :
  Membership.mem (γ := Set α)
    (fixedPoints
      (⇑(↑((Perm.subtypeEquivSubtypePerm p :
                  (a : Perm (Subtype p)) → { f : Perm α // ∀ (a : α), ¬p a → (f : (a : α) → α) a = a })
                f) :
            Perm α) :
        (a : α) → α))
    a
⊢ False

Tactic:
refine hf _ ?_ ha