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

Proof state:
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

Tactic:
intro σ _

Result:
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

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.adjugateᵀ = Aᵀ.adjugate

Tactic:
ext i j

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ A.adjugateᵀ i j = Aᵀ.adjugate i j

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
⊢ Pi.single j 1 (σ⁻¹ i) = 0

Tactic:
apply Pi.single_eq_of_ne

Result:
case neg.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
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ σ⁻¹ i ≠ j

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 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'

Tactic:
congr 1 with rfl

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

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

Tactic:
rw [Pi.single_eq_same, Pi.single_eq_same]

Result:
no goals

Proof state:
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

Tactic:
by_cases h : i = σ j

Result:
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

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

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1)).det

Tactic:
rw [det_apply', det_apply']

Result:
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

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ A.adjugateᵀ i j = Aᵀ.adjugate i j

Tactic:
rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1)).det

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
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'

Tactic:
rw [updateRow_apply, updateCol_apply]

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:
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
⊢ A.updateRow i (Pi.single j 1) (σ (σ⁻¹ i)) (σ⁻¹ i) = 0

Tactic:
erw [apply_symm_apply σ i, updateRow_self]

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
⊢ Pi.single j 1 (σ⁻¹ i) = 0

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 = 0

Tactic:
apply prod_eq_zero (mem_univ (σ⁻¹ i))

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
⊢ A.updateRow i (Pi.single j 1) (σ (σ⁻¹ i)) (σ⁻¹ i) = 0

Proof state:
case neg.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
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
h' : σ⁻¹ i = j
⊢ False

Tactic:
exact h ((symm_apply_eq σ).mp 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 α
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'

Tactic:
subst h

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
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'

Proof state:
case neg.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
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ σ⁻¹ i ≠ j

Tactic:
intro h'

Result:
case neg.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
this : ∏ j' : n, A.updateCol j (Pi.single i 1) (σ j') j' = 0
h' : σ⁻¹ i = j
⊢ False