mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ZPow

Goal state before:
pp: case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A ^ ((m + 1) * (n + 1))).det

Tactic:
rw [det_pow]

Goal state after:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (n + 1)))
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝³ : P.IsCrystallographic
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : Finite ι
i j : ↥b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : Module.IsReflexive R N
h₁ :
  (P.pairingIn ℤ ↑i ↑j, P.pairingIn ℤ ↑j ↑i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
h₂ : P.pairingIn ℤ ↑i ↑j ≤ 0
contra : P.root ↑i = -2 • P.root ↑j
⊢ ∑ i_1 ∈ { val := {i, j}, nodup := ⋯ }, (⇑(Finsupp.single i 1) + ⇑(Finsupp.single j 2)) i_1 • P.root ↑i_1 = 0 ∧
    ∃ i_1 ∈ { val := {i, j}, nodup := ⋯ }, (⇑(Finsupp.single i 1) + ⇑(Finsupp.single j 2)) i_1 ≠ 0

Tactic:
simp [contra, hij, hij.symm]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
⊢ ∃ d, (∀ (i : ↥b.support), 0 < d i) ∧ (b.cartanMatrix * Matrix.diagonal d).PosDef

Tactic:
have _i : Fintype ι := Fintype.ofFinite ι
  set d : b.support → ℤ := fun i ↦ P.RootFormIn ℤ (P.rootSpanMem ℤ i) (P.rootSpanMem ℤ i) with hd
  refine ⟨d, fun i ↦ ?_, ?_⟩
  · rw [hd, ← posRootForm_eq]
    exact RootPositiveForm.zero_lt_posForm_apply_root _ _
  · rw [cartanMatrix_mul_diagonal_eq]
    refine Matrix.PosDef.smul ?_ two_pos
    have aux : (P.posRootForm ℤ).posForm.IsSymm := by
      simpa only [posRootForm_eq, LinearMap.BilinForm.isSymm_iff] using P.rootFormIn_isSymm ℤ
    rw [← LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix _ _ aux]
    simpa using P.posRootForm_rootFormIn_posDef ℤ

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
⊢ ∃ d, (∀ (i : ↥b.support), 0 < d i) ∧ (b.cartanMatrix * Matrix.diagonal d).PosDef

Tactic:
by
  have _i : Fintype ι := Fintype.ofFinite ι
  set d : b.support → ℤ := fun i ↦ P.RootFormIn ℤ (P.rootSpanMem ℤ i) (P.rootSpanMem ℤ i) with hd
  refine ⟨d, fun i ↦ ?_, ?_⟩
  · rw [hd, ← posRootForm_eq]
    exact RootPositiveForm.zero_lt_posForm_apply_root _ _
  · rw [cartanMatrix_mul_diagonal_eq]
    refine Matrix.PosDef.smul ?_ two_pos
    have aux : (P.posRootForm ℤ).posForm.IsSymm := by
      simpa only [posRootForm_eq, LinearMap.BilinForm.isSymm_iff] using P.rootFormIn_isSymm ℤ
    rw [← LinearMap.BilinForm.posDef_toQuadraticMap_iff_matrix _ _ aux]
    simpa using P.posRootForm_rootFormIn_posDef ℤ

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : P.IsRootSystem
this : ¬HasEigenvalue (toLin' b.cartanMatrix) 4
aux : toLin' (4 - b.cartanMatrix) = -(toLin' b.cartanMatrix - 4 • 1)
⊢ (4 - b.cartanMatrix).det ≠ 0

Tactic:
rwa [ne_eq, ← det_toLin', det_eq_zero_iff_ker_ne_bot, aux, ker_neg, ← eigenspace_def,
      ← hasEigenvalue_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker ((aeval f) (q.leadingCoeff • X + C (q.coeff 0)))

Tactic:
aeval_def

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : q.degree = 1
⊢ LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
rcases lt_trichotomy k n with hkn | rfl | hkn

Goal state after:
case succ.inl
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

case succ.inr.inl
R : Type u
inst✝ : Ring R
k : ℕ
ih : k < k → eval (-↑k) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-↑k) (ascPochhammer R k) * (-↑k + ↑k) = 0

case succ.inr.inr
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ vandermonde v = of Fin.cons (fun j ↦ v 0 ^ ↑j) fun i ↦ Fin.cons 1 fun j ↦ v i.succ * vandermonde (tail v) i j

Tactic:
conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.inr.inl.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.inr.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
← mul_right_inj' (a := ((Equiv.swap 0 i₀).sign : K))
      (by simp [show 0 ≠ i₀ by rintro rfl; contradiction]),

Goal state after:
case succ.inr.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
i₀ : Fin (n + 1)
hi₀ : w i₀ ≠ 0
⊢ ↑↑(Perm.sign (swap 0 i₀)) * (projVandermonde v w).det =
    ↑↑(Perm.sign (swap 0 i₀)) * ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ (f - g).degree < ↑(#s)

Tactic:
rw [← mem_degreeLT]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g ∈ degreeLT R #s
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor x (id y) + basisDivisor (id y) x

Tactic:
id

Goal state after:
F : Type u_1
inst✝ : Field F
x y : F
hxy : x ≠ y
⊢ basisDivisor x y + basisDivisor y x = basisDivisor x y + basisDivisor y x
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ f ((aeval g) φ) = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ

Tactic:
map_aeval,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial τ R →+* S
g : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom (f.comp (algebraMap R (MvPolynomial τ R))) fun i ↦ f (g i)) φ = (eval₂Hom (f.comp C) fun i ↦ f (g i)) φ
Module: Mathlib.Algebra.MvPolynomial.Monad

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ (bind₂ f) ((monomial d) 1) = (monomial d) 1

Tactic:
bind₂_monomial,

Goal state after:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* MvPolynomial σ S
d : σ →₀ ℕ
⊢ f 1 * (monomial d) 1 = (monomial d) 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
⊢ eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v)

