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
h_inj : Injective v'
⊢ LinearIndependent L (⇑b' ∘ v')

Tactic:
exact b'.linearIndependent.comp _ h_inj

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
this : ∀ (j : Fin (n + 1)), (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det

Tactic:
by
    rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (M.submatrix i.succ.succAbove id).updateRow i (∑ k, -1 • M.submatrix i.succ.succAbove id k) a b =
    M.submatrix i.castSucc.succAbove id a b

Tactic:
simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (if a = i then -∑ x, M (i.succ.succAbove x) b else M (i.succ.succAbove a) b) = M (i.castSucc.succAbove a) b
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑A 1 0 = 0
⊢ (↑(reduceStep A) 1 0).natAbs < (↑A 1 0).natAbs

Tactic:
zify
    exact reduce_aux h

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

Goal state before:
pp: m : ℤ
a : FixedDetMatrix (Fin 2) ℤ m
h : ¬↑a 1 0 = 0
⊢ (↑(reduceStep a) 1 0).natAbs < (↑a 1 0).natAbs

Tactic:
zify
    exact reduce_aux h

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✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
⊢ ∃ j, 0 < A i j

Tactic:
by
  let : Quiver n := toQuiver A
  by_contra h_row
  have no_out : ∀ j : n, IsEmpty (i ⟶ j) :=
    fun j => ⟨fun e => h_row ⟨j, e.down⟩⟩
  obtain ⟨j, hij⟩ := exists_pair_ne n
  obtain ⟨p, hp_pos⟩ := h_irr.connected i j
  have h_le : 1 ≤ p.length := Nat.succ_le_of_lt hp_pos
  have ⟨v, p₁, p₂, _hp_eq, hp₁_len⟩ := p.exists_eq_comp_of_le_length (n := 1) h_le
  have hlen_ne : p₁.length ≠ 0 := by simp [hp₁_len]
  obtain ⟨c, p', e, rfl⟩ := (Quiver.Path.length_ne_zero_iff_eq_cons (p := p₁)).1 (by lia)
  obtain ⟨rfl⟩ : i = c := Quiver.Path.eq_of_length_zero p' (by simp_all)
  exact (no_out _).false e

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

Goal state before:
pp: case succ.mpr.cons
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
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j

Tactic:
have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down

Goal state after:
case succ.mpr.cons
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
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
h_prod : 0 < (A ^ m) i b * A b j
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case mp
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
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
⊢ ∃ k > 0, 0 < (A ^ k) i j

Tactic:
obtain ⟨p, hp_len⟩ := h_irr.2 i j

Goal state after:
case mp
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
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
⊢ ∃ k > 0, 0 < (A ^ k) i j
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
⊢ Path c i

Tactic:
have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down

Goal state after:
case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
eT : 0 < Aᵀ c b
⊢ Path c i
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ (fromDFinsuppEquiv κ R).symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)

Tactic:
DirectSum.lof,

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ (fromDFinsuppEquiv κ R).symm f p = f.compLinearMap fun i ↦ DFinsupp.lsingle (p 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) • (tprod R) (update (fun i ↦ 1) i 1)

Tactic:
update_eq_self,

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 • 1) • ⨂ₜ[R] (i : ι), 1
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝² : CommRing R
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
j : (i : ι) → γ i
⊢ (Submodule.span R (Set.range fun j ↦ ⨂ₜ[R] (i : ι), g (j i))).mkQ (⨂ₜ[R] (i : ι), g (j i)) =
    0 (⨂ₜ[R] (i : ι), g (j i))

Tactic:
simp only [Submodule.mkQ_apply, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝² : CommRing R
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
j : (i : ι) → γ i
⊢ (⨂ₜ[R] (i : ι), g (j i)) ∈ Submodule.span R (Set.range fun j ↦ ⨂ₜ[R] (i : ι), g (j i))
Module: Mathlib.LinearAlgebra.Projectivization.Collinear

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

Tactic:
| h v hv =>

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Projectivization.mk K v hv ∉ ⊥

Tactic:
| h v hv =>

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

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

Tactic:
| h v hv =>

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
y : ℙ K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
hp3 : y ∈ Submodule.projectivization p
hq3 : y ∈ Submodule.projectivization q
v : V
hv : v ≠ 0
hxy : mk K v hv ≠ y
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
⊢ p = q

Tactic:
| h v hv =>

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : PSLAction.toPermHom g = 1
⊢ g = 1

Tactic:
← MonoidHom.mem_ker,

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : g ∈ PSLAction.toPermHom.ker
⊢ g = 1
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
⊢ Q.radical = LinearMap.ker (associated Q)

Tactic:
rw [radical_eq_ker_polarBilin]
  ext m
  simp [associated_apply, LinearMap.ext_iff, QuadraticMap.polar, invOf_smul_eq_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
m₂ : M₂
m₁' : M₁
m₂' : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                (LinearMap.compl₁₂ (LinearMap.BilinForm.tmul (associated Q₂) (associated Q₁))
                  ↑(TensorProduct.comm R M₁ M₂) ↑(TensorProduct.comm R M₁ M₂)))
              m₁)
            m₂))
        m₁')
      m₂' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry (LinearMap.BilinForm.tmul (associated Q₁) (associated Q₂))) m₁)
            m₂))
        m₁')
      m₂'

Tactic:
exact mul_comm _ _

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 : ι
hi :
  ¬P.root i = longRoot P ∧
    ¬P.root i = -longRoot P ∧
      ¬P.root i = shortRoot P ∧
        ¬P.root i = -shortRoot P ∧
          ¬P.root i = shortAddLongRoot P ∧
            ¬P.root i = -shortAddLongRoot P ∧
              ¬P.root i = twoShortAddLongRoot P ∧
                ¬P.root i = -twoShortAddLongRoot P ∧
                  ¬P.root i = threeShortAddLongRoot P ∧
                    ¬P.root i = -threeShortAddLongRoot P ∧
                      ¬P.root i = threeShortAddTwoLongRoot P ∧ ¬P.root i = -threeShortAddTwoLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0

Tactic:
obtain ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀, h₁₁, h₁₂⟩ := hi

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
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
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
χ : ↥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
⊢ d i = χ x ∧ k ≠ 0

Tactic:
simpa [hi, mulVec_eq_sum, diagonal_apply, sub_eq_zero] using! congr_fun hk (Sum.inr i)

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
  rw [SModEq.sub_mem] at h ⊢
  rw [← Commute.mul_neg_geom_sum₂ (.all _ _)]
  refine Ideal.mul_mem_mul h ?_
  have h₂ : (p : R ⧸ I) = 0 := by simpa using Ideal.Quotient.eq_zero_iff_mem.mpr hpI
  simp only [← Ideal.Quotient.eq_zero_iff_mem, map_sum, map_mul, map_pow, h₁, ← pow_add]
  trans ∑ x ∈ Finset.range p, Ideal.Quotient.mk I y ^ (p - 1)
  · exact Finset.sum_congr rfl fun _ _ ↦ by grind
  simp [h₂]

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

Goal state before:
pp: case mul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b c : SymmetricAlgebra R M
hb : Commute a b
hc : Commute a c
⊢ Commute a (b * c)

Tactic:
| mul b c hb hc =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Bijective ⇑(lift (ι R M))

Tactic:
lift_ι

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Bijective ⇑(AlgHom.id R (SymmetricAlgebra R M))
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' : κ
⊢ (bN'.repr (g (bN j'))) j • (bM'.repr (f (bM i'))) i = (bM'.repr (f (bM i'))) i * (bN'.repr (g (bN j'))) j

Tactic:
exact mul_comm _ _

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 f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule

Tactic:
have := finrank_fixedSubmodule_add_le e f

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 f : V ≃ₗ[K] V
hf : f ∈ dilatransvections K V
this :
  finrank K ↥(↑e).fixedSubmodule + finrank K ↥(↑f).fixedSubmodule ≤
    finrank K ↥((↑e).fixedSubmodule ⊔ (↑f).fixedSubmodule) + finrank K ↥(↑(e * f)).fixedSubmodule
⊢ finrank K ↥(↑e).fixedSubmodule ≤ 1 + finrank K ↥(↑(e * f)).fixedSubmodule
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
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ (↑e).fixedSubmodule ⊔ K ∙ v = (↑(transvection hfv * e)).fixedSubmodule

Tactic:
apply Submodule.eq_of_le_of_finrank_le this

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
this : (↑e).fixedSubmodule ⊔ K ∙ v ≤ (↑(transvection hfv * e)).fixedSubmodule
⊢ finrank K ↥(↑(transvection hfv * e)).fixedSubmodule ≤ finrank K ↥((↑e).fixedSubmodule ⊔ K ∙ v)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case intro
α : Type u_1
r : α → α → Prop
inst✝ : Std.Irrefl r
a✝ : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ {a}.erase a + t → Acc (CutExpand r) {a'}

Tactic:
rw [erase_singleton, zero_add]

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

Goal state before:
pp: case right
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
⊢ v ∈ (↑(transvection hfv * e)).fixedSubmodule

Tactic:
simp only [mem_fixedSubmodule_iff, LinearEquiv.coe_toLinearMap,
      LinearEquiv.mul_apply, transvection.apply]

Goal state after:
case right
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 v + f (e v) • (v - e v) = v
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
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + finrank K ↥(W ⊔ K ∙ v) = finrank K V
h2 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)

Tactic:
finrank_sup_span_singleton hv

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
W : Submodule K V
v : V
hv : v ∉ W
h1 : finrank K (V ⧸ W ⊔ K ∙ v) + (finrank K ↥W + 1) = finrank K V
h2 : finrank K (V ⧸ W) + finrank K ↥W = finrank K V
⊢ finrank K (V ⧸ W ⊔ K ∙ v) + 1 = finrank K (V ⧸ W)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case neg
ι : 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, not_false_iff, dif_neg, MeasurableSet.univ]

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

Goal state before:
pp: case inl
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 g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : y ∈ (↑e).fixedSubmodule
k : K
hk : y + k • v = v - e v
⊢ 1 = 0

Tactic:
refine (hv (k - 1) 1 ?_).right

Goal state after:
case inl
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 g : Dual K V
v : V
a b : K
hv : ∀ (s t : K), s • (↑e).fixedSubmodule.mkQ v + t • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0 → s = 0 ∧ t = 0
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c = 0
y : V
hy : y ∈ (↑e).fixedSubmodule
k : K
hk : y + k • v = v - e v
⊢ (k - 1) • (↑e).fixedSubmodule.mkQ v + 1 • e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = 0
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
hC : IsSetSemiring C
m : AddContent G C
s : Set α
hs : s ∈ C
⊢ ↑{s} ⊆ C

Tactic:
by simp [hs]

Goal state after: