-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ

Proof state:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by
  apply prod_eq_zero (mem_univ j)
  rw [updateCol_self, Pi.single_eq_of_ne' h]

Result:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ A.updateCol j (Pi.single i 1) (σ j) j = 0

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne' h]

Result:
no goals

Proof state:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if σ j' = σ j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Tactic:
simp_rw [this]

Result:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if j' = j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0

Tactic:
apply prod_eq_zero (mem_univ j)

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ A.updateCol j (Pi.single i 1) (σ j) j = 0

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ↑↑(sign σ) * ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ↑↑(sign σ) * ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
congr 1

Result:
case a.e_a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Proof state:
case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
congr

Result:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
⊢ (fun i_1 => A.updateRow i (Pi.single j 1) (σ i_1) i_1) = fun i_1 => A.updateCol j (Pi.single i 1) (σ i_1) i_1

Proof state:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'

Tactic:
have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff

Result:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'

Proof state:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
⊢ (fun i_1 => A.updateRow i (Pi.single j 1) (σ i_1) i_1) = fun i_1 => A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
ext j'

Result:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
j' : n
⊢ A.updateRow i (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single i 1) (σ j') j'

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ∑ σ : Perm n, ↑↑(sign σ) * ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
apply Finset.sum_congr rfl

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∀ x ∈ univ,
    ↑↑(sign x) * ∏ i_1 : n, A.updateRow i (Pi.single j 1) (x i_1) i_1 =
      ↑↑(sign x) * ∏ i_1 : n, A.updateCol j (Pi.single i 1) (x i_1) i_1

Proof state:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1 : n, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
rw [this]

Result:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = 0

Proof state:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if j' = j then Pi.single j 1 j' else A (σ j') j') = if j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'

Tactic:
rw [← dite_eq_ite, ← dite_eq_ite]

Result:
case pos.e_f.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ (if x : j' = j then Pi.single j 1 j' else A (σ j') j') = if x : j' = j then Pi.single (σ j) 1 (σ j') else A (σ j') j'