mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
i j : ι
hij : v' i = v' j
⊢ i = j

Tactic:
have : Injective v := hv.injective

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this✝ : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
i j : ι
hij : v' i = v' j
this : Injective v
⊢ i = j
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e'_2.a
ι : 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 : Fin n), f j ≠ i
x : Fin n
a✝ : x ∈ Finset.univ
⊢ (if i = f x then ⋯.choose • a x else 0) = 0

Tactic:
specialize hj x

Goal state after:
case e'_2.a
ι : 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 : ι
x : Fin n
hj : f x ≠ i
a✝ : x ∈ Finset.univ
⊢ (if i = f x then ⋯.choose • a x else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : (A.submatrix (f ∘ ⇑(Fintype.equivFin ι).symm) (g ∘ ⇑(Fintype.equivFin ι).symm)).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
← submatrix_submatrix,

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ι → m
g : ι → n
hA : ((A.submatrix f g).submatrix ⇑(Fintype.equivFin ι).symm ⇑(Fintype.equivFin ι).symm).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

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

Tactic:
← submatrix_submatrix,

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
k : ℕ
f : Fin k → m
g : Fin k → n
hA : ((A.submatrix f g).submatrix ⇑Equiv.ulift ⇑Equiv.ulift).det ∈ Set.range SignType.cast
⊢ (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ (!![0, -1; 1, 0] * (!![1, -(↑A 0 0 / ↑A 1 0); 0, 1] * ↑A)) 1 0 = ↑A 0 0 + -(↑A 1 0 * (↑A 0 0 / ↑A 1 0))

Tactic:
norm_num [vecMul, vecHead, vecTail, mul_comm]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(A i j * ↑((A i j).den * k)).num = A i j * ↑((A i j).den * k)

Tactic:
Nat.cast_mul,

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ ↑(A i j * (↑(A i j).den * ↑k)).num = A i j * (↑(A i j).den * ↑k)
Module: Mathlib.LinearAlgebra.Matrix.Unique

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst✝¹ : Unique m
inst✝ : Unique n
M : Matrix m n A
i : m
j : n
⊢ (fun a ↦ of fun x x_1 ↦ a) ((fun M ↦ M default default) M) i j = M i j

Tactic:
simp [Subsingleton.elim i default, Subsingleton.elim j default]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ IsSelfAdjoint f

Tactic:
simp_rw [IsIdempotentElem, WithConv.ext_iff, ← Matrix.ext_iff, convMul_def, hadamard_apply,
    ← isIdempotentElem_iff, IsIdempotentElem.iff_eq_zero_or_one] at hf
  rw [IsSelfAdjoint, WithConv.ext_iff]
  ext i j
  obtain (h | h) := hf i j <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Dual

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
f : (i : ι) → Dual R (M i)
m : (i : ι) → M i
⊢ (dualDistrib ((tprod R) fun i ↦ f i)) (⨂ₜ[R] (i : ι), m i) = ∏ i, (f i) (m i)

Tactic:
rw [dualDistrib, Subsingleton.elim (Fintype.ofFinite ι) ‹_›]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 ((X.toModuleCat ⊗ Y.toModuleCat) ⊗ Z.toModuleCat) ≫ (𝟙 (X.toModuleCat ⊗ Y.toModuleCat) ⊗ₘ 𝟙 Z.toModuleCat)) ≫
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom ≫
        𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat) ≫ 𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat)

Tactic:
Category.id_comp,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 (X.toModuleCat ⊗ Y.toModuleCat) ⊗ₘ 𝟙 Z.toModuleCat) ≫
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom ≫
        𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat) ≫ 𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat)
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 (X.toModuleCat ⊗ Y.toModuleCat) ⊗ₘ 𝟙 Z.toModuleCat) ≫
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom ≫
        𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat) ≫ 𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat)

Tactic:
Category.id_comp,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X Y Z : QuadraticModuleCat R
⊢ (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom =
    (𝟙 (X.toModuleCat ⊗ Y.toModuleCat) ⊗ₘ 𝟙 Z.toModuleCat) ≫
      (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).hom ≫ 𝟙 (X.toModuleCat ⊗ Y.toModuleCat ⊗ Z.toModuleCat)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
m₁ : M₁
m₃ : M₃
m₁' : M₁
m₃' : M₃
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))))
              m₁)
            m₃))
        m₁')
      m₃' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₃))) m₁) m₃))
        m₁')
      m₃'

