mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: 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 • -(Φ z) ⁅x, y⁆ = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x

Tactic:
hΦs.eq z ⁅x, y⁆,

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 • -(Φ ⁅x, y⁆) z = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
obtain ⟨⟨s, hn⟩, hs, hs'⟩ := hf.existsUnique_cycle_subtype
  refine ⟨⟨s, hn, ?_⟩, ?_, ?_⟩
  · rw [hn.nontrivial_iff]
    subst f
    intro H
    refine hf.ne_one ?_
    simpa using Cycle.formPerm_subsingleton _ H
  · simpa using hs
  · rintro ⟨t, ht, ht'⟩ ht''
    simpa using hs' ⟨t, ht⟩ ht''

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

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
⊢ z ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑(x + y), ↑z⁆, ⋯⟩ = ⟨⁅↑x, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑z⁆, ⋯⟩

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑(y + z)⁆, ⋯⟩ = ⟨⁅↑x, ↑y⁆, ⋯⟩ + ⟨⁅↑x, ↑z⁆, ⋯⟩

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x : ↥L'
⊢ ⟨⁅↑x, ↑x⁆, ⋯⟩ = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝² : CommRing A
inst✝¹ : LieRing L
inst✝ : Module A L
L' : LieRinehartSubalgebra A L
x y z : ↥L'
⊢ ⟨⁅↑x, ↑⟨⁅↑y, ↑z⁆, ⋯⟩⁆, ⋯⟩ = ⟨⁅↑⟨⁅↑x, ↑y⁆, ⋯⟩, ↑z⁆, ⋯⟩ + ⟨⁅↑y, ↑⟨⁅↑x, ↑z⁆, ⋯⟩⁆, ⋯⟩

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

Goal state before:
pp: A : Type u_1
L : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : LieRing L
inst✝⁶ : Module A L
L' : LieRinehartSubalgebra A L
inst✝⁵ : LieRingModule L A
inst✝⁴ : LieRinehartRing A L
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R A
inst✝¹ : LieAlgebra R L
inst✝ : LieRinehartAlgebra R A L
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ B n i i = 2

Tactic:
simp [B, Matrix.of_apply]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ 1 - (∑ i, (monomial ↑i) (E.coeffs i)).coeff E.order = 1

Tactic:
finsetSum_coeff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
a✝ : Nontrivial R
⊢ 1 - ∑ b, ((monomial ↑b) (E.coeffs b)).coeff E.order = 1
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : Associates M
n : ℕ
hn : n ≠ 0
hp : Prime p
⊢ (fun i ↦ p ^ ↑i) 1 = p

Tactic:
dsimp only
    rw [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt, pow_one]
    exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)

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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
⊢ ↑α (coroot ↑β) = 0

Tactic:
have h_ker : coroot (α : Weight K H L) ∈ (β : Weight K H L).ker :=
    I.root_apply_eq_zero_of_notMem_rootSet
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule _)) hβ

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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
h_ker : coroot ↑α ∈ Weight.ker
⊢ ↑α (coroot ↑β) = 0
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
α : ↥LieSubalgebra.root
hα : α ∈ I.rootSet
β : ↥LieSubalgebra.root
hβ : β ∉ I.rootSet
⊢ ↑α (coroot ↑β) = 0

Tactic:
have h_ker : coroot (α : Weight K H L) ∈ (β : Weight K H L).ker :=
    I.root_apply_eq_zero_of_notMem_rootSet
      (I.corootSubmodule_le hα (coe_coroot_mem_corootSubmodule _)) hβ
  change coroot (β : Weight K H L) ∈ (α : Weight K H L).ker
  rw [← orthogonal_span_coroot_eq_ker,
    LinearMap.BilinForm.orthogonal_span_singleton_eq_toLin_ker, LinearMap.mem_ker]
  exact traceForm_eq_zero_of_mem_ker_of_mem_span_coroot h_ker (Submodule.mem_span_singleton_self _)

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case neg.refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ d ⟨c₁ t, ⋯⟩ < d ⟨c₁ u, ⋯⟩

Tactic:
d.lt_iff_lt,

