mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ Module.rank S N

Tactic:
;

Goal state after:
case a
R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
h✝ : Nontrivial R
inj : Function.Injective ⇑(algebraMap R S)
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ Module.rank S N
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
N : Type uN
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
hp : p ≤ R⁰
⊢ Module.rank S N = Module.rank R N

Tactic:
cases subsingleton_or_nontrivial R
  · have := (algebraMap R S).codomain_trivial; simp only [rank_subsingleton]
  have inj := IsLocalization.injective S hp
  apply le_antisymm <;> (rw [Module.rank]; apply ciSup_le'; intro ⟨s, hs⟩)
  · have := (faithfulSMul_iff_algebraMap_injective R S).mpr inj
    exact (hs.restrict_scalars' R).cardinal_le_rank
  · have := inj.nontrivial
    exact (hs.localization S p).cardinal_le_rank

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

Goal state before:
pp: case C_mul_T
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
s : R
⊢ r • C s * T n = C r * C s * T n

Tactic:
mul_left_inj_of_invertible,

Goal state after:
case C_mul_T
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
s : R
⊢ r • C s = C r * C s
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
⊢ (comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r) = toFinsupp 0

Tactic:
ext a
    have : a ≠ n := by lia
    simp [-single_eq_C_mul_T, single_eq_of_ne this]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∃ n f', toLaurent f' = f * T ↑n

Tactic:
by
  refine f.induction_on' ?_ fun n a => ?_ <;> clear f
  · rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
    refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
    simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
      mul_T_assoc, Int.natCast_add]
  · rcases n with n | n
    · exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
    · refine ⟨n + 1, Polynomial.C a, ?_⟩
      simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc,
        neg_add_cancel, T_zero, mul_one]

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

Goal state before:
pp: case mul_T.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)) * T 1)

Tactic:
;

Goal state after:
case mul_T.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (toLaurent f * T (-↑n))
⊢ Q (toLaurent f * T (-↑(n + 1)) * T 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : v i ∈ nonZeroDivisors α
⊢ M.det = 0

Tactic:
apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
M : Matrix n n α
v : n → α
h : M *ᵥ v = 0
i : n
hi : v i ∈ nonZeroDivisors α
⊢ M.det * v i = 0
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Subsingleton R
this : Subsingleton T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
;

Goal state after:
case inl
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
inj : Function.Injective ⇑(algebraMap R T)
this✝ : NoZeroDivisors R
h✝ : Subsingleton R
this : Subsingleton T
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝).coeff a✝ = (C x✝).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
x✝ : R
a✝ : ℤ
⊢ ((⇑invert ∘ ⇑C) x✝).coeff a✝ = (C x✝).coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)).coeff a✝ = (C t).coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
t : R
a✝ : ℤ
⊢ (invert (C t)).coeff a✝ = (C t).coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)).coeff a✝ = x✝.coeff a✝

Tactic:
;

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)).coeff a✝ = x✝.coeff a✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_1
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
w✝ : R
mem : w✝ ∈ ↑R⁰
⊢ (algebraMap R FT) w✝ ∈ IsUnit.submonoid FT

Tactic:
;

Goal state after:
case inr.refine_1
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
w✝ : R
mem : w✝ ∈ ↑R⁰
⊢ (algebraMap R FT) w✝ ∈ IsUnit.submonoid FT
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case pos.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg0 : g 0 = 0
hg : ∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * ↑s ^ (x_1 + (1 + x))) = 0
hin : 0 < n + 1
⊢ g 0 = 0

pp: case pos.succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg0 : g 0 = 0
hg : ∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * ↑s ^ (x_1 + (1 + x))) = 0
n✝ : ℕ
hin : n✝ + 1 < n + 1
⊢ g (n✝ + 1) = 0

Tactic:
;

Goal state after:
case pos.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg0 : g 0 = 0
hg : ∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * ↑s ^ (x_1 + (1 + x))) = 0
hin : 0 < n + 1
⊢ g 0 = 0

case pos.succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg0 : g 0 = 0
hg : ∑ x_1 ∈ Finset.range n, g (x_1 + 1) • (r * ↑s ^ (x_1 + (1 + x))) = 0
n✝ : ℕ
hin : n✝ + 1 < n + 1
⊢ g (n✝ + 1) = 0
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det =
    (blockDiagonal fun x ↦ A.map fun a ↦ (f a) 1).det * (blockDiagonal fun x ↦ B.map fun b ↦ (f 1) b).det

Tactic:
rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : β), (f 0) x = 0

R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : α), (f x) 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : β
⊢ (f 0) x✝ = 0

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : β
⊢ (f 0) x✝ = 0
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : α
⊢ (f x✝) 0 = 0

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
x✝ : α
⊢ (f x✝) 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
m : Type u_10
n : Type u_11
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn ↦ ↑(a * b)) = ↑(a * b)

Tactic:
;

Goal state after:
α : Type u_3
m : Type u_10
n : Type u_11
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn ↦ ↑(a * b)) = ↑(a * b)
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ i✝ j✝

Tactic:
;

Goal state after:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ =
    (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap i✝ j✝

Tactic:
;

Goal state after:
R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ i✝ j✝ =
    (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (tmul R) x y)ᴴ i✝ j✝ = kroneckerMap (tmul R) xᴴ yᴴ i✝ j✝

Tactic:
;

Goal state after:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
i✝ : m × p
j✝ : l × n
⊢ (kroneckerMap (tmul R) x y)ᴴ i✝ j✝ = kroneckerMap (tmul R) xᴴ yᴴ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹

Tactic:
by
  rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]

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

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'

Tactic:
apply is_reg.matrix

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := ⋯
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ (fun x ↦ A'.det • x) A'.adjugate.adjugate = (fun x ↦ A'.det • x) (A'.det ^ (Fintype.card n - 2) • A')
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (single i j c).BlockTriangular b

Tactic:
intro r

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r : m
⊢ ∀ ⦃j_1 : m⦄, b j_1 < b r → single i j c r j_1 = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ (fun σ ↦ ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i) = fun σ ↦
    ↑↑(Equiv.Perm.sign σ) *
      ∏ i,
        fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
          (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i

Tactic:
;

Goal state after:
case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ (fun σ ↦ ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i) = fun σ ↦
    ↑↑(Equiv.Perm.sign σ) *
      ∏ i,
        fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
          (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i =
    ↑↑(Equiv.Perm.sign σ) *
      ∏ i,
        fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
          (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i

Tactic:
;

Goal state after:
case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i =
    ↑↑(Equiv.Perm.sign σ) *
      ∏ i,
        fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
          (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ (fun i ↦ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i) = fun i ↦
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i

Tactic:
;

Goal state after:
case e_f.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ (fun i ↦ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i) = fun i ↦
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (v * (⅟(diagonal v)).diag) i = 1 i

Tactic:
let : Invertible (diagonal v).det := detInvertibleOfInvertible _
      rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
      dsimp
      rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
      exact mul_invOf_self _

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

Goal state before:
pp: case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

pp: case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : ¬M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
;

Goal state after:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : ¬M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal