mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ (φ.polyCharpoly (chooseBasis R L)).coeff (Fintype.card ι) ≠ 0

Tactic:
rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
    Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Lie.SkewAdjoint

Goal state before:
pp: R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : Fintype n
J : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : Invertible P
A : Matrix n n R
this : (P.lieConj h) A ∈ skewAdjointMatricesSubmodule J ↔ A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P)
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    A ∈ skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)

Tactic:
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
      exact this

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

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ finrank R (n → R) = Fintype.card n

Tactic:
finrank_pi

Goal state after:
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ Fintype.card n = Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: l : Type ul
m : Type um
n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : Field R
inst✝¹ : Finite l
inst✝ : Fintype m
A : Matrix l m R
B : Matrix m n R
hAB : A * B = 0
⊢ A.rank + B.rank ≤ Fintype.card m

Tactic:
let el : Basis l R (l → R) := Pi.basisFun R l
  let em : Basis m R (m → R) := Pi.basisFun R m
  let en : Basis n R (n → R) := Pi.basisFun R n
  rw [Matrix.rank_eq_finrank_range_toLin A el em,
      Matrix.rank_eq_finrank_range_toLin B em en,
      ← Module.finrank_fintype_fun_eq_card R,
      ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
      add_le_add_iff_left]
  apply Submodule.finrank_mono
  rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ -(a ⁅x, y⁆) z + -(a y) ⁅x, z⁆ - -(a x) ⁅y, z⁆ = 0

Tactic:
h x y z

Goal state after:
case mpr
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_2
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
a : ↥(twoCochain R L M)
h : ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
x y z : L
⊢ -(a ⁅x, y⁆) z + -(a y) ⁅x, z⁆ - -((a ⁅x, y⁆) z + (a y) ⁅x, z⁆) = 0
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inr
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
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
⊢ χ ⁅z, a⁆ = 0

