mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.algebraMap
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) ((algebraMap R (CliffordAlgebra Q₂)) r✝) =
    (-1) ^ ↑0 • ((map f₂) ((algebraMap R (CliffordAlgebra Q₂)) r✝) * (ι Qₙ) (f₁ v₁))

Tactic:
AlgHom.commutes,

Goal state after:
case mem.mem_mul.e_a.e_a.mem.algebraMap
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝ =
    (-1) ^ ↑0 • ((algebraMap R (CliffordAlgebra Qₙ)) r✝ * (ι Qₙ) (f₁ v₁))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.algebraMap
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝ =
    (-1) ^ ↑0 • ((algebraMap R (CliffordAlgebra Qₙ)) r✝ * (ι Qₙ) (f₁ v₁))

Tactic:
Nat.cast_zero,

Goal state after:
case mem.mem_mul.e_a.e_a.mem.algebraMap
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝ =
    (-1) ^ 0 • ((algebraMap R (CliffordAlgebra Qₙ)) r✝ * (ι Qₙ) (f₁ v₁))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ involute ↑x⁻¹ * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
simp_rw [← invOf_units x, inv_inv, ← ha, map_invOf, involute_ι, invOf_neg, neg_mul,
      invOf_ι_mul_ι_mul_ι, ← map_neg, 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
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
hx : x ∈ lipschitzGroup Q
b : M
⊢ involute ↑x * (ι Q) b * ↑x⁻¹ ∈ (ι Q).range

Tactic:
by
  unfold lipschitzGroup at hx
  induction hx using Subgroup.closure_induction'' generalizing b 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, involute_ι, neg_mul, ι_mul_ι_mul_invOf_ι Q a b, ← map_neg,
      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
    let := invertibleNeg (ι Q a)
    let := Invertible.map involute (ι Q a)
    simp_rw [← invOf_units x, inv_inv, ← ha, map_invOf, involute_ι, invOf_neg, neg_mul,
      invOf_ι_mul_ι_mul_ι, ← map_neg, LinearMap.mem_range_self]
  | one => simp_rw [inv_one, Units.val_one, map_one, one_mul, mul_one, LinearMap.mem_range_self]
  | mul y z _ _ hy hz =>
    simp_rw [mul_inv_rev, Units.val_mul, map_mul]
    suffices involute (Q := Q) ↑y * (involute (Q := Q) ↑z * ι Q b * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using this
    obtain ⟨z', hz'⟩ := hz b
    obtain ⟨y', hy'⟩ := hy z'
    simp_rw [← hz', ← hy', LinearMap.mem_range_self]

Goal state after:
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 ℤˣ)
⊢ ∀ (x y : B), 1 ᵍ⊗ₜ[R] (x + y) = 1 ᵍ⊗ₜ[R] x + 1 ᵍ⊗ₜ[R] y

Tactic:
simp [tmul, TensorProduct.tmul_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
⊢ Module.rank R M = 0

Tactic:
by_contra! h'

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : IsTorsion R M
h' : Module.rank R M ≠ 0
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ (liftι R M) ((algebraMap R (ExteriorAlgebra R M)) r✝) =
    (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) 0) ⟨(algebraMap R (ExteriorAlgebra R M)) r✝, ⋯⟩

Tactic:
AlgHom.commutes,

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ (algebraMap R (⨁ (i : ℕ), ↥(⋀[R]^i M))) r✝ =
    (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) 0) ⟨(algebraMap R (ExteriorAlgebra R M)) r✝, ⋯⟩
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
motive : (⨁ (i : ι), M i) → Prop
x : ⨁ (i : ι), M i
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
induction x using DirectSum.induction_on with

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)
⊢ (⇑(frobenius K[X] p))^[k] (M ^ p ^ k).charpoly = (⇑(frobenius K[X] p))^[k] M.charpoly

Tactic:
iterate_frobenius (R := K[X])

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)
⊢ (M ^ p ^ k).charpoly ^ p ^ k = (⇑(frobenius K[X] p))^[k] M.charpoly
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)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = (⇑(frobenius K[X] p))^[k] M.charpoly

Tactic:
iterate_frobenius (R := K[X])

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)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ p ^ k
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:
by
  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)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ Fintype.card K

Tactic:
iterate_frobenius (R := K[X])

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)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ Fintype.card K
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix (Fin.succAbove 0) id).det = (↑0).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
Nat.cast_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow 0 • (M.submatrix (Fin.succAbove 0) id).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

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

Tactic:
· intro _ _ _ _ _
    apply hA

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

Goal state before:
pp: case mp
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✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : ((A.submatrix f g).submatrix ⇑(Fintype.equivFin ι).symm ⇑(Fintype.equivFin ι).symm).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
det_submatrix_equiv_self

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
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: 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
hA : ((A.submatrix f g).submatrix ⇑Equiv.ulift ⇑Equiv.ulift).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
det_submatrix_equiv_self

Goal state after:
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
hA : (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ (A.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
⊢ ∑ x, ((-1) ^ (↑i₀ + ↑x) * ∑ c, M c x) * (M.submatrix i₀.succAbove x.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
Fintype.sum_eq_add_sum_subtype_ne _ j₀

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
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c, M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i, ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case mp.refine_3
α : 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 α
h : (fromBlocks A B C D).IsDiag
i : n
j : m
⊢ C i j = 0 i j

pp: case mp.refine_4
α : 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 α
h : (fromBlocks A B C D).IsDiag
i j : n
hij : i ≠ j
⊢ (fun i j ↦ D i j = 0) i j

Tactic:
· exact h Sum.inr_ne_inl

Goal state after:
case mp.refine_4
α : 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 α
h : (fromBlocks A B C D).IsDiag
i j : n
hij : i ≠ j
⊢ (fun i j ↦ D i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ permanent 1 = 1

Tactic:
by
  rw [← diagonal_one]; simp [-diagonal_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.FiniteDimensional

Goal state before:
pp: case succ
R : Type u_2
M₂ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [∀ (i : Fin n), Module.Finite R (N i)] [∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst✝³ : (i : Fin (n + 1)) → AddCommGroup (N i)
inst✝² : (i : Fin (n + 1)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (n + 1)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (n + 1)), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
suffices
      Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) ∧
        Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) by
      cases this
      exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩
    cases ih fun i => N i.succ
    exact ⟨Module.Free.linearMap _ _ _ _, Module.Finite.linearMap _ _ _ _⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (x + y) i_1 (p i_1)) =
    ((f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)) + (f p) fun i_1 ↦ Function.update m i y i_1 (p i_1)

Tactic:
simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]

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

Goal state before:
pp: G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = LinearMap.GeneralLinearGroup.ofLinearEquiv e • mk K D.rep ⋯

Tactic:
smul_mk

Goal state after:
G : Type u_1
K : Type u_2
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : DivisionRing K
inst✝³ : Module K V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G K V
e : V ≃ₗ[K] V
D : ℙ K V
⊢ mk K (e • D.rep) ⋯ = mk K (LinearMap.GeneralLinearGroup.ofLinearEquiv e • D.rep) ⋯
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
exact Subgroup.mem_sup_right <| transvection_mem_lineStab one_ne_zero c

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : SpecialLinearGroup R V
⊢ LinearMap.det ↑↑u = 1

Tactic:
simp [← LinearEquiv.coe_det, u.prop]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : SpecialLinearGroup R V
n : ℕ
⊢ LinearEquiv.det (↑x ^ n) = 1

Tactic:
by simp [x.prop]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x : SpecialLinearGroup R V
n : ℤ
⊢ LinearEquiv.det (↑x ^ n) = 1

Tactic:
by simp [x.prop]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
b : Module.Basis n R V
u : _root_.SpecialLinearGroup R (n → R)
⊢ (LinearMap.toMatrix' ↑↑u).det = 1

Tactic:
simp [← LinearEquiv.coe_det, u.prop]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
⊢ fromBlocks 0 0 0 (x + y) = fromBlocks 0 0 0 x + fromBlocks 0 0 0 y

Tactic:
ext (i | i) (j | j)

Goal state after:
case inl.inl
ι : 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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i j : ↥b.support
⊢ fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inl j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inl i) (Sum.inl j)

case inl.inr
ι : 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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i : ↥b.support
j : ι
⊢ fromBlocks 0 0 0 (x + y) (Sum.inl i) (Sum.inr j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inl i) (Sum.inr j)

case inr.inl
ι : 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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i : ι
j : ↥b.support
⊢ fromBlocks 0 0 0 (x + y) (Sum.inr i) (Sum.inl j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inr i) (Sum.inl j)

case inr.inr
ι : 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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
x y : Matrix ι ι R
i j : ι
⊢ fromBlocks 0 0 0 (x + y) (Sum.inr i) (Sum.inr j) = (fromBlocks 0 0 0 x + fromBlocks 0 0 0 y) (Sum.inr i) (Sum.inr j)