mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := ⋯
b : Basis (Fin n) R V
S : Type := ⋯
γ : S →+* R := ⋯
this : IsDomain S
x✝² : Algebra S R := ⋯
x✝¹ : Module S V := ⋯
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := ⋯
ibc : IsBaseChange R ε
M : Type := ⋯
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := ⋯
vM : M := ⋯
⊢ ∀ (i : Fin n), (ibc.toDual fM) (b i) = f (b i)

Tactic:
intro i

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ (ibc.toDual fM) (b i) = f (b i)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) (a₁ ᵍ⊗ₜ[R] ↑b₁)))
        ((auxEquiv R 𝒜 ℬ) (↑a₂ ᵍ⊗ₜ[R] b₂))) =
    (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
dsimp [auxEquiv, tmul]

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (decompose ℬ) ↑b₁))
          ((decompose 𝒜) ↑a₂ ⊗ₜ[R] (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
inst✝ : Invertible 2
m : M
⊢ ↑x * (ι Q) m * ↑x⁻¹ ∈ (ι Q).range

Tactic:
induction hx using Subgroup.closure_induction'' generalizing m with
  | mem x hx =>
    obtain ⟨a, ha⟩ := hx
    let := x.invertible
    let : Invertible (ι Q a) := by rwa [ha]
    let : Invertible (Q a) := invertibleOfInvertibleι Q a
    simp_rw [← invOf_units x, ← ha, ι_mul_ι_mul_invOf_ι, LinearMap.mem_range_self]
  | inv_mem x hx =>
    obtain ⟨a, ha⟩ := hx
    let := x.invertible
    let : Invertible (ι Q a) := by rwa [ha]
    let : Invertible (Q a) := invertibleOfInvertibleι Q a
    simp_rw [← invOf_units x, inv_inv, ← ha, invOf_ι_mul_ι_mul_ι, LinearMap.mem_range_self]
  | one => simp_rw [inv_one, Units.val_one, one_mul, mul_one, LinearMap.mem_range_self]
  | mul y z _ _ hy hz =>
    simp_rw [mul_inv_rev, Units.val_mul]
    suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using this
    obtain ⟨z', hz'⟩ := hz m
    obtain ⟨y', hy'⟩ := hy z'
    simp_rw [← hz', ← hy', LinearMap.mem_range_self]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, ↑x_1 = ↑x) ↔ x ∈ lipschitzGroup Q

Tactic:
norm_cast

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ (∃ x_1 ∈ lipschitzGroup Q, x_1 = x) ↔ x ∈ lipschitzGroup Q
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : 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)
⊢ ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)

Tactic:
intro i

Goal state after:
ι : 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)
i : Fin n
⊢ ↑(bN' i) = Pi.single (f i) (a i)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_1
ι : 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
c : Fin n → R
⊢ ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ (∑ x, c x • Pi.single (f x) (a x)) i

Tactic:
intro i

Goal state after:
case refine_1
ι : 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
c : Fin n → R
i : ι
⊢ (if h : ∃ j, f j = i then a h.choose else 0) ∣ (∑ x, c x • Pi.single (f x) (a x)) i
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ maps : {i : I} → A i →ₐ[R] B
x y : FreeTensorAlgebra R A
r : rel R A x y
⊢ (RingCon.ker ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)).toRingHom) x y

Tactic:
cases r with
          | id => simp
          | prod => simp

Goal state after:
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' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Tactic:
let M' := L.map (LinearMap.fst ..)
  let N' := L.map (LinearMap.snd ..)
  let P : L →ₗ[R] M' := (LinearMap.fst ..).submoduleMap L
  let Q : L →ₗ[R] N' := (LinearMap.snd ..).submoduleMap L
  let L' : Submodule R (M' × N') := LinearMap.range (P.prod Q)
  have hL₁' : Surjective (Prod.fst ∘ L'.subtype) := by
    simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
    simpa only [L', ← LinearMap.range_comp, fst_prod, range_eq_top] using
      (LinearMap.fst ..).submoduleMap_surjective L
  have hL₂' : Surjective (Prod.snd ∘ L'.subtype) := by
    simp only [← coe_snd (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
    simpa only [L', ← LinearMap.range_comp, snd_prod, range_eq_top] using
      (LinearMap.snd ..).submoduleMap_surjective L
  obtain ⟨e, he⟩ := goursat_surjective hL₁' hL₂'
  use M', N', L'.goursatFst, L'.goursatSnd, e
  rw [← he]
  simp only [LinearMap.range_comp, Submodule.range_subtype, L', M', N', P, Q]
  rw [comap_map_eq_self]
  · ext ⟨m, n⟩
    constructor
    · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply,
      Subtype.exists, Prod.exists, LinearMap.prodMap_apply, subtype_apply, Prod.mk.injEq,
      Subtype.ext_iff, submoduleMap_coe_apply, fst_apply, snd_apply]
      grind
    · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply,
      Subtype.exists, Prod.exists, LinearMap.prodMap_apply, subtype_apply, Prod.mk.injEq,
      snd_apply, fst_apply, Subtype.ext_iff, submoduleMap_coe_apply]
      grind
  · convert! goursatFst_prod_goursatSnd_le (range <| P.prod Q)
    simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff]
    grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C M ^ p ^ k

pp: case inl.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)