Goal state after:
case neg.refine_1
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m : Associates M
n : Associates N
hn : n ≠ 0
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
s : ℕ
hs : ¬s = 0
c₁ : Fin (s + 1) → Associates M
hp : c₁ 1 ∈ normalizedFactors m
hs' : c₁ 1 ^ s ≤ m
hc₁' : StrictMono c₁
hc₁'' : ∀ {r : Associates M}, r ≤ c₁ 1 ^ s ↔ ∃ i, r = c₁ i
c₂ : Fin (s + 1) → Associates N := fun t ↦ ↑(d ⟨c₁ t, ⋯⟩)
c₂_def : ∀ (t : Fin (s + 1)), c₂ t = ↑(d ⟨c₁ t, ⋯⟩)
t u : Fin (s + 1)
h : t < u
⊢ ⟨c₁ t, ⋯⟩ < ⟨c₁ u, ⋯⟩
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
⊢ ↑(Nat.unaryCast 0) = ↑0

Tactic:
simp [*, Nat.unaryCast]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
n✝ : ℕ
a✝ : ↑n✝.unaryCast = ↑n✝
⊢ ↑(n✝ + 1).unaryCast = ↑(n✝ + 1)

Tactic:
simp [*, Nat.unaryCast]

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
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = 1

Tactic:
convert! congr_arg (· * I⁻¹) mul_self

Goal state after:
case e'_2
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
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ I = I * I * I⁻¹

case e'_3
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
x : K
hx : IsIntegral A x
I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx
hI : IsUnit I
mul_self : IsIdempotentElem I
⊢ 1 = I * I⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Operations

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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
⊢ (canonicalEquiv S P P') ((canonicalEquiv S P' P) I) = I

Tactic:
by
  rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]

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

Goal state before:
pp: case refine_1
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
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ x ∈ I →
    ∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y'

