mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝¹ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this✝ : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (⇑(Pi.algebraMap ι' R L) ∘ v)
⊢ ⇑(Pi.algebraMap ι' R L) ∘ v = ⇑(Pi.algebraMap ι' S L) ∘ ⇑(Pi.algebraMap ι' R S) ∘ v

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝¹ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this✝ : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (⇑(Pi.algebraMap ι' R L) ∘ v)
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' S L) ∘ ⇑(Pi.algebraMap ι' R S) ∘ v) x✝¹ x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ⇑(Pi.algebraMap ι' R L) ∘ v = ⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v) x✝¹ x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
aux : ⇑(Pi.algebraMap ι' R L) ∘ v = ⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v
⊢ LinearIndependent L (⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v)

Tactic:
replace h := h.linearIndependent_algebraMap_comp_aux L

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
aux : ⇑(Pi.algebraMap ι' R L) ∘ v = ⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v
h : LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ (⇑(Pi.algebraMap ι' R K) ∘ v) i
⊢ LinearIndependent L (⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v)
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
m : M
n : N
⊢ (m, n) ∈ L ↔
    (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range

Tactic:
constructor

Goal state after:
case h.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := ⋯
N' : Submodule R N := ⋯
P : ↥L →ₗ[R] ↥M' := ⋯
Q : ↥L →ₗ[R] ↥N' := ⋯
L' : Submodule R (↥M' × ↥N') := ⋯
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
m : M
n : N
⊢ (m, n) ∈ L →
    (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range

case h.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := ⋯
N' : Submodule R N := ⋯
P : ↥L →ₗ[R] ↥M' := ⋯
Q : ↥L →ₗ[R] ↥N' := ⋯
L' : Submodule R (↥M' × ↥N') := ⋯
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
m : M
n : N
⊢ (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range →
    (m, n) ∈ L
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ ((((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ).ker =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ ∀ (x : ↥(map (LinearMap.fst R M N) L) × ↥(map (LinearMap.snd R M N) L)),
    x ∈
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.prod
          (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd ↔
      x ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
⊢ (circulant v)ᵀ = circulant fun i ↦ v (-i)

Tactic:
ext

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᵀ i✝ j✝ = circulant (fun i ↦ v (-i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : SubtractionMonoid n
v : n → α
⊢ (circulant v)ᴴ = circulant (star fun i ↦ v (-i))

Tactic:
ext

Goal state after:
α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᴴ i✝ j✝ = circulant (star fun i ↦ v (-i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
constructor

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular → ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) → A.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
have hu : (Finset.univ : Finset { x // x ∈ Finset.filter (fun x ↦ ∃ j, f j = x) Finset.univ }) =
      Finset.univ.map f'' := by
      ext x
      simp only [Finset.univ_eq_attach, Finset.mem_attach, Finset.mem_map, Finset.mem_univ,
        true_and, true_iff]
      have hx := x.property
      simp only [Finset.univ_filter_exists, Finset.mem_image, Finset.mem_univ, true_and] at hx
      rcases hx with ⟨i, hi⟩
      refine ⟨i, ?_⟩
      rw [Subtype.ext_iff]
      exact hi

Goal state after:
case e_a
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
⊢ ∏ x, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
constructor

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast) →
    ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
constructor

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular → A.IsTotallyUnimodular

case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular → Aᵀ.IsTotallyUnimodular
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
⊢ ∀ ⦃a b : m⦄, a < b → l a ≤ l b

Tactic:
intro i₁

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ : m
⊢ ∀ ⦃b : m⦄, i₁ < b → l i₁ ≤ l b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∑ j, Mᵀ j = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin (n + 1)) R
hv : ∀ (i : Fin n), ∑ j, M i j = 0
j₁ j₂ : Fin (n + 1)
x✝ : Fin n
⊢ (∑ j, Mᵀ j) x✝ = 0 x✝
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos.refine_2
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det ∈ MonoidHom.mrange ↑SignType.castHom

Tactic:
· exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (↑A.den)⁻¹ • A.num.map Int.cast = A

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i✝ : m
j✝ : n
⊢ ((↑A.den)⁻¹ • A.num.map Int.cast) i✝ j✝ = A i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (-A).num = -A.num

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i✝ : m
j✝ : n
⊢ (-A).num i✝ j✝ = (-A.num) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ Aᵀ.num = A.numᵀ

Tactic:
ext

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i✝ : n
j✝ : m
⊢ Aᵀ.num i✝ j✝ = A.numᵀ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j ↔ Nonempty { p // p.length = m + 1 }

Tactic:
constructor

Goal state after:
case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j → Nonempty { p // p.length = m + 1 }

case succ.mpr
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
⊢ Nonempty { p // p.length = m + 1 } → 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
⊢ A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
constructor

Goal state after:
case mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
⊢ A.IsIrreducible → ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

case mpr
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
⊢ (∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j) → A.IsIrreducible
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case mpr
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ A.IsIrreducible

Tactic:
constructor

Goal state after:
case mpr.nonneg
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ ∀ (i j : n), 0 ≤ A i j

case mpr.connected
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := ⋯
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ IsSStronglyConnected n
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsDiag → A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

case mpr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag → (fromBlocks A B C D).IsDiag
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Matrix ι ι R
v : ι → M
⊢ N • v = ∑ j, fun i ↦ N i j • v j

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Matrix ι ι R
v : ι → M
x✝ : ι
⊢ (N • v) x✝ = (∑ j, fun i ↦ N i j • v j) x✝
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
S : Type u_6
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x✝² : R
x✝¹ : Matrix ι ι S
x✝ : ι → M
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
S : Type u_6
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x✝³ : R
x✝² : Matrix ι ι S
x✝¹ : ι → M
x✝ : ι
⊢ ((x✝³ • x✝²) • x✝¹) x✝ = (x✝³ • x✝² • x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
x✝¹ : Matrix ι ι R
x✝ : ι → M
⊢ (f.compLeft ι) (x✝¹ • x✝) = (RingHom.id (Matrix ι ι R)) x✝¹ • (f.compLeft ι) x✝

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
x✝² : Matrix ι ι R
x✝¹ : ι → M
x✝ : ι
⊢ (f.compLeft ι) (x✝² • x✝¹) x✝ = ((RingHom.id (Matrix ι ι R)) x✝² • (f.compLeft ι) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ mapMatrixModule ι id = id

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝¹ : ι → M
x✝ : ι
⊢ (mapMatrixModule ι id) x✝¹ x✝ = id x✝¹ x✝