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

Goal state before:
pp: 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} := ⋯
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⋯
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L := ⋯
hx₀ : x ≠ 0
Q : Type u_2 := ⋯
r : ℕ := ⋯
hr : r < finrank K L
x' : ↥U := ⋯
y' : ↥U := ⋯
u : ↥U := ⋯
χ : K[X][X] := ⋯
ψ : K[X][X] := ⋯
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α (constantCoeff ψ) ≠ 0
⊢ r - i < s.card

Tactic:
omega

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

Goal state before:
pp: K m n : Type u
inst✝² : CommRing K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
w : m → K
v : n → K
⊢ (toLin' (vecMulVec w v)).rank ≤ 1

Tactic:
nontriviality K
  rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]
  refine le_trans (LinearMap.rank_comp_le_left _ _) ?_
  refine (LinearMap.rank_le_domain _).trans_eq ?_
  rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]

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

Goal state before:
pp: case h
ι : 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)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : (decompose ℒ).symm b ∈ ℒ k
⊢ (lof R ι (fun x ↦ ↥(ℒ x)) k) ⟨(decompose ℒ).symm b, hb⟩ = b

Tactic:
simp [lof_eq_of, ← decompose_of_mem]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
⊢ 0 + χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆

Tactic:
zero_add

Goal state after:
R : Type u_1
L : Type u_2
A : Type u_3
V : Type u_4
inst✝¹⁹ : CommRing R
inst✝¹⁸ : IsPrincipalIdealRing R
inst✝¹⁷ : IsDomain R
inst✝¹⁶ : CharZero R
inst✝¹⁵ : LieRing L
inst✝¹⁴ : LieAlgebra R L
inst✝¹³ : LieRing A
inst✝¹² : LieAlgebra R A
inst✝¹¹ : Bracket L A
inst✝¹⁰ : Bracket A L
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module R V
inst✝⁷ : Module.Free R V
inst✝⁶ : Module.Finite R V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule R L V
inst✝³ : LieRingModule A V
inst✝² : LieModule R A V
inst✝¹ : IsLieTower L A V
inst✝ : IsLieTower A L V
χ : A → R
z : L
v : V
hv : ∀ (x : A), ⁅x, v⁆ = χ x • v
a : A
hv' : v ≠ 0
this : χ ⁅z, a⁆ = 0
⊢ χ a • ⁅z, v⁆ = χ a • ⁅z, v⁆
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ (f.toList x).formPerm y = y

Tactic:
formPerm_apply_of_notMem

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y = y

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
y : α
hy : ¬f.SameCycle x y
⊢ y ∉ f.toList x
Module: Mathlib.Algebra.Lie.Extension

Goal state before:
pp: R : Type u_1
N : Type u_2
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x : L
⊢ E.proj (s₁ x) = E.proj (s₂ x)

Tactic:
hs₁,

Goal state after:
R : Type u_1
N : Type u_2
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
E : Extension R M L
s₁ s₂ : L →ₗ[R] E.L
hs₁ : LeftInverse ⇑E.proj ⇑s₁
hs₂ : LeftInverse ⇑E.proj ⇑s₂
x : L
⊢ x = E.proj (s₂ x)
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
⊢ (Cohomology.d₂₃ R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R)) (twoCochainOfBilinear R A L Φ hΦs) =
    0

Tactic:
ext a x b y c z

Goal state after:
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
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (((TensorProduct.AlgebraTensorModule.curry
                    (((TensorProduct.AlgebraTensorModule.curry
                            ((Cohomology.d₂₃ R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))
                              (twoCochainOfBilinear R A L Φ hΦs)) ∘ₗ
                          AddMonoidAlgebra.lsingle a)
                        1)
                      x) ∘ₗ
                  AddMonoidAlgebra.lsingle b)
                1)
              y) ∘ₗ
          AddMonoidAlgebra.lsingle c)
        1)
      z =
    ((TensorProduct.AlgebraTensorModule.curry
            (((TensorProduct.AlgebraTensorModule.curry
                    (((TensorProduct.AlgebraTensorModule.curry 0 ∘ₗ AddMonoidAlgebra.lsingle a) 1) x) ∘ₗ
                  AddMonoidAlgebra.lsingle b)
                1)
              y) ∘ₗ
          AddMonoidAlgebra.lsingle c)
        1)
      z
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 ⇑χ₀)
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
obtain ⟨z, -, hz⟩ := SetLike.exists_of_lt (hA.lt_top)