Tactic:
have T_apply_succ (w : A) (n : ℕ) :
      Submodule.map (T χ w) (U' (n + 1)) ≤ U' n := by
    simp only [OrderHom.coe_mk, U', Submodule.map_span, Submodule.span_le, Set.image_subset_iff]
    simp only [Set.subset_def, Set.mem_ofPred_eq, Set.mem_preimage, SetLike.mem_coe,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    induction n generalizing w
    · simp only [zero_add, Nat.lt_one_iff, LinearMap.sub_apply, LieModule.toEnd_apply_apply,
        LinearMap.smul_apply, Module.End.one_apply, forall_eq, pow_zero, hv w, sub_self, zero_mem]
    · next n hn =>
      intro m hm
      obtain (hm | rfl) : m < n + 1 ∨ m = n + 1 := by lia
      · exact U'.mono (Nat.le_succ n) (hn w m hm)
      have H : ∀ w, ⁅w, (π z ^ n) v⁆ = (T χ w) ((π z ^ n) v) + χ w • ((π z ^ n) v) := by simp
      rw [T, LinearMap.sub_apply, pow_succ', Module.End.mul_apply, LieModule.toEnd_apply_apply,
        LieModule.toEnd_apply_apply, LinearMap.smul_apply, Module.End.one_apply, leibniz_lie,
        lie_swap_lie w z, H, H, lie_add, lie_smul, add_sub_assoc, add_sub_assoc, sub_self, add_zero]
      refine add_mem (neg_mem <| add_mem ?_ ?_) ?_
      · exact U'.mono n.le_succ (hn _ n n.lt_succ_self)
      · exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨n, n.lt_succ_self, rfl⟩)
      · exact map_U'_le _ <| Submodule.mem_map_of_mem <| hn w n n.lt_succ_self

Goal state after:
case inr
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
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
⊢ χ ⁅z, a⁆ = 0
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
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
w : A
x : V
U : Submodule R V := ⨆ k, U' k
hx : x ∈ U.carrier
⊢ Submodule.map (T χ w) U ≤ U

Tactic:
Submodule.map_iSup,

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
U' : ℕ →o Submodule R V :=
  { toFun := fun n ↦ Submodule.span R {x | ∃ i < n, ((toEnd R L V) z ^ i) v = x}, monotone' := ⋯ }
map_U'_le : ∀ (n : ℕ), Submodule.map ((toEnd R L V) z) (U' n) ≤ U' (n + 1)
T_apply_succ : ∀ (w : A) (n : ℕ), Submodule.map (T χ w) (U' (n + 1)) ≤ U' n
w : A
x : V
U : Submodule R V := ⨆ k, U' k
hx : x ∈ U.carrier
⊢ ⨆ i, Submodule.map (T χ w) (U' i) ≤ U
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
inst✝ : IsLieAbelian M
E : Extension R M L
x y : L
m : M
h : HasRightInverse ⇑E.proj := Surjective.hasRightInverse (proj_surjective E)
aux : ∀ (z : ↥E.proj.ker), ⁅⁅Exists.choose h x, Exists.choose h y⁆, z⁆ = ⁅Exists.choose h ⁅x, y⁆, z⁆
⊢ E.toKer.symm ⁅Exists.choose h x, E.toKer (E.toKer.symm ⁅Exists.choose h y, E.toKer m⁆)⁆ =
    E.toKer.symm ⁅Exists.choose h ⁅x, y⁆, E.toKer m⁆ +
      E.toKer.symm ⁅Exists.choose h y, E.toKer (E.toKer.symm ⁅Exists.choose h x, E.toKer m⁆)⁆

Tactic:
rw [← map_add, EquivLike.apply_eq_iff_eq, LieEquiv.apply_symm_apply, LieEquiv.apply_symm_apply,
      leibniz_lie, aux]

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

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

Tactic:
simp only [d₁₂_apply_coe_apply_apply, oneCochainOfTwoSplitting_apply, AddSubgroupClass.coe_sub,
    twoCocycleOf_coe_coe, LinearMap.sub_apply, LinearMap.compr₂_apply, LinearMap.coe_mk,
    AddHom.coe_mk, LinearEquiv.coe_coe, LieEquiv.coe_toLinearEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
⊢ birdDet A = (-1) ^ k * (stepEntry A)^[k] A 0 0

Tactic:
by
  rw [birdDet]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n lo : ℕ
f : ℕ → R
⊢ BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
by
  induction lo using BirdDet.sumFrom_induct n with
  | step lo hlo ih => rw [sumFrom_step n lo f hlo, ih, ← Finset.sum_eq_sum_Ico_succ_bot hlo f]
  | stop lo hlo => rw [sumFrom_stop n lo f hlo, Finset.Ico_eq_empty hlo, Finset.sum_empty]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
ih :
  ∀ (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
i j : Fin n
⊢ stepEntry n A ((stepEntry n A)^[t] (BirdDet.get n A)) ↑i ↑j =
    Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0)
      ((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

Tactic:
stepEntry_eq,

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Array R
hA : A.size = n * n
t : ℕ
ih :
  ∀ (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
i j : Fin n
⊢ ((-BirdDet.sumFrom n (↑i + 1) fun k ↦ (stepEntry n A)^[t] (BirdDet.get n A) k k) * BirdDet.get n A ↑i ↑j +
      BirdDet.sumFrom n (↑i + 1) fun k ↦ (stepEntry n A)^[t] (BirdDet.get n A) (↑i) k * BirdDet.get n A k ↑j) =
    Spec.stepEntry (Matrix.of fun i j ↦ A.getD (n * ↑i + ↑j) 0)
      ((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.Module.Bimodule

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
a : A
m : M
hm : m ∈ p
⊢ a • m ∈ p

Tactic:
by
  suffices a • m = a ⊗ₜ[R] (1 : B) • m by exact this.symm ▸ p.smul_mem _ hm
  simp [TensorProduct.Algebra.smul_def]

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
E : LinearRecurrence R
inst✝ : Nontrivial R
⊢ E.charPoly.degree = ↑E.order

Tactic:
by
  rw [charPoly, degree_sub_eq_left_of_degree_lt]
    <;> rw [degree_monomial E.order one_ne_zero]
  simp_rw [← C_mul_X_pow_eq_monomial]
  exact degree_sum_fin_lt E.coeffs

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
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:
obtain ⟨⟨i, hi⟩, rfl⟩ := h₂.1 (hb.le.trans (h₂.2 ⟨1, rfl⟩))

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
i : ℕ
hi : i < n + 1 + 1
hb : c ⟨i, hi⟩ < c 1
⊢ c ⟨i, hi⟩ = ⊥
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
x : P
⊢ x ∈ ↑I + ↑J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
Submodule.add_eq_sup

Goal state after:
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
x : P
⊢ x ∈ ↑I ⊔ ↑J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 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
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
x y : P
x✝¹ : x ∈ span R s
x✝ : y ∈ span R s
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • (x + y))

Tactic:
by
          rw [smul_add]
          exact isInteger_add hx hy

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

Goal state before:
pp: case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : (algebraMap K L) y ∈ I
⊢ (algebraMap K L) x ∈ I

Tactic:
← div_mul_cancel₀ x y_ne,

Goal state after:
case mpr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
x y : K
y_ne : y ≠ 0
y_mem : (algebraMap K L) y ∈ I
⊢ (algebraMap K L) (x / y * y) ∈ I
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
i : ℕ
⊢ x ^ i ∈ ↑(↑I)⁻¹

Tactic:
induction i with

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⁻¹

pp: case inr
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 J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹

Tactic:
· simp [inv_zero']

Goal state after:
case inr
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 J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I / J = I * J⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this✝ : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ M = ⊤

Tactic:
rw [eq_top_iff, ← coeIdeal_le_coeIdeal (FractionRing A), coeIdeal_top]

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this✝ : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
this : (↑M)⁻¹ * ↑P ≤ ↑P
⊢ 1 ≤ ↑M
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
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
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_in_q : Weight.toLinear K (↥H) L χ ∈ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
by
  have h_h_containment : ⁅x_χ, (y : L)⁆ ∈ genWeightSpace L χ := by
    have h_zero_weight : H.toLieSubmodule.incl y ∈ genWeightSpace L (0 : H → K) := by
      apply toLieSubmodule_le_rootSpace_zero
      exact y.property
    convert! lie_mem_genWeightSpace_of_mem_genWeightSpace hx_χ h_zero_weight
    ext h; simp
  have h_bracket_decomp : ⁅x_χ, m_α⁆ ∈
      genWeightSpace L (χ.toLinear + α.toLinear) ⊔
      genWeightSpace L (χ.toLinear - α.toLinear) ⊔ genWeightSpace L χ := by
    rw [h_bracket_sum]
    exact add_mem (add_mem
      (Submodule.mem_sup_left (Submodule.mem_sup_left h_pos_containment))
      (Submodule.mem_sup_left (Submodule.mem_sup_right h_neg_containment)))
      (Submodule.mem_sup_right h_h_containment)
  let I := ⨆ β : {β : Weight K H L // ↑β ∈ q ∧ β.IsNonZero}, sl2SubmoduleOfRoot β.2.2
  have genWeightSpace_le_I (β_lin : H →ₗ[K] K) (hβ_in_q : β_lin ∈ q)
      (hβ_ne_zero : β_lin ≠ 0) : genWeightSpace L β_lin ≤ I := by
    by_cases h_trivial : genWeightSpace L β_lin = ⊥
    · simp [h_trivial]
    · let β : Weight K H L := ⟨β_lin, h_trivial⟩
      have hβ_nonzero : β.IsNonZero := Weight.coe_toLinear_ne_zero_iff.mp hβ_ne_zero
      refine le_trans ?_ (le_iSup _ ⟨β, hβ_in_q, hβ_nonzero⟩)
      rw [sl2SubmoduleOfRoot_eq_sup]
      exact le_sup_of_le_left (le_sup_of_le_left le_rfl)
  have h_plus_contain : genWeightSpace L (χ.toLinear + α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (q.add_mem h_chi_in_q hαq) w_plus
  have h_minus_contain : genWeightSpace L (χ.toLinear - α.toLinear) ≤ I :=
    genWeightSpace_le_I _ (by
      have : -α.toLinear = (-1 : K) • α.toLinear := by simp
      rw [sub_eq_add_neg, this]
      exact q.add_mem h_chi_in_q (q.smul_mem (-1) hαq)) w_minus
  have h_chi_contain : genWeightSpace L χ.toLinear ≤ I :=
    genWeightSpace_le_I _ h_chi_in_q (fun h_eq => (w_chi h_eq).elim)
  exact sup_le (sup_le h_plus_contain h_minus_contain) h_chi_contain h_bracket_decomp

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
⊢ ∀ {a : Ideal A}, Irreducible a ↔ Prime a

Tactic:
intro P

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
P : Ideal A
⊢ Irreducible P ↔ Prime P
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: 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
⊢ Associated (factors I).prod I

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 factors_prod hI

Goal state after:
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

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.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
x✝¹ x✝ : Ideal A
⊢ x✝¹ ⊔ x✝ ∣ x✝¹

Tactic:
by simpa only [dvd_iff_le] using le_sup_left

Goal state after: