awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
rw :
  Nat.card.{u_1} { x : P // x ∈ (↑l : L) } - Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p } =
    order P L
⊢ Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L

Tactic:
rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
        Nat.card_eq_fintype_card]

Premises used: Fintype.card_congr, Membership.mem, Ne, Equiv.subtypeSubtypeEquivSubtypeInter, Subtype.val, Fintype.card_subtype_compl, Eq, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
⊢ Nat.card.{u_1} { x : P // x ∈ (↑l : L) } - Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p } =
    order P L

Tactic:
tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)

Premises used: tsub_eq_of_eq_add, Configuration.ProjectivePlane.pointCount_eq, Subtype.val, Eq.trans
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
refine : order P L + 1 = order P L + Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p }
⊢ Nat.card.{u_1} { x : P // x ∈ (↑l : L) } - Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p } =
    order P L

Tactic:
refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)

Premises used: tsub_eq_of_eq_add, Configuration.ProjectivePlane.pointCount_eq, Subtype.val, Eq.trans
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
l : { l : L // p ∈ l }
⊢ order P L +
      Fintype.card.{u_1} { x : { q : P // q ∈ (↑l : L) } // x = Subtype.mk (p := fun (q : P) ↦ q ∈ (↑l : L)) p ⋯ } =
    order P L + Fintype.card.{u_1} { x : { x : P // x ∈ (↑l : L) } // (↑x : P) = p }

Tactic:
simp_rw [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
⊢ ∀ (l : { l : L // p ∈ l }), Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L

Tactic:
have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L := by
      intro l
      rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
        Nat.card_eq_fintype_card]
      refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)
      rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
      simp_rw [Subtype.ext_iff]
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l : L // p ∈ l }), Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L
intro : Fintype.card.{u_2} { l : L // p ∈ l } • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

Tactic:
simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]

Premises used: Fintype.card_congr, Finset.card_univ, Fintype.card_sigma, Finset.sum_const
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
h2 : ∀ (l : { l : L // p ∈ l }), Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L
intro : Nat.card.{u_2} { l : L // p ∈ l } • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₁ : lineCount L p • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₂ : (order P L + 1) • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₃ : (order P L + 1) * order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₄ : order P L * order P L + order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₅ intro₆ : order P L * order P L + order P L + 1 = order P L * order P L + order P L + 1
⊢ Fintype.card.{u_2} { l : L // p ∈ l } • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

Tactic:
rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]

Premises used: Configuration.lineCount, sq, Configuration.ProjectivePlane.lineCount_eq, Nat.succ_mul, smul_eq_mul, Nat.card_eq_fintype_card
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Fintype P
inst_3 : Finite L
val : Fintype L
p : P
ϕ : { q : P // q ≠ p } ≃ (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p } :=
  {
    toFun := fun (q : { q : P // q ≠ p }) ↦
      Sigma.mk (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })
        (Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯)
        (Subtype.mk (p := fun (q_1 : P) ↦
          q_1 ∈ (↑(Subtype.mk (p := fun (l : L) ↦ p ∈ l) (@mkLine _ _ inst _ _ _ ⋯) ⋯) : L) ∧ q_1 ≠ p) (↑q : P) ⋯),
    invFun := fun (lq : (l : { l : L // p ∈ l }) × { q : P // q ∈ (↑l : L) ∧ q ≠ p }) ↦
      Subtype.mk (p := fun (q : P) ↦ q ≠ p)
        (↑(lq.snd (β := fun (l : { l : L // p ∈ l }) ↦ { q : P // q ∈ (↑l : L) ∧ q ≠ p })) : P) ⋯,
    left_inv := ⋯, right_inv := ⋯ }
have : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
intro :
  ∀ (h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P),
    Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
have₁ : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P
intro₁ intro₂ :
  ∀ (h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P),
    Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₃ :
  ∀ (h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P)
    (h2 : ∀ (l : { l : L // p ∈ l }), Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L),
    Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
intro₄ :
  ∀ (h1 : Fintype.card.{u_1} { q : P // q ≠ p } + 1 = Fintype.card P)
    (h2 : ∀ (l : { l : L // p ∈ l }), Fintype.card.{u_1} { q : P // q ∈ (↑l : L) ∧ q ≠ p } = order P L),
    Fintype.card.{u_2} { l : L // p ∈ l } • order P L + 1 = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1
⊢ Fintype.card P = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

Tactic:
classical
    have h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P := by
      apply (eq_tsub_iff_add_eq_of_le (Nat.succ_le_of_lt (Fintype.card_pos_iff.mpr ⟨p⟩))).mp
      convert! (Fintype.card_subtype_compl _).trans (congr_arg _ (Fintype.card_subtype_eq p))
    have h2 : ∀ l : { l : L // p ∈ l }, Fintype.card { q // q ∈ l.1 ∧ q ≠ p } = order P L := by
      intro l
      rw [← Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (· ∈ l.val) (· ≠ p)),
        Fintype.card_subtype_compl fun x : Subtype (· ∈ l.val) => x.val = p, ←
        Nat.card_eq_fintype_card]
      refine tsub_eq_of_eq_add ((pointCount_eq P l.1).trans ?_)
      rw [← Fintype.card_subtype_eq (⟨p, l.2⟩ : { q : P // q ∈ l.1 })]
      simp_rw [Subtype.ext_iff]
    simp_rw [← h1, Fintype.card_congr ϕ, Fintype.card_sigma, h2, Finset.sum_const, Finset.card_univ]
    rw [← Nat.card_eq_fintype_card, ← lineCount, lineCount_eq, smul_eq_mul, Nat.succ_mul, sq]

Premises used: Finset.card_univ, Configuration.lineCount, Fintype.card_sigma, sq, Configuration.ProjectivePlane.lineCount_eq, Nat.succ_mul, smul_eq_mul, Nat.card_eq_fintype_card, Finset.sum_const
-- Module: Mathlib.Combinatorics.Configuration
Goal:
P : Type u_1
L : Type u_2
inst : Membership P L
inst_1 : ProjectivePlane P L
inst_2 : Finite P
inst_3 : Fintype L
⊢ Fintype.card L = HPow.hPow (β := ℕ) (order P L) 2 + order P L + 1

Tactic:
(card_points (Dual L) (Dual P)).trans (congr_arg (fun n => n ^ 2 + n + 1) (Dual.order P L))

Premises used: Configuration.Dual, Configuration.ProjectivePlane.card_points, congr_arg, HPow.hPow, HAdd.hAdd, Configuration.ProjectivePlane.Dual.order, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Combinatorics.Configuration
Goal:
K : Type u_3
inst : Field K
v w : ℙ K (Fin 3 → K)
⊢ v ∈ w ↔ v.orthogonal w

Tactic:
Iff.rfl

Premises used: Iff.rfl, Projectivization.orthogonal
-- 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
by_contra :
  ∀
    (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))),
    False
⊢ 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:
by_contra h
-- 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 :
  ¬(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))
⊢ LinearIndependent K ![a, b] ∧ LinearIndependent K ![c, d]

Tactic:
simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h

Premises used: ne_eq, not_or, crossProduct_ne_zero_iff_linearIndependent
-- 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 K ![a, b] ∧ LinearIndependent K ![c, d]
⊢ 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]))

Tactic:
rw [← Matrix.of_row (![a, b]), ← Matrix.of_row (![c, d])] at h

Premises used: Matrix.vecEmpty, Matrix.of_row, Matrix.vecCons
-- 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₁ : ∀ (i j : Fin 2), (A * Bᵀ) i j = 0 i j
⊢ A * Bᵀ = 0

Tactic:
ext i j
-- 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]
i j : Fin 2
a₁ : (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
a₂ : (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ (A * Bᵀ) i j = 0 i j

Tactic:
fin_cases i
-- 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]
j : Fin 2
a₁ :
  (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₂ :
  (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j = 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- 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]
j : Fin 2
a₁ :
  (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₂ :
  (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, ⋯⟩)
⊢ (A * Bᵀ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j = 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- 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) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

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ᵀ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((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ᵀ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
assumption