mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range) σ₁ σ₂
⊢ Perm.sign σ₁ • MultilinearMap.domDomCongr σ₁ ((↑a).domCoprod ↑b) =
    Perm.sign σ₂ • MultilinearMap.domDomCongr σ₂ ((↑a).domCoprod ↑b)

Tactic:
rw [QuotientGroup.leftRel_apply] at H
    obtain ⟨⟨sl, sr⟩, h⟩ := H
    ext v
    simp only [MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply,
      coe_multilinearMap, _root_.smul_apply]
    replace h := inv_mul_eq_iff_eq_mul.mp h.symm
    have : Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr))
      = Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) := by simp
    rw [h, this, mul_smul, mul_smul, smul_left_cancel_iff, ← TensorProduct.tmul_smul,
      TensorProduct.smul_tmul', a.map_congr_perm _ sl, b.map_congr_perm _ sr]
    simp only [Sum.map_inr, Perm.sumCongrHom_apply, Perm.sumCongr_apply, Sum.map_inl,
      Function.comp_def, Perm.coe_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
w : Fin (n + 1) → k
hw : ∀ i_1 ∈ univ.erase i, w i_1 = 0
x✝ :
  (affineCombination k univ s.points) w ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hshift : w i = 1
j : Fin (n + 1)
hj : ¬j = i
⊢ j ∈ univ.erase i

Tactic:
by simpa using hj

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

Goal state before:
pp: case pos
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Module.rank K ↥u.range = 0
⊢ ∃ f v, ↑e = LinearMap.transvection f v

pp: case neg
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : ¬Module.rank K ↥u.range = 0
⊢ ∃ f v, ↑e = LinearMap.transvection f v

Tactic:
· use 0, 0
      ext x
      suffices u x = 0 by simp [← hu, this]
      rw [rank_zero_iff] at hr
      simpa [← Subtype.coe_inj] using Subsingleton.allEq (⟨u x , mem_range_self u x⟩ : range u) 0

Goal state after:
case neg
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : ¬Module.rank K ↥u.range = 0
⊢ ∃ f v, ↑e = LinearMap.transvection f v
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case refine_1.right
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = refl K (V ⧸ (↑e).fixedSubmodule)

Tactic:
fixedReduce_eq_one,

Goal state after:
case refine_1.right
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule
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
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
⊢ ∀ (v w : V),
    (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
      ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1

Tactic:
intro v w

Goal state after:
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
this✝ : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
this : Invertible 2 := (Invertible.map (algebraMap R (A ⊗[R] CliffordAlgebra Q)) 2).copy 2 ⋯
v w : V
⊢ (1 * 1) ⊗ₜ[R] ((ι Q) v * (ι Q) w) + (1 * 1) ⊗ₜ[R] ((ι Q) w * (ι Q) v) =
    ((QuadraticMap.polarBilin (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

Tactic:
induction hx using Subgroup.closure_induction'' generalizing m with

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
⊢ ((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra =
    (LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra

Tactic:
ext (a b)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ ((((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b =
    (((((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x ↦ a.elim0)) (List.finRange 0)).prod =
    GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

Tactic:
rw [List.finRange_zero, List.map_nil, List.prod_nil]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ 1 = GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
i j : Fin n
hij : f' i = f' j
⊢ i = j

Tactic:
rw [Subtype.ext_iff] at hij

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN'✝ : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
i j : Fin n
hij : ↑(f' i) = ↑(f' j)
⊢ i = j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
⊢ Aᵀ.IsTotallyUnimodular

Tactic:
simp only [isTotallyUnimodular_iff, ← transpose_submatrix, det_transpose] at hA ⊢

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

Tactic:
apply IsTotallyUnimodular.transpose

Goal state after:
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
⊢ A.IsTotallyUnimodular → Aᵀ.IsTotallyUnimodular

Tactic:
apply IsTotallyUnimodular.transpose

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

Goal state before:
pp: case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-↑A 0 1 + -(↑A 1 1 * (-↑A 0 1 / ↑A 1 1))| < |↑A 1 1|

Tactic:
← Int.sub_eq_add_neg,

Goal state after:
case neg.refine_2
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ |-↑A 0 1 - ↑A 1 1 * (-↑A 0 1 / ↑A 1 1)| < |↑A 1 1|
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ (if i = j then ∑ x, Bᴴ i' x * (Fintype.card m • B) x j' else 0) = (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')

Tactic:
by
        simp only [← mul_apply, mul_smul_comm, hB.conjTranspose_mul]
        simp [one_apply, ← Nat.cast_mul, ← ite_and]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
⊢ ∃ p, 0 < p.length

Tactic:
let qT := transposePath (A := A) (q.cons e)

Goal state after:
case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
⊢ ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

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

Tactic:
| h0 A a1 a4 _ a6 =>

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Semigroup α
x✝² x✝¹ x✝ : WithConv (Matrix m n α)
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
simp [convMul_def, hadamard_assoc]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = (mul (r • 1)) x

Tactic:
rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply]

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • (mul 1) x
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
b : { v // v ≠ 0 }
⊢ MulAction.stabilizer kˣ ↑b = ⊥

Tactic:
Module.stabilizer_units_eq_bot_of_ne_zero k b.property

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
b : { v // v ≠ 0 }
⊢ ⊥ = ⊥
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : ℙ K V
v : V
hv : v ≠ 0
h : ¬mk K v hv = b
⊢ IsCollinear {mk K v hv, b}

Tactic:
induction b using Projectivization.ind with

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i j : ι
hij : i ≠ j
b : F
w : ι → F
⊢ (b * w j) • Pi.single i 1 = SpecialLinearGroup.transvection hij b • w - w

Tactic:
simp [mul_smul,
    Matrix.SpecialLinearGroup.smul_def, transvection_coe, add_smul, Matrix.single_mulVec_eq]

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

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ ∃ h, LinearEquiv.det h = a ∧ h • mk K D.rep ⋯ = mk K D.rep ⋯ ∧ h • mk K D'.rep ⋯ = mk K D'.rep ⋯

Tactic:
refine ⟨dilatransvection (f := b.coord ⟨D.rep, hD_mem⟩)
      (v := (a.val - 1) • b ⟨D.rep, hD_mem⟩) (by simp), ?_, ?_, ?_⟩

Goal state after:
case pos.refine_1
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ LinearEquiv.det (dilatransvection ⋯) = a

case pos.refine_2
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ dilatransvection ⋯ • mk K D.rep ⋯ = mk K D.rep ⋯

case pos.refine_3
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ dilatransvection ⋯ • mk K D'.rep ⋯ = mk K D'.rep ⋯
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
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
rcases max_cases (Module.finrank R V) 1 with ⟨h, h'⟩ |  ⟨h, h'⟩

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1

case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ((Q.toBilin bm) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)) (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

Tactic:
simp_rw [LinearMap.map_sum₂, map_sum, LinearMap.map_smul₂, map_smul, toBilin_apply,
    smul_ite, smul_zero, ← Finset.sum_product', ← Finset.diag_union_offDiag,
    Finset.sum_union (Finset.disjoint_diag_offDiag _), Finset.sum_diag, if_true]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 = x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • Q (bm x_1.1)
        else if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Free R M
⊢ Function.Surjective BilinMap.toQuadraticMap

Tactic:
intro Q

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Free R M
Q : QuadraticMap R M N
⊢ ∃ a, a.toQuadraticMap = Q
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
⊢ (∃ Q', Q'.comp N.mkQ = Q) → N ≤ Q.radical

Tactic:
· rintro ⟨Q', rfl⟩ m hm
    simp [radical, (Submodule.Quotient.mk_eq_zero _).mpr hm, LinearMap.ext_iff, polar]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
⊢ (Q m = 0 ∧ ∀ (n : M), Q (m + n) = Q n) ↔ ∀ (x : M), Q (m + x) - Q m - Q x = 0

Tactic:
refine ⟨by simp +contextual, fun h ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : ∀ (x : M), Q (m + x) - Q m - Q x = 0
⊢ Q m = 0 ∧ ∀ (n : M), Q (m + n) = Q n
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | 0 < w i}.ncard + ({i | w i < 0}.ncard + {i | w i = 0}.ncard) = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard

Tactic:
add_left_cancel_iff,

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | w i < 0}.ncard + {i | w i = 0}.ncard = {i | w i ≤ 0}.ncard
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
⊢ P.root k - P.root j ∈ range ⇑P.root

Tactic:
suffices 0 < P.pairingIn ℤ l i by
    convert! P.root_sub_root_mem_of_pairingIn_pos this hli using 1
    rw [hl]
    module

Goal state after:
case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
⊢ 0 < P.pairingIn ℤ l i