Tactic:
simp [h₁, h₃, associated_tmul]

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✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ sigPos Q + Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 M

Tactic:
rw [← hr]

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ Module.finrank 𝕜 ↥Vp + Module.finrank 𝕜 ↥V ≤ 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ span R (range h)
⊢ x j (Sum.inl i) = 0

Tactic:
by
  induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]

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 i = P.root l
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 n = P.root k - 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
contra : P.root n = -P.root i
⊢ 2 • P.root n = P.root m

Tactic:
← two_nsmul,

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 i = P.root l
h₂ : P.root k - P.root j = P.root m
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : 2 • P.root n = P.root k - 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
contra : P.root n = -P.root i
⊢ 2 • P.root n = P.root m
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✝⁹ : 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)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
contra : P.root l = P.root ↑i + P.root k
⊢ P.root l = P.root j + (n + 1) • P.root ↑i

Tactic:
rw [contra, hk₁]; module

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

Goal state before:
pp: case inl.inl
ι : 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 k l : ↥b.support
⊢ ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)

Tactic:
simp [h, e]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
⊢ (allRoots P).Nodup

Tactic:
have hli : Injective (Fintype.linearCombination ℤ ![shortRoot P, longRoot P]) := by
    rw [← linearIndependent_iff_injective_fintypeLinearCombination]
    exact (linearIndependent_short_long P).restrict_scalars' ℤ
  rw [allRoots_eq_map_allCoeffs, nodup_map_iff hli]
  decide

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι),
      P.root j ∉ Submodule.span R (⇑P.root '' {long P, short P}) → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R (⇑P.root '' {long P, short P}) = ⊤
⊢ Submodule.span R {longRoot P, shortRoot P} = ⊤

Tactic:
rw [show P.root '' {long P, short P} = {longRoot P, shortRoot P} by aesop] at this

Goal state after:
ι : 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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
⊢ Submodule.span R {longRoot P, shortRoot P} = ⊤
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
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j✝ j : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : ∀ (k : ↥b.support), u k ∈ U
k : ↥b.support
⊢ u k ∈ ωConjLieSubmodule U

Tactic:
simp [hωu, hU]

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 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
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
aux₃ : ∀ (x : ι), x ≠ m → ¬(P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x)
aux₄ : ∀ (x : ι), x ≠ l' → ¬(P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j)
⊢ P.root k = P.root l' - P.root ↑j

Tactic:
by rw [hl', hk]

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)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ Measurable (Finset.restrict₂ hJI)

Tactic:
· exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ s.restrict f' ∈ S

Tactic:
simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
hS : MeasurableSet S
⊢ ∃ s_1 S_1, MeasurableSet S_1 ∧ (cylinder s S)ᶜ = cylinder s_1 S_1

Tactic:
refine ⟨s, Sᶜ, hS.compl, ?_⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Finset ι
S : Set ((i : ↥s) → α ↑i)
hS : MeasurableSet S
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr.a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ instWithTopOfOrderTopology ≤ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Goal state after:
case inr.a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
⊢ {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ⊆ {s | IsOpen[instWithTopOfOrderTopology] s}
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ ∃ I, ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧ (↑I).PairwiseDisjoint id ∧ Set.Ioc u v \ Set.Ioc u' v' = ⋃₀ ↑I

Tactic:
rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ ∃ I, ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} ∧ (↑I).PairwiseDisjoint id ∧ Set.Ioc u u' ∪ Set.Ioc v' v = ⋃₀ ↑I
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
⊢ generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} ≤ Preorder.topology (WithTop ι)

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Goal state after:
case a
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
⊢ {s | ∃ a, s = Ioi a ∨ s = Iio a} ⊆ {s | IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] s}
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case base
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
refine ⟨{{u}}, finite_singleton {u},
      fun a ha ↦ eq_of_mem_singleton ha ▸ finite_singleton u,
      fun a ha t ht ↦ ?_, by simp⟩
    rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *
    exact Or.inl u_mem

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_mem
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ⋃₀ ↑(Finset.image f a) ∈ C

Tactic:
rwa [← A]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ⋃ i, ![s, t] i ∈ C

Tactic:
rwa [← A]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∑ s ∈ J, m (s ∩ t) = m t

Tactic:
nth_rewrite 2 [this]

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
this : t = ⋃ s ∈ J, s ∩ t
⊢ ∑ s ∈ J, m (s ∩ t) = m (⋃ s ∈ J, s ∩ t)