mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
h : LinearMap.det (transvection f v) ≠ 1
this✝ : Free R V
this : Module.Finite R V
⊢ 1 + f v = 1

Tactic:
hfv,

Goal state after:
R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
h : LinearMap.det (transvection f v) ≠ 1
this✝ : Free R V
this : Module.Finite R V
⊢ 1 + 0 = 1
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
⊢ Module.rank R M ≤ Module.rank R (M ⧸ M')

Tactic:
by
    nontriviality R
    rw [Module.rank]
    refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_
    rw [LinearIndepOn, linearIndependent_iff'] at hs
    simp_rw [linearIndependent_iff', ← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]
    intro t g hg i hi
    obtain ⟨r, hg⟩ := hN hg
    simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg
    exact r.prop.2 _ (mul_comm (g i) r ▸ hs t _ hg i hi)

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
n : ℕ
x : Fin n → M
⊢ (List.ofFn fun x_1 ↦ toDirectSum ((ι R) (x x_1))).prod =
    (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)

Tactic:
toDirectSum_ι

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (List.ofFn fun x_1 ↦ (DirectSum.of (fun n ↦ ⨂[R]^n M) 1) ((PiTensorProduct.tprod R) fun x_2 ↦ x x_1)).prod =
    (DirectSum.of (fun i ↦ ⨂[R]^i M) n) ((PiTensorProduct.tprod R) x)
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_2
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
⊢ Surjective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
suffices mod ∘ b.repr = g ∘ nG.mkQ by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp
    ext x b
    simp [mod, g, f, H]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case convert_3
ι : 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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ ∀ b ∈ Finset.univ, b ≠ hj.choose → (if i = f b then ⋯.choose • a b else 0) = 0

pp: case convert_4
ι : 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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ hj.choose ∉ Finset.univ → (if i = f hj.choose then ⋯.choose • a hj.choose else 0) = 0

Tactic:
· rintro j - h
                have hinj := f.injective.ne h
                rw [hj.choose_spec] at hinj
                simp [hinj.symm]

Goal state after:
case convert_4
ι : 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
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ hj.choose ∉ Finset.univ → (if i = f hj.choose then ⋯.choose • a hj.choose else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
⊢ p₁.length ≠ 0

Tactic:
simp [hp₁_len]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
hdet : IsRegular (A.det * star A.det)
⊢ Aᴴ * A = ↑(Fintype.card n) • 1

Tactic:
have hreg : IsLeftRegular A :=
    (isRegular_of_isLeftRegular_det hdet.of_mul_left.left).left

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
hdet : IsRegular (A.det * star A.det)
hreg : IsLeftRegular A
⊢ Aᴴ * A = ↑(Fintype.card n) • 1
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 • (1 * x) = r • (x * 1)

Tactic:
rw [mul_one, one_mul]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ span Set.univ = ⊤

Tactic:
rw [eq_top_iff, SetLike.le_def]

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
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
⊢ Nondegenerate ↔ Q.radical = ⊥

Tactic:
by
  refine ⟨Nondegenerate.radical_eq_bot, fun h ↦ ⟨h, ?_⟩⟩
  rw [← QuadraticMap.radical_eq_ker_polarBilin, h]
  nontriviality R
  simp only [rank_subsingleton', zero_le]

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : NeZero 2
inst✝² : Fintype ι
w : ι → 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i | w i = 0}) = {i | w i = 0}.ncard

Tactic:
Pi.dim_spanSubset

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : NeZero 2
inst✝² : Fintype ι
w : ι → 𝕜
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ {i | w i = 0}.ncard = {i | w i = 0}.ncard
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 + Module.finrank 𝕜 ↥(Pi.spanSubset 𝕜 {i | w i = 0}) = Nat.card ι

Tactic:
Pi.dim_spanSubset

Goal state after:
𝕜 : 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 = Nat.card ι
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: M : Type u_2
inst✝⁵ : AddCommGroup M
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : FiniteDimensional 𝕜 M
this : Invertible 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos (weightedSumSquares 𝕜 w) + sigNeg Q + Module.finrank 𝕜 ↥(radical Q) = Module.finrank 𝕜 M

Tactic:
e.sigNeg_eq,

Goal state after:
M : Type u_2
inst✝⁵ : AddCommGroup M
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : FiniteDimensional 𝕜 M
this : Invertible 2
w : Fin (Module.finrank 𝕜 M) → 𝕜
e : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos (weightedSumSquares 𝕜 w) + sigNeg (weightedSumSquares 𝕜 w) + Module.finrank 𝕜 ↥(radical Q) = Module.finrank 𝕜 M
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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
⊢ ω b * f i = e i * ω b

Tactic:
by
  classical
  have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
  simp only [← mul_assoc, ω_mul_ω] at this
  simpa [mul_assoc, ω_mul_ω] using this.symm

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

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
⊢ (e i ^ 0).col (Sum.inr j) = 0 ∨
    ∃ k x, P.root k = P.root j + 0 • P.root ↑i ∧ (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1

Tactic:
exact Or.inr ⟨j, 1, by simp, by ext; simp [Pi.single_apply]⟩

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

Goal state before:
pp: ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : P.root l = (x + 1) • P.root i + y • P.root j
⊢ 2 * (x + 1) + A * y = (x + 1) • 2 + y • P.pairingIn ℤ j i

Tactic:
Int.zsmul_eq_mul,

Goal state after:
ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : P.root l = (x + 1) • P.root i + y • P.root j
⊢ 2 * (x + 1) + A * y = (x + 1) * 2 + y • P.pairingIn ℤ j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : P.root m = x • P.root i + (y - 1) • P.root j
⊢ 2 * x + A * (y - 1) = x • 2 + (y - 1) • P.pairingIn ℤ j i

Tactic:
Int.zsmul_eq_mul,

Goal state after:
ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : P.root m = x • P.root i + (y - 1) • P.root j
⊢ 2 * x + A * (y - 1) = x * 2 + (y - 1) • P.pairingIn ℤ j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j
⊢ 2 * (x + 1) + A * (y - 1) = (x + 1) • 2 + (y - 1) • P.pairingIn ℤ j i

Tactic:
Int.zsmul_eq_mul,

Goal state after:
ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j
⊢ 2 * (x + 1) + A * (y - 1) = (x + 1) * 2 + (y - 1) • P.pairingIn ℤ j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ 2 * x + A * y = x • 2 + y • P.pairingIn ℤ j i

Tactic:
Int.zsmul_eq_mul,

Goal state after:
ι : 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 l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ 2 * x + A * y = x * 2 + y • P.pairingIn ℤ j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CharZero 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✝ : Fintype ι
i : ↥b.support
⊢ (h i).trace = 0

Tactic:
by
  classical
  let _i := P.indexNeg
  suffices ∑ j, P.pairingIn ℤ j i = 0 by
    simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach,
      Sum.elim_inl, Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add]
    norm_cast
  suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from
    eq_zero_of_neg_eq <| by simpa using this
  let σ : ι ≃ ι := Function.Involutive.toPerm _ neg_involutive
  exact σ.sum_comp (P.pairingIn ℤ · i)

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

Goal state before:
pp: case h
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : genWeightSpace (↥U) χ ≠ ⊥
this : ∀ {w : ↥b.support ⊕ ι → K}, w ≠ 0 → w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ → ∃ i t, t • w = v b i
w : ↥U
hw₀ : w ≠ 0
hw : U.incl w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
i : ι
t : K
hi : t • ↑w = v b i
⊢ t • ↑w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ ∧ t • ↑w ∈ U

Tactic:
exact ⟨SMulMemClass.smul_mem _ hw, SMulMemClass.smul_mem _ w.property⟩

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

Goal state before:
pp: case inr.inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ι
hij : i ≠ j
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)

Tactic:
· suffices d j ≠ χ x by
          simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero, this, hij, hi] using!
            congr_fun hk (Sum.inr j)
        rw [← hχx]
        exact hd₁ <| by simp [hij.symm]

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j

Tactic:
exact (this a hij.symm (lt_of_le_of_ne ltij hij.symm)).symm

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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
⊢ v - e v ∈ (↑e).fixedSubmodule

Tactic:
rw [← e.fixedSubmodule.ker_mkQ, LinearMap.mem_ker,
          map_sub, sub_eq_zero]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n✝ : ℕ
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
n : ℕ
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 → finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
f : Dual K V
v : V
hf : (↑e).fixedSubmodule ≤ ker f
hv : f v = 1
hv_notMem : v ∉ (↑e).fixedSubmodule
⊢ (↑e).fixedSubmodule.mkQ v = (↑e).fixedSubmodule.mkQ (e v)