mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
⊢ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
    ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
by
  rcases hx.1.eq_or_lt with hx0 | hxpos
  · simpa [hx0.symm, nonempty_closedInterior] using s.closedInterior_inter_shift_zero i
  ext p
  by_cases hp : p ∈ affineSpan k (.range s.points)
  · obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
    rw [Set.mem_inter_iff, SetLike.mem_coe, s.independent.affineCombination_mem_shift_iff i hw,
      affineCombination_mem_closedInterior_iff hw, Set.mem_image]
    simp_rw [AffineMap.homothety_eq_iff_of_mul_eq_one (mul_inv_cancel₀ hxpos.ne.symm),
      univ.homothety_affineCombination _ _ (mem_univ i)]
    simp only [↓existsAndEq, and_true]
    rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc,
      closedInterior_inter_shift_aux i hxpos hx.2 hw]
    · simp only [mem_compl, mem_singleton, not_not, forall_eq]
      congrm (∀ j, (hj : _) → $(by simp [lineMap_apply, hj])) ∧ $(by simp [lineMap_apply])
    · simp [AffineMap.lineMap_apply, Finset.sum_add_distrib, ← Finset.mul_sum,
        Finset.sum_sub_distrib, hw]
  · apply iff_of_false (hp <| s.closedInterior_subset_affineSpan ·.1)
    rintro ⟨q, hq, rfl⟩
    exact hp <| homothety_mem (mem_affineSpan _ (by simp)) _ <|
      affineSpan_mono _ (by simp) ((s.faceOpposite i).closedInterior_subset_affineSpan hq)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (AlgHom.op (toBaseChange A Q)).comp reverseOp =
    (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
      ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))

Tactic:
by
  ext v
  change op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
    Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
      (Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
        (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))
  rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul,
    Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι]
  rfl

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

Goal state before:
pp: case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
r✝ : R
⊢ r✝ • 0 = c • r✝ • 0

Tactic:
smul_zero

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

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
y : CliffordAlgebra 0
x : Unit
⊢ (ι 0) x * y = y * (ι 0) x

Tactic:
| ι x =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * y + x₂ * y = y * x₁ + y * x₂

Tactic:
hx₁,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ + x₂ * y = y * x₁ + y * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ x₁ * y * x₂ = y * (x₁ * x₂)

Tactic:
hx₁,

Goal state after:
case mul
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ * x₂ = y * (x₁ * x₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ reverse ((ι 0) x) = (ι 0) x

Tactic:
| ι x =>

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

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ * reverse x₂ = x₁ * x₂

Tactic:
hx₁,

Goal state after:
case mul
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * reverse x₂ = x₁ * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ + reverse x₂ = x₁ + x₂

Tactic:
hx₁,

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + reverse x₂ = x₁ + x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case ι
x : ℝ
⊢ reverse ((ι Q) x) = (ι Q) x

Tactic:
| ι x =>

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

Goal state before:
pp: case mul
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ * reverse x₂ = x₁ * x₂

Tactic:
hx₁,

Goal state after:
case mul
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * reverse x₂ = x₁ * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse x₁ + reverse x₂ = x₁ + x₂

Tactic:
hx₁,

Goal state after:
case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + reverse x₂ = x₁ + x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0 = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2)

Tactic:
ring

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

Goal state before:
pp: case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2 = 0

Tactic:
ring

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

Goal state before:
pp: case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1 = 0

Tactic:
ring

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

Goal state before:
pp: case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 = 0

Tactic:
ring

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

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x : R × R
⊢ toQuaternion (involute (reverse ((ι (Q c₁ c₂)) x))) = star (toQuaternion ((ι (Q c₁ c₂)) x))

Tactic:
| ι x =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (r₁ * r₂) • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
obtain ⟨ι, b, i, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    suffices toMatrix b b (transvection f v) =
      Matrix.diagonal (Function.update 1 i (1 + f v)) by
      rw [this]
      simp only [Matrix.det_diagonal]
      rw [Finset.prod_eq_single i]
      · simp
      · intro j _ hj
        simp [Function.update_of_ne hj]
      · simp
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.diagonal]
    simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
    rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
    simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]
    split_ifs with hxy hxi
    · simp [← hxy, hxi]
    · rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]
    · rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
      convert! mul_zero _
      by_cases hxi : x = i
      · simp [← hxi, Finsupp.single_eq_of_ne hxy]
      · simp [Finsupp.single_eq_of_ne hxi]

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

Goal state before:
pp: case zero
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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ 0 = (-1) ^ (i₂ * i₁) • 0

Tactic:
smul_zero

Goal state after:
case zero
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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ 0 = 0
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 z : 𝒜 ᵍ⊗[R] ℬ
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x))
          (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x)) ((auxEquiv R 𝒜 ℬ) y)))
        ((auxEquiv R 𝒜 ℬ) z)) =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x))
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) y)) ((auxEquiv R 𝒜 ℬ) z)))

Tactic:
rw [gradedMul_assoc]

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

Goal state before:
pp: case mem.mem_mul.e_a.e_a.zero
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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
⊢ 0 = (-1) ^ i₂ • 0

Tactic:
smul_zero

Goal state after:
case mem.mem_mul.e_a.e_a.zero
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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem
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₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n : ℕ
hm₁ : m₁' ∈ (ι Q₁).range ^ i₁n
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * ↑i₁n) • ((map f₂) m₂ * (map f₁) m₁')

Tactic:
induction hm₁ using Submodule.pow_induction_on_left' with

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
hA : A.IsTotallyUnimodular
⊢ ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
intro k f g
    by_cases hfg : f.Injective ∧ g.Injective
    · exact hA k f g hfg.1 hfg.2
    · use 0
      rw [SignType.coe_zero, eq_comm]
      simp_rw [not_and_or, Function.not_injective_iff] at hfg
      obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := hfg
      · rw [← det_transpose, transpose_submatrix]
        apply det_zero_of_column_eq hij.symm
        simp [hfij]
      · apply det_zero_of_column_eq hij
        simp [hgij]

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

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

Tactic:
simp_rw [Finset.sum_apply, transpose_apply, hv, Pi.zero_apply]

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

Goal state before:
pp: 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 : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
f : Fin k → m ⊕ m'
g : Fin k → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
induction k with
  | zero => use 1; simp
  | succ k ih =>
    specialize hB ⟨g 0⟩
    -- Either `f` is `inr` somewhere or `inl` everywhere
    obtain ⟨i, j, hfi⟩ | ⟨f', rfl⟩ : (∃ i j, f i = .inr j) ∨ (∃ f', f = .inl ∘ f') := by
      simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
      intro hfr
      choose f' hf' using hfr
      exact ⟨f', funext hf'⟩
    · have hAB := det_succ_row ((fromRows A B).submatrix f g) i
      simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
      obtain ⟨j', s, hj'⟩ := hB j
      · simp only [hj'] at hAB
        by_cases hj'' : ∃ x, g x = j'
        · obtain ⟨x, rfl⟩ := hj''
          rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
          · rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)
          · simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]
        · rw [not_exists] at hj''
          use 0
          simpa [hj''] using hAB.symm
    · rw [isTotallyUnimodular_iff] at hA
      apply hA

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) ↔ C B

Tactic:
refine ⟨?_, hS _⟩

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) → C B
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ diagonal A.diag i j = A i j

Tactic:
by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [diagonal_apply_eq, diag]
    · rw [diagonal_apply_ne _ hij, h hij]

Goal state after:
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 j h

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 j : n
h : i ≠ j
⊢ A.map f i j = 0
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 j h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (-A) i j = 0
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 j h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A + B) i j = 0
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 j h

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A - B) i j = 0
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 j h

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 j : n
h : i ≠ j
⊢ (k • A) i j = 0
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case inl
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = 1
⊢ (1 + A s j) * (1 + A t j) = 1 + A s j + A t j + A s j * A t j

Tactic:
ring

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

Goal state before:
pp: case inr
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
j : n
hr : A r j = -1
⊢ (1 + -A s j) * (1 + -A t j) = 1 + -A s j + -A t j + A s j * A t j

Tactic:
ring

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

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
j : n
⊢ 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)

Tactic:
by
    obtain hs | hs := hpm s j <;> obtain hr | hr := hpm r j <;>
      obtain ht | ht := hpm t j <;> simp [hs, hr, ht]

Goal state after:
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
ind : LinearIndependent R A.col
a✝ b✝ : R
bal : A.IsDetpBalanced a✝ b✝
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a✝ b✝
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
this : ∀ (s : ℤˣ), detp s Ai = ∑ j, detp (-s) (Aj j) * A.col (g j) i + detp s D * A.col j₀ i
a b : R
⊢ (Finsupp.linearCombination R A.col) (v a b) i = a * detp 1 Ai + b * detp (-1) Ai

Tactic:
simp [v, Finset.sum_add_distrib, mul_assoc, ← Finset.mul_sum, add_add_add_comm, mul_add, this]

Goal state after:
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
ind : LinearIndependent R A.row
⊢ A.Nonsingular

Tactic:
by
  simpa using Nonsingular.of_linearIndependent_col (A := Aᵀ) ind

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

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)

Tactic:
have hc : Nat.card V = Nat.card k ^ n := by simp [Nat.card_congr e.toEquiv, Nat.card_fun]

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
hc : Nat.card V = Nat.card k ^ n
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
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_pair_iff_eq u v

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
⊢ ¬u = v ↔ u ≠ v
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
hS : S.ncard = 2
⊢ IsCollinear S

Tactic:
by
  obtain ⟨x, y, _, rfl⟩ := Set.ncard_eq_two.1 hS
  exact isCollinear_pair x y

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ Module.finrank K ↥(Submodule.span K {u, v}) = Module.finrank K ↥p

Tactic:
rw [hp1, ← Matrix.range_cons_cons_empty _ _ ![]]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
hp2 : mk K u hu ∈ Submodule.projectivization p
hp3 : mk K v hv ∈ Submodule.projectivization p
h1 : Submodule.span K {u, v} ≤ p
this : Module.Finite K ↥p
⊢ Module.finrank K ↥(Submodule.span K (Set.range ![u, v])) = 2