Goal state after:
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
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
i j : Fin n
⊢ (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j = (Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j

Tactic:
rw [Matrix.ofArray_eq_of_getD]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
i j : Fin n
⊢ (stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j =
    (Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0))^[t] (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0) i j
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
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = c • e (π₂ x) • v

Tactic:
smul_comm

Goal state after:
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
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝ : i = j
⊢ 2 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ¬(↑i + 1 = ↑j ∨ ↑j + 1 = ↑i)
⊢ 0 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ↑j = n - 1
⊢ -2 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ↑i + 1 = ↑j
h✝ : ¬↑j = n - 1
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ↑j + 1 = ↑i
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬↑i + 1 = ↑j
h✝ : ¬↑j + 1 = ↑i
⊢ 0 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : ↑i + 1 = ↑j
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ↑i = n - 1
⊢ -2 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬↑i + 1 = ↑j
h✝¹ : ↑j + 1 = ↑i
h✝ : ¬↑i = n - 1
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝¹ : ¬i = j
h✝ : n ≤ 2
⊢ 0 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝² : ¬i = j
h✝¹ : ¬n ≤ 2
h✝ : ↑i + 1 = ↑j ∧ ↑j + 2 < n
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝³ : ¬i = j
h✝² : ¬n ≤ 2
h✝¹ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝ : ↑j + 1 = ↑i ∧ ↑i + 2 < n
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁴ : ¬i = j
h✝³ : ¬n ≤ 2
h✝² : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝¹ : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝ : ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n)
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n)
⊢ -1 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
h : i ≠ j
h✝⁵ : ¬i = j
h✝⁴ : ¬n ≤ 2
h✝³ : ¬(↑i + 1 = ↑j ∧ ↑j + 2 < n)
h✝² : ¬(↑j + 1 = ↑i ∧ ↑i + 2 < n)
h✝¹ : ¬(↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n))
h✝ : ¬(↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n))
⊢ 0 ≤ 0

Tactic:
omega

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

Goal state before:
pp: case ha
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
bI : P
hbI : bI ∈ I
bJ : P
hbJ : bJ ∈ J
hb : bI + bJ ∈ I ⊔ J
⊢ IsInteger R (aI • aJ • bI)

Tactic:
smul_comm

Goal state after:
case ha
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ b ∈ J, IsInteger R (aJ • b)
bI : P
hbI : bI ∈ I
bJ : P
hbJ : bJ ∈ J
hb : bI + bJ ∈ I ⊔ J
⊢ IsInteger R (aJ • aI • bI)
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
rw [smul_eq_mul, mem_ofPred, map_mul, ← Algebra.smul_def]

Goal state after:
case mp.refine_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
J : FractionalIdeal S P
hJ : J ≤ 1
c x : R
hx : x ∈ { carrier := {x | (algebraMap R P) x ∈ J}, add_mem' := ⋯, zero_mem' := ⋯ }.carrier
⊢ c • (algebraMap R P) x ∈ J
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ (x / x) = 1

Tactic:
div_self hx,

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : K
hx : x ≠ 0
⊢ spanSingleton R₁⁰ 1 = 1
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁵ : Field K
R₁ : Type u_4
inst✝⁴ : CommRing R₁
inst✝³ : IsDomain R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
⊢ I * I⁻¹ = 1 ↔ generator ↑I ≠ 0

Tactic:
by
  constructor
  · intro hI hg
    apply ne_zero_of_mul_eq_one _ _ hI
    rw [eq_spanSingleton_of_principal I, hg, spanSingleton_zero]
  · intro hg
    apply invertible_of_principal
    rw [eq_spanSingleton_of_principal I]
    intro hI
    have := mem_spanSingleton_self R₁⁰ (generator (I : Submodule R₁ K))
    rw [hI, mem_zero_iff] at this
    contradiction