Tactic:
← C_pow

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ matPolyEquiv ((expand K (p ^ k)).mapMatrix (M ^ p ^ k).charmatrix) = X ^ p ^ k - C (M ^ p ^ k)

case inl.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (C M)
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
⊢ ∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun i ↦ v (-i)

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : Star α
⊢ ∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun i ↦ v (-i))

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
⊢ (circulant fun i ↦ if ↑i = 0 then 1 else 0) = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case succ.inl
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
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
have hAB := det_succ_row ((fromRows A B).submatrix f g) i

Goal state after:
case succ.inl
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
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ j,
      (-1) ^ (↑i + ↑j) * (A.fromRows B).submatrix f g i j *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove j.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ ∑ j,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k, 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k, 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ ∀ (i : Fin n), a i ≠ 0

Tactic:
intro i

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
⊢ a i ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
⊢ (A.submatrix Subtype.val g).IsUpperTriangular

Tactic:
intro i

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
i : { i // l i ≠ ⊤ }
⊢ ∀ ⦃j : { i // l i ≠ ⊤ }⦄, id j < id i → A.submatrix Subtype.val g i j = 0
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
rw [this, abs_eq_self.mpr (Int.emod_nonneg (A.1 0 0) h)]

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ ↑A 0 0 % ↑A 1 0 < |↑A 1 0|
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: 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

Tactic:
intro i

Goal state after:
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 := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i : n
⊢ ∀ (j : n), ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
⊢ (A.map f).IsDiag

Tactic:
intro i

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ A.map f i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
⊢ (-A).IsDiag

Tactic:
intro i

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (-A) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
⊢ (A + B).IsDiag

Tactic:
intro i

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (A + B) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
⊢ (A - B).IsDiag

Tactic:
intro i

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (A - B) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
R : Type u_3
n : Type u_4
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
⊢ (k • A).IsDiag

Tactic:
intro i

Goal state after:
α : Type u_1
R : Type u_3
n : Type u_4
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (k • A) i j = 0) i 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
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
⊢ IsSStronglyConnected n

Tactic:
intro i

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i : n
⊢ ∀ (j : n), ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ A ∈ closure {S, T}

Tactic:
rw [reps_one_id A a1 a4 a6]

Goal state after:
case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ 1 ∈ closure {S, T}
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
B : Matrix n n R
hA : IsLeftRegular A
hB : IsLeftRegular B
⊢ IsLeftRegular (A * B)

Tactic:
exact hA.mul hB

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
x y : Fin m → R
eq : g x = g y
i : Fin m
⊢ x i = y i

Tactic:
by
      simpa [g] using congr($eq ⟨i, i.prop.trans hnm⟩)

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r s : R'
⊢ 1 = 1 * 1

Tactic:
rw [mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ ↑E

Tactic:
exact ha hE hx

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
intro i

Goal state after:
case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬Dependent f

Tactic:
dependent_iff_not_independent,

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬¬Independent f
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ Dependent ![u, v] ↔ u = v

Tactic:
dependent_iff_not_independent,

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬Independent ![u, v] ↔ u = v
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬LinearIndependent K (Projectivization.rep ∘ ![u, v]) ↔ u = v

Tactic:
linearIndependent_fin2

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ a, a • v = u) ↔ LinearIndependent K ![u, v]

Tactic:
linearIndependent_fin2

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ a, a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
⊢ ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → (↑a ∈ s) = (↑b ∈ s)

Tactic:
by
      rintro ⟨-, h⟩ ⟨y, -⟩ c rfl
      exact Iff.eq <| s.smul_mem_iff <| left_ne_zero_of_smul h

Goal state after: