mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)

Tactic:
by
  rw [sSup_eq_iSup]
  exact iSup₂ h

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight 1
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ n * m = ∑ i_1 ∈ i.support, n * i i_1

pp: case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ∀ i_1 ∈ i.support, ((fun n e ↦ g n ^ e) i_1 (i i_1)).IsHomogeneous (n * i i_1)

Tactic:
· rw [Finsupp.mem_support_iff] at hi
    rw [← Finset.mul_sum, ← hφ hi, weight_apply]
    simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]

Goal state after:
case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ∀ i_1 ∈ i.support, ((fun n e ↦ g n ^ e) i_1 (i i_1)).IsHomogeneous (n * i i_1)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
⊢ toMvPolynomial (basis A b) (basis A bₘ).end (tensorProduct R A M M ∘ₗ baseChange A φ) ij =
    (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b bₘ.end φ ij)

Tactic:
toMvPolynomial_comp _ (basis A (Basis.end bₘ)),

Goal state after:
case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
⊢ (bind₁ (toMvPolynomial (basis A b) (basis A bₘ.end) (baseChange A φ)))
      (toMvPolynomial (basis A bₘ.end) (basis A bₘ).end (tensorProduct R A M M) ij) =
    (MvPolynomial.map (algebraMap R A)) (toMvPolynomial b bₘ.end φ ij)
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ∑ j, (monomial (Finsupp.single j 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij j) =
    X ij

Tactic:
Finset.sum_eq_single ij

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ (monomial (Finsupp.single ij 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij ij) = X ij

case h₀
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ∀ b ∈ Finset.univ,
    b ≠ ij →
      (monomial (Finsupp.single b 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij b) = 0

case h₁
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij : ιM × ιM
this :
  ∀ (kl : ιM × ιM),
    (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
⊢ ij ∉ Finset.univ →
    (monomial (Finsupp.single ij 1)) ((toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij ij) = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij kl : ιM × ιM
⊢ ((basis A bₘ).end.repr ((tensorProduct R A M M) ((basis A bₘ.end) kl))) ij = if kl = ij then 1 else 0

Tactic:
tensorProduct,

Goal state after:
case e_f.hX
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ιM : Type u_7
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ιM
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ιM
b : Basis ι R L
bₘ : Basis ιM R M
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
ij kl : ιM × ιM
⊢ ((basis A bₘ).end.repr
        ((TensorProduct.AlgebraTensorModule.lift
            { toFun := fun a ↦ a • baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ })
          ((basis A bₘ.end) kl)))
      ij =
    if kl = ij then 1 else 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case succ.inr
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
⊢ ∃ r, (eval r) F ≠ 0

Tactic:
have hφR : φ.natDegree < #R := by
      refine lt_of_lt_of_le ?_ hnR
      norm_cast
      refine lt_of_le_of_lt natDegree_map_le ?_
      suffices (finSuccEquiv _ _ F).natDegree ≠ n by lia
      rintro rfl
      refine leadingCoeff_ne_zero.mpr ?_ hFn
      simpa using! (finSuccEquiv R N).injective.ne hF₀

Goal state after:
case succ.inr
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
i : ℕ
hi : ((finSuccEquiv R N) F).coeff i ≠ 0
hin✝ : i ≤ n
hFn : ((finSuccEquiv R N) F).coeff n = 0
hin : i < n
j : ℕ
hj : i + (j + 1) = n
r : Fin N → R
hr : (eval r) (((finSuccEquiv R N) F).coeff i) ≠ 0
φ : R[X] := Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ : φ = Polynomial.map (eval r) ((finSuccEquiv R N) F)
hφ₀ : φ ≠ 0
hφR : ↑φ.natDegree < #R
⊢ ∃ r, (eval r) F ≠ 0
Module: Mathlib.Algebra.Lie.Character

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅χ x, χ y⁆ = 0

Tactic:
rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := ⋯
bₘ : Basis (ChooseBasisIndex R M) R M := ⋯
n : ℕ := ⋯
aux : ((φ.polyCharpoly b).coeff φ.nilRank).IsHomogeneous (n - φ.nilRank)
x : ChooseBasisIndex R L → R
hx : (eval x) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
c : ChooseBasisIndex R L →₀ R := ⋯
⊢ φ.IsNilRegular (b.repr.symm c)

Tactic:
rwa [isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero _ b, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R

Tactic:
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R),
    fromBlocks_smul, Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]

Goal state after:
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr.refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ((toEnd K ↥U ↥E) (α • u + x')) ⟨↑z, ⋯⟩ = 0

Tactic:
change ⁅z, _⁆ = (0 : E)
      ext
      exact lie_self z.1

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

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).rank ≤ A.rank

Tactic:
nontriviality R
  have := Module.Finite.span_of_finite R (Set.finite_range (A.submatrix r id).col)
  calc
    _ = (((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ).rank := by simp
    _ ≤ finrank R (span R (range (A.submatrix r id).col)) := by
      rw [rank, Matrix.mulVecLin_transpose, Matrix.transpose_submatrix, transpose_transpose,
        range_vecMulLinear, ← Matrix.transpose_submatrix, row_transpose]
      exact Submodule.finrank_mono (Submodule.span_mono (fun v ⟨j, hj⟩ => ⟨c j, hj⟩))
    _ = (A.submatrix r id)ᵀᵀ.rank := by
      rw [rank, Matrix.mulVecLin_transpose, range_vecMulLinear]
      rfl
    _ = (A.submatrix r (Equiv.refl n)).rank := by simp
  rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
    show LinearMap.funLeft R R (Equiv.refl n).symm = LinearEquiv.funCongrLeft R R
      (Equiv.refl n).symm from rfl, LinearEquiv.range, Submodule.map_top]
  exact Submodule.finrank_map_le _ _

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ toNat (Module.rank R ↥(toLin' (diagonal w)).range) = Fintype.card { i // w i ≠ 0 }

Tactic:
← LinearMap.rank,

Goal state after:
m : Type um
R : Type uR
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ toNat (toLin' (diagonal w)).rank = Fintype.card { i // w i ≠ 0 }
Module: Mathlib.Algebra.Lie.Graded

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) ⁅x, y⁆ =
    ⁅x, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) y⁆ -
      ⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) x⁆

Tactic:
have hM (k : ι) (b : ⨁ i, ℒ i) (hb : (decompose ℒ).symm b ∈ ℒ k) :
          (toModule R ι (⨁ (i : ι), ℒ i) fun i ↦ lof R ι (ℒ ·) i ∘ₗ (φ i • .id)) b = (φ k) • b := by
        obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]
        simp

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid ι
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
ℒ : ι → Submodule R L
inst✝ : GradedLieAlgebra ℒ
φ : ι →+ R
x y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i)),
    (decompose ℒ).symm b ∈ ℒ k →
      (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ (φ i • LinearMap.id)) b = φ k • b
⊢ (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) ⁅x, y⁆ =
    ⁅x, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) y⁆ -
      ⁅y, (toModule R ι (⨁ (i : ι), ↥(ℒ i)) fun i ↦ lof R ι (fun x ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯) x⁆
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
m : ℕ
hm : m < (p.toList x).length
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm⟩ → ⟨n, hn⟩ = ⟨m, hm⟩

Tactic:
rw [length_toList, ← hc.orderOf] at hm hn

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : ¬p x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ (fun i ↦ (p.toList x)[↑i]) ⟨n, hn✝⟩ = (fun i ↦ (p.toList x)[↑i]) ⟨m, hm✝⟩ → ⟨n, hn✝⟩ = ⟨m, hm✝⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
⊢ (if f x = x then if f y = y then s else ↑(f.toList y) else ↑(f.toList x)) =
    if f y = y then if f x = x then s else ↑(f.toList x) else ↑(f.toList y)

Tactic:
split_ifs with hx hy hy

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : f y = y
⊢ s = s

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : f x = x
hy : ¬f y = y
⊢ ↑(f.toList y) = ↑(f.toList y)

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : f y = y
⊢ ↑(f.toList x) = ↑(f.toList x)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
f : Perm α
hf : f.IsCycle
x y : α
m✝ : Multiset α
s : Cycle α
hx : ¬f x = x
hy : ¬f y = y
⊢ ↑(f.toList x) = ↑(f.toList y)
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

Tactic:
by_cases h0 : a + b + c = 0

Goal state after:
case pos
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x

case neg
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : ¬a + b + c = 0
⊢ b • (Φ ((Finsupp.single (a + c) ⁅x, z⁆) (-b))) y =
    c • (Φ ((Finsupp.single (a + b) ⁅x, y⁆) (-c))) z + a • (Φ ((Finsupp.single (b + c) ⁅y, z⁆) (-a))) x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case stop
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : ¬lo < n
⊢ 0 = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
Finset.Ico_eq_empty hlo,

Goal state after:
case stop
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : ¬lo < n
⊢ 0 = ∑ k ∈ ∅, f k
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
⊢ ⁅x, E.toKer.symm ⟨s₁ y - s₂ y, ⋯⟩⁆ - ⁅y, E.toKer.symm ⟨s₁ x - s₂ x, ⋯⟩⁆ - E.toKer.symm ⟨s₁ ⁅x, y⁆ - s₂ ⁅x, y⁆, ⋯⟩ =
    E.toKer.symm ⟨⁅s₁ x, s₁ y⁆ - s₁ ⁅x, y⁆, ⋯⟩ - E.toKer.symm ⟨⁅s₂ x, s₂ y⁆ - s₂ ⁅x, y⁆, ⋯⟩

Tactic:
nth_rw 1 [← hs x]

Goal state after:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : LieRing M
inst✝¹ : LieAlgebra R M
inst✝ : IsLieAbelian M
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x y : L
s : L → E.L
hs : ∀ (b : L), E.proj (s b) = b
this : ∀ {s' : L → E.L}, LeftInverse (⇑E.proj) s' → ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
⊢ ⁅E.proj (s x), E.toKer.symm ⟨s₁ y - s₂ y, ⋯⟩⁆ - ⁅y, E.toKer.symm ⟨s₁ x - s₂ x, ⋯⟩⁆ -
      E.toKer.symm ⟨s₁ ⁅x, y⁆ - s₂ ⁅x, y⁆, ⋯⟩ =
    E.toKer.symm ⟨⁅s₁ x, s₁ y⁆ - s₁ ⁅x, y⁆, ⋯⟩ - E.toKer.symm ⟨⁅s₂ x, s₂ y⁆ - s₂ ⁅x, y⁆, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: i j : Fin 2
h : i ≠ j
⊢ G₂ i j ≤ 0

Tactic:
by
  fin_cases i <;> fin_cases j <;> simp_all [G₂]

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

Goal state before:
pp: case mp
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
⊢ A.IsSimplyLaced → ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1

Tactic:
intro h i j hij

Goal state after:
case mp
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : A.IsSimplyLaced
i j : ι
hij : j < i
⊢ A i j = 0 ∨ A i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case mpr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
⊢ (∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1) → A.IsSimplyLaced

Tactic:
intro h i j hij

Goal state after:
case mpr
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : ∀ ⦃i j : ι⦄, j < i → A i j = 0 ∨ A i j = -1
i j : ι
hij : i ≠ j
⊢ A i j = 0 ∨ A i j = -1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ I = 1

Tactic:
@SetLike.ext_iff _ _ _ I 1,

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
⊢ ∀ (x : L), x ∈ I ↔ x ∈ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
⊢ (∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J) → ∀ z ∈ I, x * z ∈ J

Tactic:
intro h zI hzI
    exact h x ⟨1, one_smul _ _⟩ zI hzI

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ (I ⊔ J) * (I ⊓ J) = I * J

Tactic:
have hlcm : lcm I J = I ⊓ J := by
    rw [lcm_eq_normalize _ _, normalize_eq]
    · rw [lcm_dvd_iff, dvd_iff_le, dvd_iff_le]
      simp
    · rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
      exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
hlcm : lcm I J = I ⊓ J
⊢ (I ⊔ J) * (I ⊓ J) = I * J
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra R K
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Module R V
inst✝⁴ : IsScalarTower R K V
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsFractionRing R K
M : Submodule R V
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = Module.rank K V

Tactic:
by
  let b := Module.Free.chooseBasis R M
  rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]

Goal state after:
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : IsFractionRing R K
M : Submodule R (ι → K)
inst✝ : IsLattice K M
⊢ Module.rank R ↥M = ↑(Fintype.card ι)

Tactic:
rw [IsLattice.rank' K M]
  simp

Goal state after: