mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3.e'_16
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 ℤˣ)
a₁ : A
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
SetLike.coe_gOne,

Goal state after:
case e'_3.e'_16
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 ℤˣ)
a₁ : A
b₂ : B
⊢ a₁ = a₁ * 1
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3.e'_17
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 ℤˣ)
a₁ : A
b₂ : B
⊢ b₂ = ↑GradedMonoid.GOne.one * b₂

Tactic:
SetLike.coe_gOne,

Goal state after:
case e'_3.e'_17
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 ℤˣ)
a₁ : A
b₂ : B
⊢ b₂ = 1 * b₂
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e_f
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 ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] ↑GradedMonoid.GOne.one) =
    (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] (↑GradedMonoid.GOne.one * ↑GradedMonoid.GOne.one)

Tactic:
SetLike.coe_gOne,

Goal state after:
case e_f
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 ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] 1) = (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] (1 * 1)
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
r : R
⊢ ((lift R A) fun {i} ↦ maps) ((algebraMap R (FreeProduct R A)) r) = (algebraMap R B) r

Tactic:
lift_apply,

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
r : R
⊢ ((ringCon R A).liftₐ ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)) ⋯)
      ((algebraMap R (FreeProduct R A)) r) =
    (algebraMap R B) r
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:
rw [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:
rw [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.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:
rw [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.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖

Tactic:
by congr; field

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
⊢ (f fun i ↦ x i) = g fun i ↦ x i

Tactic:
have (i : _) := (nonempty_fintype (κ i)).some

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this : (i : ι) → Fintype (κ i)
⊢ (f fun i ↦ x i) = g fun i ↦ x i
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'
i : ι
inst✝ : DecidableEq ι
this : Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i ↦ 1) i (r • 1)
⊢ r • (tprod R) 1 = (r • 1) • ⨂ₜ[R] (i : ι), 1

Tactic:
smul_one_smul,

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'
i : ι
inst✝ : DecidableEq ι
this : Pi.mulSingle i ((algebraMap R' (A i)) r) = update (fun i ↦ 1) i (r • 1)
⊢ r • (tprod R) 1 = r • ⨂ₜ[R] (i : ι), 1
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

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

Tactic:
rw [← ne_eq, ← independent_pair_iff_ne, independent_mk_iff_LinearIndependent] at h

Goal state after:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
w : V
hw : w ≠ 0
h : LinearIndependent K ![v, w]
⊢ IsCollinear {mk K v hv, mk K w hw}
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = ↑(center_equiv_rootsOfUnity g)

Tactic:
have hι : ¬ IsEmpty ι := fun hι ↦ hV (by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty])
    rw [not_subsingleton_iff_nontrivial] at hV
    have := Module.Free.instFaithfulSMulOfNontrivial R V
    suffices (((((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)).trans
      centerEquivRootsOfUnity g).val : R) • LinearMap.id) : V →ₗ[R] V) =
        ((Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity g).val : R) • LinearMap.id by
      rw [← Units.val_inj]
      apply FaithfulSMul.eq_of_smul_eq_smul (α := V)
      intro x
      simp only [MulEquiv.trans_apply, LinearMap.ext_iff, LinearMap.smul_apply, LinearMap.id_coe,
        id_eq] at this
      rw [MulEquiv.trans_apply, this]
    simp only [MulEquiv.trans_apply]
    have hgg' := Subgroup.centerCongr_apply_coe (Matrix.SpecialLinearGroup.toLin_equiv b) g
    rw [← Subtype.coe_inj, ← LinearEquiv.toLinearMap_inj, LinearMap.ext_iff] at hgg'
    set g' := ((Subgroup.centerCongr (Matrix.SpecialLinearGroup.toLin_equiv b)) g)
    ext x
    have := centerEquivRootsOfUnity_apply_apply g' x
    simp only [Subgroup.smul_def, Units.smul_def] at this
    simp only [LinearMap.smul_apply, LinearMap.id_coe, id_eq]
    rw [this, ← LinearEquiv.coe_toLinearMap, hgg',
      Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq,
      Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity g,
      Matrix.toLin_scalar]
    simp

Goal state after:
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 Q + sigNeg Q + Module.finrank 𝕜 ↥(radical Q) = Module.finrank 𝕜 M

Tactic:
e.sigPos_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 Q + Module.finrank 𝕜 ↥(radical Q) = Module.finrank 𝕜 M
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: 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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (∑ a₁,
        0 k a₁ *
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
            (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
            (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
            (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂,
        if P.root a₂ = P.root ↑i + P.root l then (if -k = a₂ then 1 else 0) * (↑(chainBotCoeff (↑i) l) + 1)
        else (if -k = a₂ then 1 else 0) * 0) =
    ∑ x,
        (if -k = ↑i then ↑|b.cartanMatrix i x| else 0) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl x) (Sum.inr l) +
      ∑ a₂,
        if a₂ = -l then (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 1
        else (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 0

Tactic:
rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]

Goal state after:
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✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (∑ a₁,
        0 k a₁ *
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
            (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
            (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
            (Sum.inl a₁) (Sum.inr l) +
      if P.root (-k) = P.root ↑i + P.root l then (if -k = -k then 1 else 0) * (↑(chainBotCoeff (↑i) l) + 1)
      else (if -k = -k then 1 else 0) * 0) =
    ∑ x,
        (if -k = ↑i then ↑|b.cartanMatrix i x| else 0) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl x) (Sum.inr l) +
      ∑ a₂,
        if a₂ = -l then (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 1
        else (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 0
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 j : ↥b.support
⊢ ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b

Tactic:
rw [Ring.lie_def, sub_mul]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
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
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
x : ι
contra : P.root (-↑i) = P.root ↑i + P.root x
⊢ P.root x = -(P.root ↑i + P.root ↑i)

Tactic:
simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra

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

Goal state before:
pp: ι : 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ∀ (j : ι), v b j ∈ U
⊢ range ⇑(Pi.basisFun K (↥b.support ⊕ ι)) ⊆ ↑↑U

Tactic:
range_subset_iff,

Goal state after:
ι : 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ∀ (j : ι), v b j ∈ U
⊢ ∀ (y : ↥b.support ⊕ ι), (Pi.basisFun K (↥b.support ⊕ ι)) y ∈ ↑↑U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
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
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∉ range ⇑P.root
aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
aux₄ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
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
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
h₇ : P.root l - P.root ↑j ∉ range ⇑P.root
aux₃ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
aux₄ : ∀ x ∈ Finset.univ, ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
simp [Finset.sum_ite_of_false aux₃, Finset.sum_ite_of_false aux₄]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a

Tactic:
· rintro ⟨ht, h, rfl⟩
    exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).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
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
⊢ (↑e).fixedSubmodule ≤ (↑(transvection hfv * e)).fixedSubmodule ∧ v ∈ (↑(transvection hfv * e)).fixedSubmodule

Tactic:
have ht : e.fixedSubmodule ≤ (transvection hfv).fixedSubmodule := fun x hx ↦ by
    rw [mem_fixedSubmodule_transvection_iff, smul_eq_zero]
    left
    rw [← Submodule.mem_bot K, ← hf]
    exact mem_map_of_mem hx

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
e : V ≃ₗ[K] V
f : Dual K V
v : V
hv : v ∉ (↑e).fixedSubmodule
hf : map f (↑e).fixedSubmodule = ⊥
hfv : f (v - e v) = 0
hfv' : f (e v) = 1
ht : (↑e).fixedSubmodule ≤ (↑(transvection hfv)).fixedSubmodule
⊢ (↑e).fixedSubmodule ≤ (↑(transvection hfv * e)).fixedSubmodule ∧ v ∈ (↑(transvection hfv * e)).fixedSubmodule
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
hacc : Acc r a
⊢ Acc (CutExpand r) {a}

Tactic:
induction hacc with

Goal state after:
case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) {a}
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case hf
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f : Dual K V
u : V
hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ ker f
hfu : f u = 1
⊢ (↑e).fixedSubmodule ≤ ker f

Tactic:
exact le_trans le_sup_left hf

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)
hμ : IsProjectiveLimit μ P
⊢ IsFiniteMeasure μ

Tactic:
constructor
  rw [hμ.measure_univ_eq (∅ : Finset ι)]
  exact measure_lt_top _ _

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet ((fun j ↦ if hji : j = i then ⋯.mpr t else univ) j)

Tactic:
simp only [hji, eq_mpr_eq_cast, dif_pos]

Goal state after:
case pos
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet (cast ⋯ t)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: α : Type u_1
ι : Type u_2
X : ι → Type u_3
mα : MeasurableSpace α
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
g : α → (i : ι) → X i
⊢ Measurable g ↔ ∀ ⦃i : ι⦄, i ∈ Δ → Measurable fun a ↦ g a i

Tactic:
by
  simp_rw [measurable_iff_comap_le, cylinderEvents, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

Goal state after: