awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
by_contra! : ∀ (h : j < i), False
⊢ i ≤ j

Tactic:
by_contra! h
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
h : j < i
⊢ i = j

Tactic:
σ.injective (le_antisymm hij (hσ h.le))

Premises used: LT.lt.le, le_antisymm, Equiv.injective
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
h : j < i
⊢ LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n)

Tactic:
obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))

Premises used: LT.lt.le, le_antisymm, Equiv.injective, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i j : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
h : j < i
hij₁ : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n)
⊢ i < i

Tactic:
obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))

Premises used: LT.lt.le, le_antisymm, Equiv.injective, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h_1 : a ≠ b
σ : Equiv.Perm (Fin n)
h_2 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
i : Fin n
hij : LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n)
h : i < i
⊢ False

Tactic:
simp only [lt_self_iff_false] at h

Premises used: lt_self_iff_false
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
⊢ Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)

Tactic:
have hσ' : Monotone σ.symm := fun i j hij ↦ by
    obtain ⟨i, rfl⟩ := σ.surjective i
    obtain ⟨j, rfl⟩ := σ.surjective j
    simp only [Equiv.symm_apply_apply]
    by_contra! h
    obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
    simp only [lt_self_iff_false] at h
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
H : ∀ (i : Fin n), Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((1 : (a : Fin n) → Fin n) i : Fin n)
⊢ σ = 1

Tactic:
ext i : 1
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
i : Fin n
⊢ Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((1 : (a : Fin n) → Fin n) i : Fin n)

Tactic:
DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: DFunLike.congr_fun, Equiv.toOrderIso, Subsingleton.elim, OrderIso.refl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
i : Fin n
⊢ Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((1 : (a : Fin n) → Fin n) i : Fin n)

Tactic:
exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: DFunLike.congr_fun, Equiv.toOrderIso, Subsingleton.elim, OrderIso.refl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
⊢ Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1

Tactic:
obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
⊢ ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0

Tactic:
obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
⊢ Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))

Tactic:
obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this₁ :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
⊢ Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)

Tactic:
obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ σ
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((σ : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑σ : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm σ) : (a : Fin n) → Fin n)
x₁ : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h'₁ :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this₁ :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
hσ₁ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
⊢ Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm 1) : (a : Fin n) → Fin n)

Tactic:
obtain rfl : σ = 1 := by
    ext i : 1
    exact DFunLike.congr_fun (Subsingleton.elim (σ.toOrderIso hσ hσ') (OrderIso.refl _)) i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_1 : Fin n,
        (f ((a : (a : Fin n) → ι) x_1) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_1 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm 1) : (a : Fin n) → Fin n)
h₁ : ∀ (x : Fin n), Eq (α := ι) ((a : (a : Fin n) → ι) x : ι) ((b : (a : Fin n) → ι) x : ι)
⊢ a = b

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → Eq.{u_1 + 1} (α := R) ((f i : (a : M) → R) (x j) : R) (0 : R)
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
h_1 : Membership.mem (γ := Finset (Equiv.Perm (Fin n))) Finset.univ 1
h' :
  ¬Eq.{u_1 + 1} (α := R)
      (∏ x_2 : Fin n,
        (f ((a : (a : Fin n) → ι) x_2) : (a : M) → R)
          (x ((b : (a : Fin n) → ι) ((1 : (a : Fin n) → Fin n) x_2 : Fin n))))
      0
this :
  Eq (α := (a : Fin n) → ι) (⇑a : (a : Fin n) → ι)
    (Function.comp (β := Fin n) (⇑b : (a : Fin n) → ι) (⇑1 : (a : Fin n) → Fin n))
hσ : Monotone (α := Fin n) (β := Fin n) (⇑1 : (a : Fin n) → Fin n)
hσ' : Monotone (α := Fin n) (β := Fin n) (⇑(Equiv.symm 1) : (a : Fin n) → Fin n)
x_1 : Fin n
⊢ Eq (α := ι) ((a : (a : Fin n) → ι) x_1 : ι) ((b : (a : Fin n) → ι) x_1 : ι)

Tactic:
apply congr_fun this

Premises used: congr_fun
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
ι : Type w
inst_3 : FiniteDimensional K V
v : ι → V
h : LinearIndependent K v
⊢ #ι < ℵ₀

Tactic:
h.lt_aleph0_of_finite

Premises used: LinearIndependent.lt_aleph0_of_finite
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
⊢ let bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S;
  bS = Basis.ofVectorSpace K ↥S

Tactic:
set bS := Basis.ofVectorSpace K S with bS_eq

Premises used: Membership.mem, Subtype, Module.Basis.ofVectorSpace
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ Disjoint
    (span K
      (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v))
        (⇑bS : (a : (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v)) → ↥S)))
    S.subtype.ker

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
simpa [bS] using bS.linearIndependent.linearIndepOn_id.image
      (f := Submodule.subtype S) (by simp)

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent, LinearIndepOn.image
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))

Tactic:
have : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K S) := by
    simpa [bS] using bS.linearIndependent.linearIndepOn_id.image
      (f := Submodule.subtype S) (by simp)
-- Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic
Goal:
K : Type u
V : Type v
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
S : Submodule K V
h : finrank.{u, v} K ↥S = finrank K V
bS : Basis.{v, u, v} (↑(Basis.ofVectorSpaceIndex K ↥S) : Type v) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this :
  LinearIndepOn.{v, u, v} (ι := V) K id
    (Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
⊢ let b :=
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this;
  b =
    Basis.extend (s := Set.image (α := ↥S) (Subtype.val (p := fun (x : V) ↦ x ∈ S)) (Basis.ofVectorSpaceIndex K ↥S))
      this

Tactic:
set b := Basis.extend this with b_eq

Premises used: Module.Basis.extend