Goal state after:
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
s✝ : Set P
x✝² : ∃ a ∈ S, ∀ b ∈ s✝, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s✝, IsInteger R (a • b)
x✝¹ : P
hb : x✝¹ ∈ span R s✝
s : R
x : P
x✝ : x ∈ span R s✝
hx : IsInteger R (a • x)
⊢ IsInteger R (a • s • x)

Tactic:
smul_comm

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
s✝ : Set P
x✝² : ∃ a ∈ S, ∀ b ∈ s✝, IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ b ∈ s✝, IsInteger R (a • b)
x✝¹ : P
hb : x✝¹ ∈ span R s✝
s : R
x : P
x✝ : x ∈ span R s✝
hx : IsInteger R (a • x)
⊢ IsInteger R (s • a • x)
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
inst✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ IsFractional S (span R ↑I)

Tactic:
rw [isFractional_span_iff]

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✝ : IsLocalization S P
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)
⊢ ∃ a ∈ S, ∀ b ∈ ↑I, IsInteger R (a • b)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case neg
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹
p : A[X]
hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range
⊢ (Polynomial.aeval x) p ∈ ↑(↑I)⁻¹

Tactic:
Polynomial.aeval_eq_sum_range

Goal state after:
case neg
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hJ0 : ¬↑I * (↑I)⁻¹ = 0
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹
p : A[X]
hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range
⊢ ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i ∈ ↑(↑I)⁻¹
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x✝ : K
hx✝¹ : x✝ ∈ span R₁ (f '' ↑s)
c : R₁
x : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
⊢ IsInteger R₁ (↑a' • c • x)

Tactic:
smul_comm

Goal state after:
case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x✝ : K
hx✝¹ : x✝ ∈ span R₁ (f '' ↑s)
c : R₁
x : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
⊢ IsInteger R₁ (c • ↑a' • x)
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
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J

Tactic:
by
        have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)
        rw [Ideal.dvd_iff_le, Ideal.dvd_iff_le, Ideal.dvd_iff_le, SetLike.le_def, SetLike.le_def,
          SetLike.le_def]
        contrapose!
        rintro ⟨⟨x, x_mem, x_notMem⟩, ⟨y, y_mem, y_notMem⟩⟩
        exact
          ⟨x * y, Ideal.mul_mem_mul x_mem y_mem,
            mt this.isPrime.mem_or_mem (not_or_intro x_notMem y_notMem)⟩

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

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ιM), ↥(𝓜 i)

Tactic:
refine ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩,
    (DirectSum.decomposeAddEquiv 𝓜).symm.toFun, (DirectSum.decomposeAddEquiv 𝓜).left_inv,
    (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
⊢ ∀ (m : A) (x : M),
    (decomposeAddEquiv 𝓜).toAddHom.toFun (m • x) = (RingHom.id A) m • (decomposeAddEquiv 𝓜).toAddHom.toFun x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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
⊢ ∀ {a b c : Ideal A}, c ≤ a → b ≤ a → c ⊔ b ≤ a

Tactic:
exact fun h1 h2 => @sup_le (Ideal A) _ _ _ _ h1 h2

Goal state after:
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
inst✝ : IsNoetherianRing R
s : Set (Submodule R M)
hs : s.Finite
hcofg : ∀ S ∈ ↑hs.toFinset, S.CoFG
⊢ (sInf ↑hs.toFinset).CoFG

Tactic:
exact CoFG.sInf hcofg

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

Goal state before:
pp: case neg
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:
have : I.IsMaximal := hI.isMaximal hI0

Goal state after:
case neg
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 = ⊥
this : I.IsMaximal
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)

Tactic:
have hJ' : Irreducible (Associates.mk J) := by
    simpa only [Associates.irreducible_mk] using (prime_of_isPrime hJ₀ hJ).irreducible

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : x * x ∣ a
⊢ IsUnit x

Tactic:
← span_singleton_dvd_span_singleton_iff_dvd,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x * x} ∣ span {a}
⊢ IsUnit x