mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
⊢ ∀ i ∈ Finset.univ,
    (↑↑(Equiv.Perm.sign i) *
          ∏ x,
            ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
              X (some (i x, x)))).IsHomogeneous
      (0 + ∑ i, 1)

Tactic:
rintro i -

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i) *
        ∏ x,
          ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
            X (some (i x, x)))).IsHomogeneous
    (0 + ∑ i, 1)
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]
  exact nonTorsionWeight_of (Function.const σ one_ne_zero)

Goal state after:
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✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ 𝒜₊.toAddSubmonoid = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))

Tactic:
rw [irrelevant_eq_iSup]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ⨆ i, ⨆ (_ : i > 0), ofClass (𝒜 i) = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_4
S : Type u_5
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
M : Matrix m n R
i : m
⊢ (M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)

Tactic:
simp only [toMvPolynomial, map_apply, map_sum, map_monomial]

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

Goal state before:
pp: case convert_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0

Tactic:
exact IsWeightedHomogeneous.weightedHomogeneousComponent_ne m (x n).prop hmn.symm

Goal state after:
Module: Mathlib.Algebra.Lie.Rank

Goal state before:
pp: K : Type u_7
L : Type u_8
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
x : L
⊢ IsRegular K x ↔ finrank K ↥(engel K x) = rank K L

Tactic:
isRegular_iff_natTrailingDegree_charpoly_eq_rank,

Goal state after:
K : Type u_7
L : Type u_8
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
x : L
⊢ (LinearMap.charpoly ((ad K L) x)).natTrailingDegree = rank K L ↔ finrank K ↥(engel K x) = rank K L
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
x : L
i✝ j✝ : ιM
⊢ of (Function.curry fun i ↦ (eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i)) i✝ j✝ = (toMatrix bₘ bₘ) (φ x) i✝ j✝

Tactic:
of_apply,

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
x : L
i✝ j✝ : ιM
⊢ Function.curry (fun i ↦ (eval ⇑(b.repr x)) (toMvPolynomial b bₘ.end φ i)) i✝ j✝ = (toMatrix bₘ bₘ) (φ x) i✝ j✝
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
⊢ F = G

Tactic:
by
  apply funext_of_le_card hF hG h
  exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Goal state after:
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: case inr
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
⊢ Ex ≤ Ey

Tactic:
let Q := L ⧸ E

Goal state after:
case inr
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
⊢ Ex ≤ Ey
Module: Mathlib.LinearAlgebra.Matrix.Diagonal

Goal state before:
pp: m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })

Tactic:
have hIJ : IsCompl { i : m | w i ≠ 0 } { i : m | w i = 0 } := isCompl_compl.symm

Goal state after:
m : Type u_1
inst✝³ : Fintype m
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hIJ : IsCompl {i | w i ≠ 0} {i | w i = 0}
⊢ (toLin' (Matrix.diagonal w)).rank = ↑(Fintype.card { i // w i ≠ 0 })
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁶ : DecidableEq p
inst✝⁵ : DecidableEq q
inst✝⁴ : DecidableEq l
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
⊢ ↥(so' p q R) ≃ₗ⁅R⁆ ↥(so (p ⊕ q) R)

Tactic:
apply
    (skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i)
        (invertiblePso p q R hi)).trans
  apply LieEquiv.ofEq
  ext A; rw [indefiniteDiagonal_transform p q R hi]; rfl

Goal state after:
Module: Mathlib.Algebra.Lie.Semisimple.Lemmas

Goal state before:
pp: case mem
L : Type u_2
M : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : LieRingModule L M
R : Type u_4
inst✝³ : CommRing R
inst✝² : LieAlgebra R L
inst✝¹ : Module R M
inst✝ : LieModule R L M
s : Set L
hs : ∀ x ∈ s, (trace R M) ((toEnd R L M) x) = 0
x u : L
hu : u ∈ s
⊢ (trace R M) ((toEnd R L M) u) = 0

Tactic:
simpa using hs u hu

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
f : { f // f.IsCycle }
⊢ (fun s ↦ ⟨(↑s).formPerm ⋯, ⋯⟩) ((fun f ↦ ⟨(↑f).toCycle ⋯, ⋯⟩) f) = f

Tactic:
obtain ⟨x, hx, -⟩ := id f.prop
    simpa [toCycle_eq_toList (f : Perm α) f.prop x hx, formPerm_toList, Subtype.ext_iff] using
      f.prop.cycleOf_eq hx

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det =
    pminor A α * A i j + ∑ s, (-1) ^ (↑s + 1) * (A.submatrix (Fin.cons i (s.removeNth α)) α).det * A (α s) j

Tactic:
simp only [mul_comm (A i j), mul_right_comm]

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

Goal state before:
pp: R : Type u
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : Module R E
inst✝¹ : Nontrivial E
inst✝ : Module.IsTorsionFree R E
⊢ lift.{v, u} #R ≤ lift.{u, v} #E

Tactic:
by
  obtain ⟨x, hx⟩ : ∃ (x : E), x ≠ 0 := exists_ne 0
  have : Injective (fun k ↦ k • x) := smul_left_injective R hx
  exact lift_mk_le_lift_mk_of_injective this

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
⊢ (fun u ↦ ⟨E.mkSol u, ⋯⟩) ((fun u x ↦ ↑u ↑x) u) = u

Tactic:
ext n; symm; apply E.eq_mk_of_is_sol_of_eq_init u.2; intro k; rfl

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ E.charPoly.leadingCoeff = 1

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ E.charPoly.coeff E.charPoly.natDegree = 1
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ I.rootSpan ∈ (rootSystem H).invtRootSubmodule

Tactic:
rw [RootPairing.mem_invtRootSubmodule_iff]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : CharZero K
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ ∀ (i : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ.refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ c 1 ≠ ⊥

pp: case succ.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
b : Associates M
hb : b < c 1
⊢ b = ⊥

Tactic:
· exact ne_bot_of_gt (h₁ zero_lt_one)

Goal state after:
case succ.refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : Associates M
hq : q ≠ 0
n : ℕ
hn : n + 1 ≠ 0
c : Fin (n + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
b : Associates M
hb : b < c 1
⊢ b = ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ x ∈ ⊥

Tactic:
suffices (den I : R) • x = 0 from
    (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R P
hS : 0 ∉ S
I : FractionalIdeal S P
hI : I.num = ⊥
x : P
hx : x ∈ ↑I
⊢ ↑I.den • x = 0
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
C : P → Prop
r : P
hr : r ∈ I * J
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
⊢ C r

Tactic:
by
  simp only [mul_def] at hr
  exact Submodule.mul_induction_on hr hm ha

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Submonoid R
P : Type u_4
inst✝³ : Nontrivial P
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : Module.IsTorsionFree R P
hR : IsNoetherianRing R
hS : S ≤ R⁰
I : FractionalIdeal S P
⊢ (↑I).FG

Tactic:
have := hR.noetherian I.num
  rw [← Module.Finite.iff_fg] at this ⊢
  exact .equiv (I.equivNum <| coe_ne_zero ⟨(I.den : R), hS (SetLike.coe_mem I.den)⟩).symm

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

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J I : FractionalIdeal A⁰ K
⊢ I / 0 = I * 0⁻¹

Tactic:
simp [inv_zero']

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

Goal state before:
pp: R : Type u_1
A : Type u_2
K✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K✝
inst✝ : IsFractionRing A K✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ ↑J ≤ ↑K

Tactic:
← mul_le_mul_iff_right₀ (α := FractionalIdeal A⁰ (FractionRing A)) (a := I.1)
        (by simpa [pos_iff_ne_zero] using I.2.ne'),

Goal state after:
R : Type u_1
A : Type u_2
K✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K✝
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K✝
inst✝ : IsFractionRing A K✝
I : { x // 0 < x }
J K : Ideal A
e : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) I J) ((fun x y ↦ ↑x * y) I K)
⊢ ↑↑I * ↑J ≤ ↑↑I * ↑K
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x)

Tactic:
rw [mem_canonicalEquiv_apply]

Goal state after:
case mpr
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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
h : y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
⊢ ∃ y_1 ∈ spanSingleton S x, (IsLocalization.map P' (RingHom.id R) ⋯) y_1 = y
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: case prime
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ∀ i ∈ (factors I).toFinset, Prime i

pp: case coprime
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j

Tactic:
· exact prime_of_mem

Goal state after:
case coprime
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
γ : Weight K (↥H) L :=
  { toFun := ⇑(Weight.toLinear K (↥H) L χ) + ⇑(Weight.toLinear K (↥H) L α), genWeightSpace_ne_bot' := h_plus_ne_bot }
hγ_nonzero : γ.IsNonZero
i : ↥LieSubalgebra.root
hi : S.root i = Weight.toLinear K (↥H) L χ
j : ↥LieSubalgebra.root
hj : S.root j = Weight.toLinear K (↥H) L α
h_sum_in_range : S.root i + S.root j ∈ Set.range ⇑S.root
h_equiv : Weight.toLinear K (↥H) L χ ∈ ↑⟨q, ⋯⟩ ↔ S.root j ∈ ↑⟨q, ⋯⟩
⊢ S.root j ∈ ↑⟨q, ⋯⟩

Tactic:
by rw [hj]; exact hαq

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

Goal state before:
pp: K : Type u_1
V₂ : Type u_4
V₃ : Type u_6
inst✝⁴ : CommRing K
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u u' : V₃ →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h : u.IsLeftQuasiInverse v
hu : u' ≈ u
hv : v' ≈ v
⊢ u'.IsLeftQuasiInverse v'

Tactic:
by
  unfold IsLeftQuasiInverse at *
  grw [hu, hv]
  assumption

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
h₄ : Exact ⇑f₃ ⇑f₄
h₅ : Surjective ⇑f₄
this : FiniteDimensional k ↥(g ∘ₗ f).ker
⊢ (g ∘ₗ f).index = g.index + f.index

Tactic:
have : FiniteDimensional k (P ⧸ (g ∘ₗ f).range) := by rw [range_comp]; infer_instance

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : AddCommGroup N
k : Type u_3
inst✝⁸ : DivisionRing k
inst✝⁷ : Module k M
inst✝⁶ : Module k N
f : M →ₗ[k] N
P : Type u_4
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module k P
g : N →ₗ[k] P
inst✝³ : FiniteDimensional k ↥f.ker
inst✝² : FiniteDimensional k ↥g.ker
inst✝¹ : FiniteDimensional k (N ⧸ f.range)
inst✝ : FiniteDimensional k (P ⧸ g.range)
aux : f.range ≤ comap g (g ∘ₗ f).range
f₀ : ↥f.ker →ₗ[k] ↥(g ∘ₗ f).ker := inclusion ⋯
f₁ : ↥(g ∘ₗ f).ker →ₗ[k] ↥g.ker := f.restrict ⋯
f₂ : ↥g.ker →ₗ[k] N ⧸ f.range := f.range.mkQ ∘ₗ g.ker.subtype
f₃ : N ⧸ f.range →ₗ[k] P ⧸ (g ∘ₗ f).range := f.range.mapQ (g ∘ₗ f).range g aux
f₄ : P ⧸ (g ∘ₗ f).range →ₗ[k] P ⧸ g.range := factor ⋯
h₀ : Injective ⇑f₀
h₁ : Exact ⇑f₀ ⇑f₁
h₂ : Exact ⇑f₁ ⇑f₂
h₃ : Exact ⇑f₂ ⇑f₃
h₄ : Exact ⇑f₃ ⇑f₄
h₅ : Surjective ⇑f₄
this✝ : FiniteDimensional k ↥(g ∘ₗ f).ker
this : FiniteDimensional k (P ⧸ (g ∘ₗ f).range)
⊢ (g ∘ₗ f).index = g.index + f.index
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
P : Ideal B
⊢ P ∈ primesOverFinset p B ↔ P ∈ p.primesOver B

Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset hpb]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : FinitePresentation R M
S : Submonoid R
Mₚ : Type u_1
inst✝⁵ : AddCommGroup Mₚ
inst✝⁴ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝³ : IsLocalizedModule S f
Nₚ : Type u_2
inst✝² : AddCommGroup Nₚ
inst✝¹ : Module R Nₚ
g : N →ₗ[R] Nₚ
inst✝ : IsLocalizedModule S g
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)

Tactic:
obtain ⟨φ, s, hφ⟩ := FinitePresentation.exists_lift_of_isLocalizedModule S g (ϕ ∘ₗ f)

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
inst✝⁶ : FinitePresentation R M
S : Submonoid R
Mₚ : Type u_1
inst✝⁵ : AddCommGroup Mₚ
inst✝⁴ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝³ : IsLocalizedModule S f
Nₚ : Type u_2
inst✝² : AddCommGroup Nₚ
inst✝¹ : Module R Nₚ
g : N →ₗ[R] Nₚ
inst✝ : IsLocalizedModule S g
ϕ : Mₚ →ₗ[R] Nₚ
hϕ : Function.Surjective ⇑ϕ
φ : M →ₗ[R] N
s : ↥S
hφ : g ∘ₗ φ = s • ϕ ∘ₗ f
⊢ ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ s₀ • (↑e.symm ∘ₗ (IsLocalizedModule.map S f g) l) ∘ₗ f = f ∘ₗ (s₀ • LinearMap.id)

Tactic:
change s₀ • (e.symm.toLinearMap ∘ₗ e.toLinearMap) ∘ₗ _ = _

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ (s₀ • LinearMap.id)
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • s₀ • LinearMap.id
⊢ s₀ • (↑e.symm ∘ₗ ↑e) ∘ₗ f = f ∘ₗ (s₀ • LinearMap.id)