mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
i j : n
⊢ 0 < (A ^ k) i j ↔ Nonempty { p // p.length = k }

Tactic:
let := toQuiver A
  induction k generalizing i j with
  | zero =>
    refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩
    · rcases eq_or_ne i j with rfl | h_eq
      · exact ⟨⟨Quiver.Path.nil, rfl⟩⟩
      · simp_all
    · simp [Quiver.Path.eq_of_length_zero p hp]
  | succ m ih =>
    rw [pow_succ, mul_apply]
    constructor
    · intro h_pos
      obtain ⟨l, hl_mem, hl_pos⟩ :
          ∃ l ∈ (Finset.univ : Finset n), 0 < (A ^ m) i l * A l j := by
        simpa [Finset.sum_pos_iff_of_nonneg
                 (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))]
          using h_pos
      have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l
      have hA_nonneg' : 0 ≤ A l j := hA l j
      have h_Am : 0 < (A ^ m) i l := by by_contra! h; simp [le_antisymm h hAm_nonneg] at hl_pos
      have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_pos
      obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am
      exact ⟨p.cons (PLift.up h_A), by simp⟩
    · rintro ⟨p, hp_len⟩
      cases p with
      | nil => simp [Quiver.Path.length] at hp_len
      | @cons b _ q e =>
        simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len
        have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
        let h_A_pos := e
        have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down
        exact
          (Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

Goal state after:
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✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ A.IsIrreducible

Tactic:
rw [isIrreducible_iff_exists_pow_pos h_nonneg]

Goal state after:
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ (C (reduce (reduceStep A)) → C (reduceStep A)) → C (reduce A) → C A

Tactic:
ih

Goal state after:
case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
⊢ C (reduce A) → C A
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
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
p : Path j i
hp_pos : 0 < p.length
⊢ ∃ p, 0 < p.length

Tactic:
cases p with
  | nil =>
    simp at hp_pos
  | @cons b _ q e =>
    let qT := transposePath (A := A) (q.cons e)
    let : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv ((tprod R) fun i ↦ DFinsupp.single (p i) (x i)) = DFinsupp.single p ((tprod R) fun i ↦ x i)

Tactic:
simp [ofDFinsuppEquiv]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
κ : ι → Type u_3
M : (i : ι) → κ i → Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝³ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ ofDFinsuppEquiv.symm (DFinsupp.single p ((tprod R) x)) = (tprod R) fun i ↦ DFinsupp.single (p i) (x i)

Tactic:
simp [ofDFinsuppEquiv]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ (LinearEquiv.lTensor (⨂[R] (i₁ : { i // ¬i = i₀ }), M ↑i₁) (subsingletonEquiv ()))
      ((tmulEquivDep R fun i ↦
            M ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm i))).symm
        ((reindex R M ((Equiv.optionSubtypeNe i₀).symm.trans (Equiv.optionEquivSumPUnit { i // ¬i = i₀ })))
          (⨂ₜ[R] (i : ι), m i))) =
    ((tprod R) fun j ↦ m ↑j) ⊗ₜ[R] m i₀

Tactic:
dsimp% this,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
this :
  (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
⊢ (LinearEquiv.lTensor (⨂[R] (i₁ : { i // ¬i = i₀ }), M ↑i₁) (subsingletonEquiv ()))
      ((tmulEquivDep R fun i ↦
            M ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm i))).symm
        ((tprod R) fun j ↦ m ((Equiv.optionSubtypeNe i₀) ((Equiv.optionEquivSumPUnit { i // ¬i = i₀ }).symm j)))) =
    ((tprod R) fun j ↦ m ↑j) ⊗ₜ[R] m i₀
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
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span (↑W ∪ S)

Tactic:
rw [span_union, span_coe]

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
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span (S ∪ ↑W)

Tactic:
rw [span_union, span_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ n ∈ (M'.liftQ f hM').flip.ker

Tactic:
LinearMap.mem_ker,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ (M'.liftQ f hM').flip n = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker

Tactic:
LinearMap.mem_ker,

Goal state after:
case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ (LinearMap.flip Q.polarBilin) n = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Field 𝕜
inst✝¹ : NeZero 2
inst✝ : Fintype ι
w : ι → 𝕜
⊢ (weightedSumSquares 𝕜 w).radical = Pi.spanSubset 𝕜 {i | w i = 0}

Tactic:
classical
  ext v
  simp only [mem_radical_iff', weightedSumSquares_apply, ← pow_two, smul_eq_mul, Pi.add_apply,
    add_sq, mul_add, sum_add_distrib, add_eq_right, Pi.mem_spanSubset_iff]
  constructor
  · rintro ⟨hv, hvv'⟩ i
    simpa [hv, Pi.single_apply, NeZero.ne, or_iff_not_imp_left] using hvv' (Pi.single i 1)
  · simpa only [← sum_add_distrib]
      using fun h ↦ ⟨sum_eq_zero (by grind), fun v ↦ sum_eq_zero (by grind)⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
V : Submodule R M
⊢ Module.finrank R ↥⊥ ∈
    {r ∈ Iic (Module.finrank R M) | ∃ V, Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}

Tactic:
by
    simp only [mem_filter, mem_Iic]
    refine ⟨?_, ⟨⊥, rfl, fun x hx' ↦ (hx' <| Subsingleton.elim x 0).elim⟩⟩
    nontriviality R
    simp [finrank_bot]

Goal state after:
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:
rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]

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

𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ Disjoint {i | w i < 0} {i | w i = 0}
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:
rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]

Goal state after:
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
hkl : l ≠ k
⊢ 0 < P.pairingIn ℤ l i

Tactic:
replace hkl : P.pairingIn ℤ l k ≤ 0 := by
    suffices α l - α k ∉ Φ by contrapose! this; exact P.root_sub_root_mem_of_pairingIn_pos this hkl
    replace hl : α l - α k = α i - α j := by rw [hl]; module
    rw [hl]
    exact b.sub_notMem_range_root hi hj

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
hkl : P.pairingIn ℤ l k ≤ 0
⊢ 0 < P.pairingIn ℤ l i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : 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
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (threeShortAddLongRoot P) =
    3 * (2 * (B.form (P.root i)) (shortRoot P)) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
rw [threeShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]; ring

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
i : ι
⊢ P.pairingIn ℤ i (threeShortAddLong P) = P.pairingIn ℤ i (short P) + P.pairingIn ℤ i (long P)

Tactic:
suffices P.pairing i (threeShortAddLong P) =
      P.pairing i (short P) + P.pairing i (long P) from
    algebraMap_injective ℤ R <| by simpa only [algebraMap_pairingIn, map_add, map_mul, map_ofNat]
  have : Fintype ι := Fintype.ofFinite ι
  have B := (P.posRootForm ℤ).toInvariantForm
  apply mul_right_cancel₀ (B.ne_zero <| threeShortAddLong P)
  calc P.pairing i (threeShortAddLong P) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P)
    _ = 2 * B.form (P.root i) (threeShortAddLongRoot P) := ?_
    _ = 3 * (2 * B.form (P.root i) (shortRoot P)) + 2 * B.form (P.root i) (longRoot P) := ?_
    _ = P.pairing i (short P) * B.form (longRoot P) (longRoot P) +
          P.pairing i (long P) * B.form (longRoot P) (longRoot P) := ?_
    _ = (P.pairing i (short P) + P.pairing i (long P)) *
          B.form (threeShortAddLongRoot P) (threeShortAddLongRoot P) := ?_
  · rw [B.two_mul_apply_root_root]
  · rw [threeShortAddLongRoot_eq, map_add, mul_add, map_smul, smul_eq_mul]; ring
  · rw [B.two_mul_apply_root_root, B.two_mul_apply_root_root, long_eq_three_mul_short]; ring
  · rw [threeShortAddLongRoot_longRoot]; ring

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
⊢ LinearIndependent R ![shortRoot P, longRoot P]

Tactic:
have := pairing_long_short P
    refine (IsReduced.linearIndependent_iff P).mpr ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · norm_num [h] at this
    · simp only [root_eq_neg_iff] at h
      norm_num [h] at this

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD J]
hJI : J ≤ I
⊢ x ^ p ≡ y ^ p [SMOD J * I]

Tactic:
have h₁ := idealQuotientMk.mp <| h.mono hJI

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD J]
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x ^ p ≡ y ^ p [SMOD J * I]
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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : ∑ x, |b.cartanMatrix j x| • c x • v b ↑j ∈ U
⊢ v b ↑j ∈ U

Tactic:
← smul_assoc,

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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬∑ k, c k * ↑|b.cartanMatrix j k| = 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b ↑j
this : ∑ x, (|b.cartanMatrix j x| • c x) • v b ↑j ∈ U
⊢ v b ↑j ∈ U
Module: Mathlib.LinearAlgebra.TensorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (DirectSum.coeAlgHom fun x ↦ (ι R).range ^ x).comp ((lift R) (GradedAlgebra.ι R M)) = AlgHom.id R (TensorAlgebra R M)

Tactic:
ext m
      dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply,
        AlgHom.id_apply]
      rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ((bM'.tensorProduct bN').repr ((map f g) ((bM.tensorProduct bN) (i', j')))) (i, j) =
    (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j

Tactic:
Basis.tensorProduct_apply,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ((bM'.tensorProduct bN').repr ((map f g) (bM i' ⊗ₜ[R] bN j'))) (i, j) =
    (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ (toFinsupp s) b = (toFinsupp t) b

Tactic:
toFinsupp_apply

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ count b s = count b t
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ (toFinsupp s) a < (toFinsupp t) a

Tactic:
toFinsupp_apply

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ count a s < count a t
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
W : Submodule K V
v : V
hv : v ∉ W
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)

Tactic:
by
  have h1 := finrank_quotient_add_finrank (W ⊔ K ∙ v)
  have h2 := finrank_quotient_add_finrank W
  rw [finrank_sup_span_singleton hv] at h1
  omega

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.mkQ.ker

Tactic:
LinearMap.mem_ker,

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 v) = 0
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder s S ∩ cylinder t T = ∅ ↔ Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T = ∅

Tactic:
inter_cylinder,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α ↑i)
T : Set ((i : ↥t) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder (s ∪ t) (Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T) = ∅ ↔
    Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' 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
⊢ ⨆ i ∈ Δ, MeasurableSpace.comap (fun x ↦ g x i) (m i) ≤ mα ↔
    ∀ ⦃i : ι⦄, i ∈ Δ → MeasurableSpace.comap (fun a ↦ g a i) (m i) ≤ mα

Tactic:
iSup_le_iff

Goal state after: