m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∏ x : o, ∑ x_1 : Perm n, ↑↑(↑sign x_1) * ∏ x_2 : n, M x (↑x_1 x_2) x_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ det (blockDiagonal M) = ∏ k : o, det (M k)
simp_rw [det_apply']
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ p in pi univ fun x => univ,
      ∏ x in attach univ, ↑↑(↑sign (p ↑x (_ : ↑x ∈ univ))) * ∏ x_1 : n, M (↑x) (↑(p ↑x (_ : ↑x ∈ univ)) x_1) x_1
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∏ x : o, ∑ x_1 : Perm n, ↑↑(↑sign x_1) * ∏ x_2 : n, M x (↑x_1 x_2) x_2
rw [Finset.prod_sum]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ p in pi univ fun x => univ,
      ∏ x in attach univ, ↑↑(↑sign (p ↑x (_ : ↑x ∈ univ))) * ∏ x_1 : n, M (↑x) (↑(p ↑x (_ : ↑x ∈ univ)) x_1) x_1
simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
let preserving_snd : Finset (Equiv.Perm (n × o)) :=
  Finset.univ.filter fun σ => ∀ x, (σ x).snd = x.snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
have mem_preserving_snd :
  ∀ {σ : Equiv.Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ x, (σ x).snd = x.snd := fun {σ} =>
  Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∑ x in preserving_snd, ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (x : Perm (n × o)), x ∈ univ → ¬x ∈ preserving_snd → ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 = 0
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∑ x : Perm (n × o), ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2
rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a : (k : o) → k ∈ univ → Perm n) (ha : a ∈ univ),
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha ∈ preserving_snd

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a : (k : o) → k ∈ univ → Perm n) (ha : a ∈ univ),
    ∏ x : o,
        ↑↑(↑sign (a x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ))) *
          ∏ x_1 : n, M x (↑(a x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
      ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha)) *
        ∏ x : n × o, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha) x) x

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a₁ a₂ : (k : o) → k ∈ univ → Perm n) (ha₁ : a₁ ∈ univ) (ha₂ : a₂ ∈ univ),
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a₁ ha₁ =
        (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a₂ ha₂ →
      a₁ = a₂

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (b : n × o ≃ n × o), b ∈ preserving_snd → ∃ a ha, b = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (x : Perm (n × o)), x ∈ univ → ¬x ∈ preserving_snd → ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 = 0
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∑ x in preserving_snd, ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 =
    ∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        ↑↑(↑sign (x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ))) *
          ∏ x_2 : n, M x_1 (↑(x x_1 (_ : ↑{ val := x_1, property := (_ : x_1 ∈ univ) } ∈ univ)) x_2) x_2

m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (x : Perm (n × o)), x ∈ univ → ¬x ∈ preserving_snd → ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 = 0
rw [(Finset.sum_bij
      (fun (σ : ∀ k : o, k ∈ Finset.univ → Equiv.Perm n) _ =>
        prodCongrLeft fun k => σ k (Finset.mem_univ k))
      _ _ _ _).symm]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝ ∈ preserving_snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a : (k : o) → k ∈ univ → Perm n) (ha : a ∈ univ),
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha ∈ preserving_snd
intro σ _
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) x).snd = x.snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝ ∈ preserving_snd
rw [mem_preserving_snd]
case mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
fst✝ : n
x : o
⊢ (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) (fst✝, x)).snd = (fst✝, x).snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∀ (x : n × o), (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) x).snd = x.snd
rintro ⟨-, x⟩
no goals
case mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
fst✝ : n
x : o
⊢ (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) (fst✝, x)).snd = (fst✝, x).snd
simp only [prodCongrLeft_apply]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∏ x : o,
      ↑↑(↑sign (σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ))) *
        ∏ x_1 : n, M x (↑(σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
    ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝)) *
      ∏ x : n × o, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) x) x
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a : (k : o) → k ∈ univ → Perm n) (ha : a ∈ univ),
    ∏ x : o,
        ↑↑(↑sign (a x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ))) *
          ∏ x_1 : n, M x (↑(a x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
      ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha)) *
        ∏ x : n × o, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha) x) x
intro σ _
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (∏ x : o, ↑↑(↑sign (σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)))) *
      ∏ x : o, ∏ x_1 : n, M x (↑(σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
    ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝)) *
      ∏ y : o, ∏ x : n, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) (x, y)) (x, y)
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ ∏ x : o,
      ↑↑(↑sign (σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ))) *
        ∏ x_1 : n, M x (↑(σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
    ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝)) *
      ∏ x : n × o, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) x) x
rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]
no goals
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : (k : o) → k ∈ univ → Perm n
ha✝ : σ ∈ univ
⊢ (∏ x : o, ↑↑(↑sign (σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)))) *
      ∏ x : o, ∏ x_1 : n, M x (↑(σ x (_ : ↑{ val := x, property := (_ : x ∈ univ) } ∈ univ)) x_1) x_1 =
    ↑↑(↑sign ((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝)) *
      ∏ y : o, ∏ x : n, blockDiagonal M (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha✝) (x, y)) (x, y)
simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,
  prodCongrLeft_apply]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq :
  (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha₁✝ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ' ha₂✝
⊢ σ = σ'
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (a₁ a₂ : (k : o) → k ∈ univ → Perm n) (ha₁ : a₁ ∈ univ) (ha₂ : a₂ ∈ univ),
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a₁ ha₁ =
        (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a₂ ha₂ →
      a₁ = a₂
intro σ σ' _ _ eq
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq :
  (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha₁✝ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ' ha₂✝
x : o
hx : x ∈ univ
k : n
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq :
  (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha₁✝ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ' ha₂✝
⊢ σ = σ'
ext (x hx k)
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq :
  (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ ha₁✝ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) σ' ha₂✝
x : o
hx : x ∈ univ
k : n
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
simp only at eq
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
this :
  ∀ (k : n) (x : o),
    ↑(prodCongrLeft fun k => σ k (_ : k ∈ univ)) (k, x) = ↑(prodCongrLeft fun k => σ' k (_ : k ∈ univ)) (k, x)
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
have :
  ∀ k x,
    prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =
      prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=
  fun k x => by rw [eq]
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
this : ∀ (k : n) (x : o), ↑(σ x (_ : x ∈ univ)) k = ↑(σ' x (_ : x ∈ univ)) k ∧ True
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
this :
  ∀ (k : n) (x : o),
    ↑(prodCongrLeft fun k => σ k (_ : k ∈ univ)) (k, x) = ↑(prodCongrLeft fun k => σ' k (_ : k ∈ univ)) (k, x)
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
simp only [prodCongrLeft_apply, Prod.mk.inj_iff] at this
no goals
case h.h.H
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x : o
hx : x ∈ univ
k : n
this : ∀ (k : n) (x : o), ↑(σ x (_ : x ∈ univ)) k = ↑(σ' x (_ : x ∈ univ)) k ∧ True
⊢ ↑(σ x hx) k = ↑(σ' x hx) k
exact (this k x).1
no goals
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ σ' : (k : o) → k ∈ univ → Perm n
ha₁✝ : σ ∈ univ
ha₂✝ : σ' ∈ univ
eq : (prodCongrLeft fun k => σ k (_ : k ∈ univ)) = prodCongrLeft fun k => σ' k (_ : k ∈ univ)
x✝ : o
hx : x✝ ∈ univ
k✝ k : n
x : o
⊢ ↑(prodCongrLeft fun k => σ k (_ : k ∈ univ)) (k, x) = ↑(prodCongrLeft fun k => σ' k (_ : k ∈ univ)) (k, x)
rw [eq]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : σ ∈ preserving_snd
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (b : n × o ≃ n × o), b ∈ preserving_snd → ∃ a ha, b = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
intro σ hσ
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : σ ∈ preserving_snd
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
rw [mem_preserving_snd] at hσ
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
have hσ' : ∀ x, (σ⁻¹ x).snd = x.snd := by
  intro x
  conv_rhs => rw [← Perm.apply_inv_self σ x, hσ]
case refine'_1
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ LeftInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst

case refine'_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ Function.RightInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst

case refine'_3
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
⊢ (fun k x =>
      { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
        left_inv := (_ : LeftInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst),
        right_inv := (_ : Function.RightInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst) }) ∈
    univ

case refine'_4
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
⊢ σ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
      (fun k x =>
        { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
          left_inv := (_ : LeftInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst),
          right_inv := (_ : Function.RightInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst) })
      ?refine'_3
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
⊢ ∃ a ha, σ = (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ)) a ha
refine' ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ⁻¹ (x, k)).fst, _, _⟩, _, _⟩
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
x : n × o
⊢ (↑σ⁻¹ x).snd = x.snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
intro x
no goals
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
x : n × o
⊢ (↑σ⁻¹ x).snd = x.snd
conv_rhs => rw [← Perm.apply_inv_self σ x, hσ]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k) = ↑σ (x, k)
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
⊢ ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
intro k x
case h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k).fst = (↑σ (x, k)).fst

case h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k).snd = (↑σ (x, k)).snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k) = ↑σ (x, k)
ext
no goals
case h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k).fst = (↑σ (x, k)).fst
simp only
no goals
case h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
k : o
x : n
⊢ ((↑σ (x, k)).fst, k).snd = (↑σ (x, k)).snd
simp only [hσ]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
⊢ ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
intro k x
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k) = ↑σ⁻¹ (x, k)
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
conv_lhs => rw [← Perm.apply_inv_self σ (x, k)]
case h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k).fst = (↑σ⁻¹ (x, k)).fst

case h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k).snd = (↑σ⁻¹ (x, k)).snd
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k) = ↑σ⁻¹ (x, k)
ext
no goals
case h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k).fst = (↑σ⁻¹ (x, k)).fst
simp only [apply_inv_self]
no goals
case h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
k : o
x : n
⊢ ((↑σ⁻¹ (↑σ (↑σ⁻¹ (x, k)))).fst, k).snd = (↑σ⁻¹ (x, k)).snd
simp only [hσ']
case refine'_1
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
x : n
⊢ (fun x => (↑σ⁻¹ (x, k)).fst) ((fun x => (↑σ (x, k)).fst) x) = x
case refine'_1
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ LeftInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst
intro x
no goals
case refine'_1
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
x : n
⊢ (fun x => (↑σ⁻¹ (x, k)).fst) ((fun x => (↑σ (x, k)).fst) x) = x
simp only [mk_apply_eq, inv_apply_self]
case refine'_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
x : n
⊢ (fun x => (↑σ (x, k)).fst) ((fun x => (↑σ⁻¹ (x, k)).fst) x) = x
case refine'_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
⊢ Function.RightInverse (fun x => (↑σ⁻¹ (x, k)).fst) fun x => (↑σ (x, k)).fst
intro x
no goals
case refine'_2
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : o
x✝ : k ∈ univ
x : n
⊢ (fun x => (↑σ (x, k)).fst) ((fun x => (↑σ⁻¹ (x, k)).fst) x) = x
simp only [mk_inv_apply_eq, apply_inv_self]
no goals
case refine'_3
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
⊢ (fun k x =>
      { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
        left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
        right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
    univ
apply Finset.mem_univ
case refine'_4.H.mk.h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : n
x : o
⊢ (↑σ (k, x)).fst =
    (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
            (fun k x =>
              { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) })
            (_ :
              (fun k x =>
                  { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                    left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                    right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
                univ))
        (k, x)).fst

case refine'_4.H.mk.h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : n
x : o
⊢ (↑σ (k, x)).snd =
    (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
            (fun k x =>
              { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) })
            (_ :
              (fun k x =>
                  { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                    left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                    right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
                univ))
        (k, x)).snd
case refine'_4
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
⊢ σ =
    (fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
      (fun k x =>
        { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
          left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
          right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) })
      (_ :
        (fun k x =>
            { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
              left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
              right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
          univ)
ext ⟨k, x⟩
no goals
case refine'_4.H.mk.h₁
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : n
x : o
⊢ (↑σ (k, x)).fst =
    (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
            (fun k x =>
              { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) })
            (_ :
              (fun k x =>
                  { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                    left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                    right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
                univ))
        (k, x)).fst
simp only [coe_fn_mk, prodCongrLeft_apply]
no goals
case refine'_4.H.mk.h₂
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (↑σ x).snd = x.snd
hσ' : ∀ (x : n × o), (↑σ⁻¹ x).snd = x.snd
mk_apply_eq : ∀ (k : o) (x : n), ((↑σ (x, k)).fst, k) = ↑σ (x, k)
mk_inv_apply_eq : ∀ (k : o) (x : n), ((↑σ⁻¹ (x, k)).fst, k) = ↑σ⁻¹ (x, k)
k : n
x : o
⊢ (↑σ (k, x)).snd =
    (↑((fun σ x => prodCongrLeft fun k => σ k (_ : k ∈ univ))
            (fun k x =>
              { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) })
            (_ :
              (fun k x =>
                  { toFun := fun x => (↑σ (x, k)).fst, invFun := fun x => (↑σ⁻¹ (x, k)).fst,
                    left_inv := (_ : ∀ (x : n), (↑σ⁻¹ ((↑σ (x, k)).fst, k)).fst = x),
                    right_inv := (_ : ∀ (x : n), (↑σ ((↑σ⁻¹ (x, k)).fst, k)).fst = x) }) ∈
                univ))
        (k, x)).snd
simp only [prodCongrLeft_apply, hσ]
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬σ ∈ preserving_snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ∀ (x : Perm (n × o)), x ∈ univ → ¬x ∈ preserving_snd → ↑↑(↑sign x) * ∏ x_1 : n × o, blockDiagonal M (↑x x_1) x_1 = 0
intro σ _ hσ
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬σ ∈ preserving_snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
rw [mem_preserving_snd] at hσ
case intro.mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ
case intro.mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ blockDiagonal M (↑σ (k, x)) (k, x) = 0
case intro.mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ ↑↑(↑sign σ) * ∏ x : n × o, blockDiagonal M (↑σ x) x = 0
rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), MulZeroClass.mul_zero]
case intro.mk.h
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ (↑σ (k, x)).snd ≠ x
case intro.mk
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ blockDiagonal M (↑σ (k, x)) (k, x) = 0
rw [← @Prod.mk.eta _ _ (σ (k, x)), blockDiagonal_apply_ne]
no goals
case intro.mk.h
m : Type ?u.1756003
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type v
inst✝² : CommRing R
o : Type u_1
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := filter (fun σ => ∀ (x : n × o), (↑σ x).snd = x.snd) univ
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (↑σ x).snd = x.snd
σ : Perm (n × o)
a✝ : σ ∈ univ
hσ : ¬∀ (x : n × o), (↑σ x).snd = x.snd
k : n
x : o
hkx : ¬(↑σ (k, x)).snd = (k, x).snd
⊢ (↑σ (k, x)).snd ≠ x
exact hkx