Tactic:
by
  rw [derivative_nodal, eval_finsetSum, ← add_sum_erase _ _ hi, add_eq_left]
  exact sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
r : R
a : MvPolynomial σ R
ha : a ∈ {x | IsWeightedHomogeneous w x m}
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
⊢ (weight w) c = m

Tactic:
exact ha (right_ne_zero_of_mul hc)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun i ↦ {i}) p = p.degrees

Tactic:
degrees_def

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun i ↦ {i}) p = p.support.sup fun s ↦ toMultiset s
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
n : ℕ
⊢ (X i ^ n).IsHomogeneous n

Tactic:
by
  simpa only [one_mul] using (isHomogeneous_X _ _).pow n

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : j = 0
⊢ ((decompose 𝒜) x) 0 = 0

Tactic:
by simpa using hx

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∑ j, (monomial (Finsupp.single j 1)) (1 i j) = X i

Tactic:
Finset.sum_eq_single i

Goal state after:
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ (monomial (Finsupp.single i 1)) (1 i i) = X i

case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

case h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case succ.inl
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
exact hF.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux hFn

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
⊢ F = G

Tactic:
apply funext_of_le_card hF hG h
  exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R ∈ symplecticGroup l R

Tactic:
mem_iff,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R * J l R * (J l R)ᵀ = J l R
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : (J l R).det * (A.det * A.det) = (J l R).det
⊢ (J l R).det * (A.det * A.det) = (J l R).det

Tactic:
exact hA

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f ∈ symplecticGroup l S

Tactic:
mem_iff,

Goal state after:
l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f * J l S * (A.map ⇑f)ᵀ = J l S
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ Aᵀ ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R

Tactic:
mem_iff,

Goal state after:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R ↔ Aᵀ * J l R * A = J l R
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ Module.rank R ↥(span R (range (of.symm 0ᵀ))) = 0

Tactic:
transpose_zero,

Goal state after:
case inr
R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hn : Nonempty n
⊢ Module.rank R ↥(span R (range (of.symm 0))) = 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : f Q • x = 0
heq2 : f P • x = 0
⊢ f U • x = f U • 0

Tactic:
f_mul,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : (f (Vᵀ⁻¹ * A) * f U) • x = 0
heq2 : (f (V * C) * f U) • x = 0
⊢ f U • x = f U • 0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : (f (Vᵀ⁻¹ * A) * f U) • x = 0
heq2 : (f (V * C) * f U) • x = 0
⊢ f U • x = f U • 0

Tactic:
f_mul,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R
heq1 : (f Vᵀ⁻¹ * f A * f U) • x = 0
heq2 : (f V * f C * f U) • x = 0
⊢ f U • x = f U • 0
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix n n R
h : IsUnit A
⊢ A.rank = Fintype.card n

Tactic:
obtain ⟨A, rfl⟩ := h

Goal state after:
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : (Matrix n n R)ˣ
⊢ (↑A).rank = Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).rank = A.rank

Tactic:
simpa only [reindex_apply] using! rank_reindex em.symm en.symm A

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : f (Qᵀ * P) = f (Pᵀ * Q)
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
f_mul,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : f Qᵀ * f P = f (Pᵀ * Q)
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0