pp: case refine_2
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
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ (∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y') →
    x ∈ I

Tactic:
· intro hx
    obtain ⟨x', hx'⟩ := ha x hx
    rw [Algebra.smul_def] at hx'
    refine ⟨algebraMap R₁ K x', (mem_coeIdeal _).mpr ⟨x', mem_singleton_mul.mpr ?_, rfl⟩, ?_⟩
    · exact ⟨x, hx, hx'⟩
    · rw [hx', ← mul_assoc, inv_mul_cancel₀ map_a_nonzero, one_mul]

Goal state after:
case refine_2
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
a_inv : R₁
nonzero✝ : a_inv ∈ R₁⁰
ha : ∀ b ∈ ↑I, IsInteger R₁ (a_inv • b)
nonzero : a_inv ≠ 0
map_a_nonzero : (algebraMap R₁ K) a_inv ≠ 0
x : K
⊢ (∃ y' ∈ ↑(comap (Algebra.linearMap R₁ K) ↑(spanSingleton R₁⁰ ((algebraMap R₁ K) a_inv) * I)),
      x = ((algebraMap R₁ K) a_inv)⁻¹ * y') →
    x ∈ I
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
x : K
hx : x ∈ I
⊢ IsInteger S (f r • ↑(semilinearEquivOfRingEquiv K L f) x)

Tactic:
specialize hr x hx

Goal state after:
case h
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
x : K
hr : IsInteger R (r • x)
hx : x ∈ I
⊢ IsInteger S (f r • ↑(semilinearEquivOfRingEquiv K L f) x)
Module: Mathlib.Algebra.Module.GradedModule

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ (of M (0 +ᵥ i)) (GSMul.smul GOne.one xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)

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
⊢ I ⊔ J = ⊤ ↔ gcd I J = ⊤

Tactic:
gcd_eq_sup

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
⊢ 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
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:
by
  rw [IsLattice.rank' K M]
  simp

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

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u : V →ₗ[K] V₂
h : u.HasFiniteRange
⊢ u.HasNoetherianRange

Tactic:
by
  rw [HasNoetherianRange]
  have := Finite.of_fg h.fg_range
  infer_instance

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
⊢ (-f).index = f.index

Tactic:
by
  rw [index_eq_finrank_sub, index_eq_finrank_sub, ker_neg, range_neg]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ Function.onFun IsCoprime (fun i ↦ f i ^ e i) i j

Tactic:
exact Ideal.isCoprime_iff_sup_eq.mpr (pow_sup_pow_eq_top (IsMaximal.coprime_of_ne
    (IsPrime.isMaximal (isPrime_of_prime (prime i hi)) (prime i hi).ne_zero)
    (IsPrime.isMaximal (isPrime_of_prime (prime j hj)) (prime j hj).ne_zero)
    (coprime i hi j hj hij)))

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

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ (span {a}).IsPrime

Tactic:
exact (span_singleton_prime (prime_of_normalized_factor a ha).ne_zero).mpr
        (prime_of_normalized_factor a ha)

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
⊢ Function.Bijective fun d ↦ ⟨span {↑d}, ⋯⟩

Tactic:
· refine ⟨?_, ?_⟩
    · rintro ⟨a, ha⟩ ⟨b, hb⟩ h
      rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton, Subtype.coe_mk,
          Subtype.coe_mk] at h
      exact Subtype.mk_eq_mk.mpr (mem_normalizedFactors_eq_of_associated ha hb h)
    · rintro ⟨i, hi⟩
      have : i.IsPrime := isPrime_of_prime (prime_of_normalized_factor i hi)
      have := exists_mem_normalizedFactors_of_dvd hr
        (Submodule.IsPrincipal.prime_generator_of_isPrime i
        (prime_of_normalized_factor i hi).ne_zero).irreducible ?_
      · obtain ⟨a, ha, ha'⟩ := this
        use ⟨a, ha⟩
        simp only [← span_singleton_eq_span_singleton.mpr ha',
            span_singleton_generator]
      · exact (Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
          ((show span {r} ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
            (mem_span_singleton.mpr (dvd_refl r)))

Goal state after:
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✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
this : IsDomain R
f : HeightOneSpectrum A → HeightOneSpectrum R := fun p ↦ HeightOneSpectrum.under R p
x✝ : HeightOneSpectrum R
P : Ideal A
hP : P.IsPrime
isPrime✝ : (Ideal.comap (algebraMap R A) P).IsPrime
hp : Ideal.comap (algebraMap R A) P ≠ ⊥
⊢ P ≠ ⊥

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ (pres₂.cokernelSolution data).postcomp
      (f.range.liftQ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }) ⋯) =
    s

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
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
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
apply LieSubmodule.mem_iSup_of_mem ⟨α, hαq, hα₀⟩
    have hx_χ_in_sl2 : x_χ ∈ sl2SubalgebraOfRoot hα₀ := by
      obtain ⟨h, e, f, ht, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα₀
      rw [mem_sl2SubalgebraOfRoot_iff hα₀ ht he hf]
      have hx_χ_neg : x_χ ∈ genWeightSpace L (-α.toLinear) := by
        rw [← (add_eq_zero_iff_eq_neg.mp w_plus)]
        exact hx_χ
      obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simp [ht.f_ne_zero])).mp
        (finrank_rootSpace_eq_one (-α) (by simpa using hα₀)) ⟨x_χ, hx_χ_neg⟩
      exact ⟨0, c, 0, by simpa using hc.symm⟩
    apply LieSubalgebra.lie_mem <;> [exact hx_χ_in_sl2; exact hm_α_original]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
← P.span_range_relation_eq_ker,

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : e.symm x ∈ Ideal.map TensorProduct.includeRight (Ideal.span (Set.range P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ LieSubmodule.restr J H = LieSubmodule.restr I H

Tactic:
J.restr_eq_iSup_sl2SubmoduleOfRoot,

Goal state after:
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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ ⨆ α ∈ J.rootSet, sl2SubmoduleOfRoot ⋯ = LieSubmodule.restr I H
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case e_g
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m
      (C (eval₂ (algebraMap R S) P.val (P.σ s)) *
        (Finsupp.mapDomain Sum.inl u).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k) =
    coeff m (C s * u.prod fun n e ↦ X n ^ e)

Tactic:
← aeval_def

Goal state after:
case e_g
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
r : σ'
u : ι' →₀ ℕ
s : S
m : ι' →₀ ℕ
⊢ coeff m (C ((aeval P.val) (P.σ s)) * (Finsupp.mapDomain Sum.inl u).prod fun i k ↦ Sum.elim X (⇑C ∘ P.val) i ^ k) =
    coeff m (C s * u.prod fun n e ↦ X n ^ e)