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

Goal state before:
pp: ⊢ D 2 = !![2, 0; 0, 2]

Tactic:
by decide

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

Goal state before:
pp: ⊢ B 2 = !![2, -2; -1, 2]

Tactic:
by decide

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

Goal state before:
pp: ⊢ C 2 = !![2, -1; -2, 2]

Tactic:
by decide

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

Goal state before:
pp: ⊢ D 3 = !![2, -1, -1; -1, 2, 0; -1, 0, 2]

Tactic:
by decide

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

Goal state before:
pp: ⊢ (reindex ((↑[0, 1]).formPerm ⋯) ((↑[0, 1]).formPerm ⋯)) (D 3) = A 3

Tactic:
by decide

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

Goal state before:
pp: ⊢ D 4 = !![2, -1, 0, 0; -1, 2, -1, -1; 0, -1, 2, 0; 0, -1, 0, 2]

Tactic:
by decide

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun n ↦ q ^ n) → q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
h : E.IsSolution fun n ↦ q ^ n
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
⊢ q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n ↦ q ^ n

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x, E.coeffs x * q ^ ↑x = 0
⊢ E.IsSolution fun n ↦ q ^ n
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
by
  rcases n with - | n; · contradiction
  refine (Associates.isAtom_iff (ne_zero_of_dvd_ne_zero hq (h₂.2 ⟨1, rfl⟩))).mp ⟨?_, fun b hb => ?_⟩
  · exact ne_bot_of_gt (h₁ zero_lt_one)
  obtain ⟨⟨i, hi⟩, rfl⟩ := h₂.1 (hb.le.trans (h₂.2 ⟨1, rfl⟩))
  cases i
  · exact (Associates.isUnit_iff_eq_one _).mp (first_of_chain_isUnit h₁ @h₂)
  · simpa [Fin.lt_def] using h₁.lt_iff_lt.mp hb

Goal state after:
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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ α ∈ LieSubalgebra.root

Tactic:
by simpa [LieSubalgebra.root] using hα

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hq : q ≠ 0
i : Fin (n + 1)
hi' : q = c 1 ^ ↑i
j : Fin (n + 1)
hr : c j ∈ Finset.image c Finset.univ
this : c j ≤ c 1 ^ ↑i
⊢ Prime (c 1)

Tactic:
rw [← irreducible_iff_prime]
      exact second_of_chain_is_irreducible hn h₁ (@h₂) hq

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

Goal state before:
pp: ⊢ E₆ᵀ = E₆

Tactic:
by decide

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

Goal state before:
pp: ⊢ E₇ᵀ = E₇

Tactic:
by decide

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

Goal state before:
pp: ⊢ E₈ᵀ = E₈

Tactic:
by decide

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

Goal state before:
pp: ⊢ G₂.det = 1

Tactic:
by decide

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

Goal state before:
pp: ⊢ F₄.det = 1

Tactic:
by decide

Goal state after:
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
x : L
hxI : x ∈ ↑↑(LieSubmodule.restr I H)
hxH : x ∈ ↑↑H.toLieSubmodule
f : ↥LieSubalgebra.root → LieIdeal K ↥H := fun α ↦ corootSpace ⇑↑α
span_I_roots : LieIdeal K ↥H := ⨆ α ∈ I.rootSet, f α
span_compl_roots : LieIdeal K ↥H := ⨆ β, ⨆ (_ : β ∉ I.rootSet), f β
h_split : span_I_roots ⊔ span_compl_roots = ⨆ α, f α
h_top : span_I_roots ⊔ span_compl_roots = ⊤
hspan_I_roots_incl : LieSubmodule.map H.toLieSubmodule.incl span_I_roots = ⨆ α ∈ I.rootSet, corootSubmodule ↑α
hspan_compl_roots_vanish : ∀ μ ∈ I.rootSet, ↑span_compl_roots ≤ Weight.ker
hx_top : ⟨x, hxH⟩ ∈ span_I_roots ⊔ span_compl_roots
a : ↥H
ha : a ∈ ↑span_I_roots
b : ↥H
hb : b ∈ ↑span_compl_roots
hab : a + b = ⟨x, hxH⟩
haI : ↑a ∈ I
hbI : ↑b ∈ I
this : b ∈ ⨅ α, Weight.ker
⊢ b = 0

Tactic:
by simpa [iInf_ker_weight_eq_bot] using this

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

Goal state after:
case mp
ι : Type u_1
inst✝ : LinearOrder ι
A : Matrix ι ι ℤ
hA : A.IsSymm
h : A.IsSimplyLaced
⊢ ∀ ⦃i j : ι⦄, 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

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
⊢ A.IsSimplyLaced
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ (Pairwise fun i j ↦ Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ Pairwise fun i j ↦ A i j = 0 ∨ A i j = -1

Tactic:
Pairwise,

Goal state after:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ ⦃i j : ι⦄, i ≠ j → Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ Pairwise fun i j ↦ A i j = 0 ∨ A i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ ⦃i j : ι⦄, i ≠ j → Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ Pairwise fun i j ↦ A i j = 0 ∨ A i j = -1

Tactic:
Pairwise,

Goal state after:
ι : Type u_1
A : Matrix ι ι ℤ
⊢ (∀ ⦃i j : ι⦄, i ≠ j → Aᵀ i j = 0 ∨ Aᵀ i j = -1) ↔ ∀ ⦃i j : ι⦄, i ≠ j → A i j = 0 ∨ A i j = -1
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: ⊢ ¬F₄.IsSimplyLaced

Tactic:
by decide

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

Goal state before:
pp: ⊢ ¬G₂.IsSimplyLaced

Tactic:
by decide

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

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ 1 ∈ (↑I)⁻¹

Tactic:
rw [mem_inv_iff (coeIdeal_ne_zero.mpr hI)]

Goal state after:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
I : Ideal A
hI : I ≠ ⊥
⊢ ∀ y ∈ ↑I, 1 * y ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_2
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
hNF : ¬IsField A
I : Ideal A
hI0 : I ≠ ⊥
Z₀ : Multiset (PrimeSpectrum A)
hZ₀ : (Multiset.map asIdeal Z₀).prod ≤ I ∧ (Multiset.map asIdeal Z₀).prod ≠ ⊥
Z : Multiset (PrimeSpectrum A)
h_eraseZ : ∀ x ∈ {Z | (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥}, ¬x < Z
hZI : (Multiset.map asIdeal Z).prod ≤ I
hprodZ : (Multiset.map asIdeal Z).prod ≠ ⊥
P : PrimeSpectrum A
hPZ : P ∈ Z
hPZ' : P.asIdeal ∈ Multiset.map asIdeal Z
this : Multiset.map asIdeal (Z.erase P) = (Multiset.map asIdeal Z).erase P.asIdeal
hP0 : P.asIdeal ≠ ⊥
hZP0 : (Multiset.map asIdeal (Z.erase P)).prod ≠ ⊥
hIM : I ≤ P.asIdeal
hM : P.asIdeal.IsMaximal
hPM : P.asIdeal ≤ P.asIdeal
⊢ ¬(Multiset.map asIdeal (Z.erase P)).prod ≤ I

Tactic:
· refine fun h => h_eraseZ (Z.erase P) ⟨h, ?_⟩ (Multiset.erase_lt.mpr hPZ)
      exact hZP0

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

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J

Tactic:
by
  rw [div_of_ne_zero hJ', ← coe_le_coe (I := I * J') (J := J), coe_mul]
  exact Submodule.le_div_iff_mul_le

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

Goal state before:
pp: case mp
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ ⟨↑I / ↑1, ⋯⟩ → x✝ ∈ I

Tactic:
intro h

Goal state after:
case mp
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ ⟨↑I / ↑1, ⋯⟩
⊢ x✝ ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
⊢ x✝ ∈ I → x✝ ∈ ⟨↑I / ↑1, ⋯⟩

Tactic:
intro h

Goal state after:
case mpr
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
x✝ : K
h : x✝ ∈ I
⊢ x✝ ∈ ⟨↑I / ↑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
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
y : P'
⊢ y ∈ (canonicalEquiv S P P') (spanSingleton S x) → y ∈ spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

Tactic:
intro h

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

Tactic:
intro h

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 ∈ (canonicalEquiv S P P') (spanSingleton S x)
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 y : P
I : FractionalIdeal S P
⊢ y ∈ spanSingleton S x * I → ∃ y' ∈ I, y = x * y'

Tactic:
intro h

Goal state after:
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 y : P
I : FractionalIdeal S P
h : y ∈ spanSingleton S x * I
⊢ ∃ y' ∈ I, y = x * y'
Module: Mathlib.LinearAlgebra.LeftExact

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst✝⁷ : AddCommGroup M1
inst✝⁶ : AddCommGroup M2
inst✝⁵ : AddCommGroup M3
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M1
inst✝² : Module R M2
inst✝¹ : Module R M3
inst✝ : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact ⇑f ⇑g
surj : Function.Surjective ⇑g
⊢ Function.Exact ⇑(lcomp R N g) ⇑(lcomp R N f)

Tactic:
intro h

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M1 : Type u_2
M2 : Type u_3
M3 : Type u_4
N : Type u_5
inst✝⁷ : AddCommGroup M1
inst✝⁶ : AddCommGroup M2
inst✝⁵ : AddCommGroup M3
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M1
inst✝² : Module R M2
inst✝¹ : Module R M3
inst✝ : Module R N
f : M1 →ₗ[R] M2
g : M2 →ₗ[R] M3
exac : Function.Exact ⇑f ⇑g
surj : Function.Surjective ⇑g
h : M2 →ₗ[R] N
⊢ (lcomp R N f) h = 0 ↔ h ∈ Set.range ⇑(lcomp R N g)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P ∈ p.primesOver A ↔ P ∈ normalizedFactors (map (algebraMap R A) p)

Tactic:
rw [primesOver, Set.mem_ofPred_eq, mem_normalizedFactors_iff (map_ne_bot_of_ne_bot hp),
    liesOver_iff, under_def, and_congr_right_iff, map_le_iff_le_comap]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P)
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

Goal state after:
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
h : ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J
⊢ ∀ z ∈ I, x * z ∈ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)

Tactic:
have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
    obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
    exact prime_span_singleton_iff.mpr <| prime_of_factor r hr

Goal state after:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q ↦ span {q}) (factors p), Prime q
⊢ factors (span {p}) = Multiset.map (fun q ↦ span {q}) (factors p)
Module: Mathlib.RingTheory.Finiteness.Cofinite

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ T.CoFG

