awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ Eq (α := (t : (i : ι) → κ i) → N t)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i) :
      (t : (i : ι) → κ i) → N t)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) : (j : (i : ι) → κ i) → N j)
have h : ∀ (q : (i : ι) → κ i),
  Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
have h : Eq.{uN + 1} (α := N p)
  ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
    (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) p)
  (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) p)
Tactic: obtain rfl | hpq := eq_or_ne p q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
h :
  Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) p)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) p)
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
have h₁ : ∀ (hpq : p ≠ q),
  Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
Tactic: obtain rfl | hpq := eq_or_ne p q
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    (Pi.single (M := N) p ((f p : (a : (i : ι) → M i (p i)) → N p) m) q)
have h : Eq.{uN + 1} (α := N q)
  ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
    (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
  0
Tactic: rw [Pi.single_eq_of_ne' hpq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (hypothesis)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0
have hpq₁ : ∃ (a : ι), p a ≠ q a
Tactic: rw [Function.ne_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : ∃ (a : ι), p a ≠ q a
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0
have h : ∀ (i : ι) (hpqi : p i ≠ q i),
  Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0
Tactic: obtain ⟨i, hpqi⟩ := hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ Eq.{uN + 1} (α := N q)
    ((piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      (fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) q)
    0
have h : Eq.{uM + 1} (α := M i (q i)) ((fun (i : ι) ↦ Pi.single (M := M i) (p i) (m i)) i (q i)) 0
Tactic: apply (f q).map_coord_zero i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
⊢ Eq (α := (t : (i : ι) → κ i) → N t)
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x :
      (t : (i : ι) → κ i) → N t)
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) : (j : (i : ι) → κ i) → N j)
have h : ∀ (p' : (i : ι) → κ i),
  Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
Tactic: ext p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
⊢ Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
have h : Eq.{uN + 1} (α := N p)
  ((piFamily (κ := κ) (M := M) (N := N)
          (Pi.single (M := fun (p : (i : ι) → κ i) ↦ MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p))
            p f) :
        (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
      x p :
    N p)
  (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p : N p)
Tactic: obtain rfl | hp := eq_or_ne p p'
Cleared hypotheses: p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Fintype ι
inst_6 : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
x : (i : ι) → (j : κ i) → M i j
p' : (i : ι) → κ i
h :
  Eq.{uN + 1} (α := N p)
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p :
      N p)
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p : N p)
⊢ Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
have h₁ : ∀ (hp : p ≠ p'),
  Eq.{uN + 1} (α := N p')
    ((piFamily (κ := κ) (M := M) (N := N)
            (Pi.single (M := fun (p : (i : ι) → κ i) ↦
              MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)) p f) :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x p' :
      N p')
    (Pi.single (M := N) p ((f : (a : (i : ι) → M i (p i)) → N p) fun (i : ι) ↦ x i (p i)) p' : N p')
Tactic: obtain rfl | hp := eq_or_ne p p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
⊢ Eq (α := MultilinearMap R (fun (i : ι) ↦ (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t))
    (piFamily (κ := κ) (M := M) (N := N) 0) 0
have H : ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
  Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) 0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 :
      N x_1)
    ((0 : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 : N x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
⊢ piFamily (κ := κ) (M := M) (N := N) (f + g) =
    piFamily (κ := κ) (M := M) (N := N) f + piFamily (κ := κ) (M := M) (N := N) g
have H : ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
  Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) (f + g) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
        x_1 :
      N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) f + piFamily (κ := κ) (M := M) (N := N) g :
          (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t)
        x x_1 :
      N x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Pi (goal)
Goal:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst : Semiring R
inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst_3 : (i : ι) → (k : κ i) → Module.{uR, uM} R (M i k)
inst_4 : (p : (i : ι) → κ i) → Module.{uR, uN} R (N p)
inst_5 : Monoid S
inst_6 : (p : (i : ι) → κ i) → DistribMulAction.{uS, uN} S (N p)
inst_7 : ∀ (p : (i : ι) → κ i), SMulCommClass.{uR, uS, uN} R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap.{uR, uι, uM, uN} R (fun (i : ι) ↦ M i (p i)) (N p)
⊢ piFamily (κ := κ) (M := M) (N := N) (s • f) = s • piFamily (κ := κ) (M := M) (N := N) f
have H : ∀ (x : (i : ι) → (j : κ i) → M i j) (x_1 : (i : ι) → κ i),
  Eq.{uN + 1} (α := N x_1)
    ((piFamily (κ := κ) (M := M) (N := N) (s • f) : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x
        x_1 :
      N x_1)
    ((s • piFamily (κ := κ) (M := M) (N := N) f : (a : (i : ι) → (j : κ i) → M i j) → (t : (i : ι) → κ i) → N t) x x_1 :
      N x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (map ι (LinearEquiv.refl R M)) (Equiv.refl (Orientation R M ι))
have rw : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domLCongr R R ι R (LinearEquiv.refl R M)))
  (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domLCongr R R ι R (LinearEquiv.refl R M)))
    (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (map ι (LinearEquiv.refl R M)) (Equiv.refl (Orientation R M ι))
have rw₁ : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
  (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domLCongr R R ι R (LinearEquiv.refl R M)))
    (Equiv.refl (Orientation R M ι))
rw₁ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
    (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (map ι (LinearEquiv.refl R M)) (Equiv.refl (Orientation R M ι))
have rw₂ : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Equiv.refl (Ray R (M [⋀^ι]→ₗ[R] R))) (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (reindex R M (Equiv.refl ι)) (Equiv.refl (Orientation R M ι))
have rw : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domDomCongrₗ R (Equiv.refl ι)))
  (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domDomCongrₗ R (Equiv.refl ι)))
    (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (reindex R M (Equiv.refl ι)) (Equiv.refl (Orientation R M ι))
have rw₁ : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
  (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domDomCongrₗ R (Equiv.refl ι)))
    (Equiv.refl (Orientation R M ι))
rw₁ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
    (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (reindex R M (Equiv.refl ι)) (Equiv.refl (Orientation R M ι))
have rw₂ : Eq (α := Orientation R M ι ≃ Orientation R M ι) (Equiv.refl (Ray R (M [⋀^ι]→ₗ[R] R))) (Equiv.refl (Orientation R M ι))
Tactic: rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ Eq (α := Orientation R M ι)
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) (rayOfNeZero R g hg) : Orientation R M ι)
    (rayOfNeZero R g hg : Ray R (M [⋀^ι]→ₗ[R] R))
have h : Eq (α := Orientation R M ι) (rayOfNeZero R (g.compLinearMap (↑f.symm : M →ₗ[R] M)) sorry) (rayOfNeZero R g hg)
Tactic: rw [Orientation.map_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R (g.compLinearMap (↑f.symm : M →ₗ[R] M)) ⋯) (rayOfNeZero R g hg)
have h : g.compLinearMap (↑f.symm : M →ₗ[R] M) = g
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ g.compLinearMap (↑f.symm : M →ₗ[R] M) = g
have h : ∀ (i : ι → M),
  Eq.{u_1 + 1} (α := R) ((g.compLinearMap (↑f.symm : M →ₗ[R] M) : (a : ι → M) → R) i : R) ((g : (a : ι → M) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ Eq.{u_1 + 1} (α := R) ((g.compLinearMap (↑f.symm : M →ₗ[R] M) : (a : ι → M) → R) i : R) ((g : (a : ι → M) → R) i : R)
have h : Eq.{u_1 + 1} (α := R) ((g : (a : ι → M) → R) fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1) : R)
  ((g : (a : ι → M) → R) i : R)
Tactic: rw [AlternatingMap.compLinearMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ Eq.{u_1 + 1} (α := R) ((g : (a : ι → M) → R) fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1) : R)
    ((g : (a : ι → M) → R) i : R)
have h : (fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1)) = i
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x
have h : ∀ (g : M [⋀^ι]→ₗ[R] R) (hg : g ≠ 0),
  Eq (α := Orientation R M ι)
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) (rayOfNeZero R g hg) : Orientation R M ι)
    (rayOfNeZero R g hg : Ray R (M [⋀^ι]→ₗ[R] R))
Tactic: induction x using Module.Ray.ind with | h g hg =>
  rw [Orientation.map_apply]
  congr
  ext i
  rw [AlternatingMap.compLinearMap_apply]
  congr
  simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]
Cleared hypotheses: x