Tactic:
← sup_eq_right.mpr hT

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ (S ⊔ T).CoFG
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:
unfold IsLeftQuasiInverse at *
  grw [hu, hv]
  assumption

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

Goal state before:
pp: T : Type u_4
inst✝³ : CommRing T
inst✝² : IsDedekindDomain T
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : Prime I
h : I ≠ ⊥
⊢ Prime (map f I)

Tactic:
rw [prime_iff_isPrime h] at hI
  exact (prime_iff_isPrime <| (I.map_eq_bot_iff_of_injective f.injective).not.2 h).2
    (map_isPrime_of_equiv _)

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
simpa [pow_succ, hI0] using h

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
⊢ ⊤.FG

Tactic:
apply Submodule.fg_of_fg_map_of_fg_inf_ker l

Goal state after:
case hs1
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
⊢ (Submodule.map l ⊤).FG

case hs2
R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
⊢ (⊤ ⊓ l.ker).FG
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t

Tactic:
intro h

Goal state after:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
⊢ s ⊆ t
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
⊢ ∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p

Tactic:
intro p q

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
H : ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)
hC : ∀ (r : R), D (C r) = 0
this : ∀ (p : MvPolynomial σ R) (i : σ), D (p * X i) = p • D (X i) + X i • D p
p q : MvPolynomial σ R
⊢ D (p * q) = p • D q + q • D p
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ finZeroElim i)

Tactic:
rw [Set.range_eq_empty, Submodule.span_empty] at hs

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : ⊥ = ⊤
⊢ Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ finZeroElim i)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ R ∙ s j = (↑f ∘ₗ (R ∙ s j).mkQ).ker

Tactic:
LinearEquiv.ker_comp,

Goal state after:
case h.succ.refine_3.refine_2.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ R ∙ s j = (R ∙ s j).mkQ.ker
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
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_neg : x_χ ∈ genWeightSpace L ⇑(-Weight.toLinear K (↥H) L α)
c : K
hc : c • ⟨f, hf⟩ = ⟨x_χ, hx_χ_neg⟩
⊢ x_χ = 0 • e + c • f + 0 • ⁅e, f⁆

Tactic:
simpa using hc.symm

Goal state after: