mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
⊢ ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)

Tactic:
intro j hjs

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
ι : Type u_4
s✝ : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH : (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
r : A
hr : r ∈ span s
⊢ ↑(((decompose 𝒜) r) i) ∈ span s

Tactic:
rw [Ideal.span, Finsupp.span_eq_range_linearCombination] at hr

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
r : A
hr : r ∈ (Finsupp.linearCombination A Subtype.val).range
⊢ ↑(((decompose 𝒜) r) i) ∈ span s
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (SupSet.sSup ℐ)

Tactic:
rw [sSup_eq_iSup]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨆ a ∈ ℐ, a)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
by
  rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]
  exact nonTorsionWeight_of (Function.const σ one_ne_zero)

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (X i).IsHomogeneous 1

Tactic:
by
  apply isHomogeneous_monomial
  simp only [degree_apply, Finsupp.support_single _ one_ne_zero, Finset.sum_singleton,
    single_eq_same]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ (weightedHomogeneousComponent w m) φ ∈ weightedHomogeneousSubmodule R w m

Tactic:
rw [mem_weightedHomogeneousSubmodule]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
m : M
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
n : M
p : MvPolynomial σ R
⊢ ((weightedHomogeneousComponent w n) p).support = {c ∈ p.support | (weight w) c = n}

Tactic:
by
  ext c
  simp [coeff_weightedHomogeneousComponent, And.comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ (homogeneousComponent n) φ = 0

Tactic:
apply homogeneousComponent_eq_zero'

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ ∀ d ∈ φ.support, degree d ≠ n
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✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
⊢ ∃ x, φ.IsNilRegular x

Tactic:
let b := chooseBasis R L

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✝ : IsDomain R
h : ↑(finrank R M) ≤ #R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
⊢ ∃ x, φ.IsNilRegular x
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)

Tactic:
LinearMap.map_span,

Goal state after:
m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ span R (⇑f '' range A.col) = span R (range (A.submatrix r id).col)
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : Invertible A
hA : fromBlocks A B C D ∈ symplecticGroup l R
⊢ (fromBlocks A B C D).det = 1

Tactic:
have h_block := fromBlocks_mem_iff.1 hA

Goal state after:
l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : Invertible A
hA : fromBlocks A B C D ∈ symplecticGroup l R
h_block : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ (fromBlocks A B C D).det = 1
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ toENat #m = ENat.card m

Tactic:
ENat.card

Goal state after:
m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ toENat #m = toENat #m
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 :
  (Q.submatrix ⇑s.symm ⇑s.symm)ᵀ * f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s) =
    f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s)ᵀ * f Q
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0

Tactic:
← hf Q,

Goal state after:
l : Type u_1
inst✝² : DecidableEq l
inst✝¹ : Fintype l
R : Type u_3
inst✝ : Field R
A C : Matrix l l R
hker : ∀ (x : l → R), A • x = 0 → C • x = 0 → x = 0
hsymm : Aᵀ * C = Cᵀ * A
V U : Matrix l l R
s : l ≃ Fin C.rank ⊕ Fin (Fintype.card l - C.rank)
hV : IsUnit V
hU : IsUnit U
P : Matrix l l R := V * C * U
heq : P = (fromBlocks 1 0 0 0).submatrix ⇑s ⇑s
P_def : P = V * C * U
Q : Matrix l l R := Vᵀ⁻¹ * A * U
Q_def : Q = Vᵀ⁻¹ * A * U
f : Matrix l l R → Matrix (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) (Fin C.rank ⊕ Fin (Fintype.card l - C.rank)) R :=
  fun x ↦ x.submatrix ⇑s.symm ⇑s.symm
hf : ∀ (x : Matrix l l R), f x = x.submatrix ⇑s.symm ⇑s.symm
f_unit : ∀ {x : Matrix l l R}, IsUnit x → IsUnit (f x)
f_mul : ∀ (x y : Matrix l l R), f (x * y) = f x * f y
x✝² : Invertible V
x✝¹ : Invertible U
x✝ : Invertible (f Vᵀ)
con1 : ∀ (x : Fin C.rank ⊕ Fin (Fintype.card l - C.rank) → R), f Q • x = 0 → f P • x = 0 → x = 0
con2 : (f Q)ᵀ * f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s) = f ((fromBlocks 1 0 0 0).submatrix ⇑s ⇑s)ᵀ * f Q
⊢ (f Q).toBlocks₁₁ᵀ = (f Q).toBlocks₁₁ ∧ (f Q).toBlocks₁₂ = 0
Module: Mathlib.Algebra.Lie.Cochain

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x : L
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun z ↦
        ⁅x, (a (x✝¹ • x✝)) z⁆ - ⁅x✝¹ • x✝, (a x) z⁆ + ⁅z, (a x) (x✝¹ • x✝)⁆ - (a ⁅x, x✝¹ • x✝⁆) z +
            (a ⁅x, z⁆) (x✝¹ • x✝) -
          (a ⁅x✝¹ • x✝, z⁆) x,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      { toFun := fun z ↦ ⁅x, (a x✝) z⁆ - ⁅x✝, (a x) z⁆ + ⁅z, (a x) x✝⁆ - (a ⁅x, x✝⁆) z + (a ⁅x, z⁆) x✝ - (a ⁅x✝, z⁆) x,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp; abel_nf; simp

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

Goal state before:
pp: 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
a : ↥(twoCochain R L M)
x✝¹ : R
x✝ : L
⊢ {
      toFun := fun y ↦
        {
          toFun := fun z ↦
            ⁅x✝¹ • x✝, (a y) z⁆ - ⁅y, (a (x✝¹ • x✝)) z⁆ + ⁅z, (a (x✝¹ • x✝)) y⁆ - (a ⁅x✝¹ • x✝, y⁆) z +
                (a ⁅x✝¹ • x✝, z⁆) y -
              (a ⁅y, z⁆) (x✝¹ • x✝),
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun y ↦
          {
            toFun := fun z ↦
              ⁅x✝, (a y) z⁆ - ⁅y, (a x✝) z⁆ + ⁅z, (a x✝) y⁆ - (a ⁅x✝, y⁆) z + (a ⁅x✝, z⁆) y - (a ⁅y, z⁆) x✝,
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp; abel_nf; simp

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

Goal state before:
pp: 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
x✝¹ : R
x✝ : ↥(twoCochain R L M)
⊢ {
      toFun := fun x ↦
        {
          toFun := fun y ↦
            {
              toFun := fun z ↦
                ⁅x, ((x✝¹ • x✝) y) z⁆ - ⁅y, ((x✝¹ • x✝) x) z⁆ + ⁅z, ((x✝¹ • x✝) x) y⁆ - ((x✝¹ • x✝) ⁅x, y⁆) z +
                    ((x✝¹ • x✝) ⁅x, z⁆) y -
                  ((x✝¹ • x✝) ⁅y, z⁆) x,
              map_add' := ⋯, map_smul' := ⋯ },
          map_add' := ⋯, map_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) x✝¹ •
      {
        toFun := fun x ↦
          {
            toFun := fun y ↦
              {
                toFun := fun z ↦
                  ⁅x, (x✝ y) z⁆ - ⁅y, (x✝ x) z⁆ + ⁅z, (x✝ x) y⁆ - (x✝ ⁅x, y⁆) z + (x✝ ⁅x, z⁆) y - (x✝ ⁅y, z⁆) x,
                map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ },
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp; abel_nf; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Grading

Goal state before:
pp: M : Type u_1
ι : Type u_2
R : Type u_3
inst✝² : AddMonoid M
inst✝¹ : AddMonoid ι
inst✝ : CommSemiring R
f : M →+ ι
m : M
h : m ∈ (coeff 1).support
⊢ f m = 0

Tactic:
by
    rw [one_def] at h
    obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h
    apply map_zero

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : DecidableEq A
inst✝ : AddCommMonoid A
i j : A
xj : ↥(AddMonoidAlgebra.grade R j) ⊗[R] L
x : ↥(AddMonoidAlgebra.grade R i)
y : L
⊢ ⁅↑x ⊗ₜ[R] y, (LinearMap.rTensor L (AddMonoidAlgebra.grade R j).subtype) xj⁆ ∈
    (LinearMap.rTensor L (AddMonoidAlgebra.grade R (i + j)).subtype).range

Tactic:
induction xj using TensorProduct.induction_on with
      | zero => simp
      | tmul u v =>
        obtain ⟨x, hx⟩ := x
        obtain ⟨u, hu⟩ := u
        use ⟨x * u, SetLike.mul_mem_graded hx hu⟩ ⊗ₜ ⁅y, v⁆
        simp
      | add u v hu hv =>
        rw [LinearMap.map_add, lie_add]
        obtain ⟨u', hu'⟩ := hu
        obtain ⟨v', hv'⟩ := hv
        use u' + v'
        simp [← hu', ← hv']

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ (f.toList x).formPerm = f.cycleOf x

Tactic:
rw [(cycleOf_eq_one_iff f).mpr hx, toList_eq_nil_iff.mpr (notMem_support.mpr hx),
      formPerm_nil]

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

Goal state before:
pp: case step
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : lo < n
ih : BirdDet.sumFrom n (lo + 1) f = ∑ k ∈ Finset.Ico (lo + 1) n, f k
⊢ f lo + ∑ k ∈ Finset.Ico (lo + 1) n, f k = ∑ k ∈ Finset.Ico lo n, f k

Tactic:
← Finset.sum_eq_sum_Ico_succ_bot hlo f

Goal state after:
case step
R : Type u_1
inst✝ : CommRing R
n : ℕ
f : ℕ → R
lo : ℕ
hlo : lo < n
ih : BirdDet.sumFrom n (lo + 1) f = ∑ k ∈ Finset.Ico (lo + 1) n, f k
⊢ ∑ k ∈ Finset.Ico lo n, f k = ∑ k ∈ Finset.Ico lo n, f k
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
⊢ A.det = Spec.birdDet A

Tactic:
have : ∑ α ∈ S k 0, bminor A 0 0 α = A.det := by simp [bminor]
    rw [Spec.birdDetSpec_succ, paper_eq1, Matrix.of_apply, ← mul_assoc, ← pow_add]; aesop

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

Goal state before:
pp: n : ℕ
⊢ (B n)ᵀ = C n

Tactic:
by
  ext; simp only [B, C, transpose_apply, of_apply]; grind

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q r : Associates M
hp : Prime p
hr : r ∣ q
hp' : p ∣ r
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
⊢ p = c 1

Tactic:
obtain ⟨i, rfl⟩ := h₂.1 (dvd_trans hp' hr)

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q r : Associates M
hr : r ∣ q
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 : Fin (n + 1 + 1)
hp : Prime (c i)
hp' : c i ∣ r
⊢ c i = c 1
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
p : FractionalIdeal S P
s : Set P
hs : s = ↑p
⊢ IsFractional S ((↑p).copy s hs)

Tactic:
convert! p.isFractional
    ext
    simp only [hs]
    rfl

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

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b

Tactic:
obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb)

Goal state after:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
h : I ≤ 1
b' : R
hb : (algebraMap R P) b' ∈ I
⊢ IsInteger R ((algebraMap R P) b')
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α_span : Weight.toLinear K (↥H) L ↑α ∈ I.rootSpan
hα_not : α ∉ I.rootSet
hα_nz : (↑α).IsNonZero
this✝ : I.rootSpan ≤ LinearMap.ker ((Dual.eval K ↥H) (coroot ↑α))
this : 2 = 0
⊢ False

Tactic:
exact absurd this two_ne_zero

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✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
⊢ ¬(↑I)⁻¹ ≤ 1

Tactic:
refine Set.not_subset.2 ⟨algebraMap A K b * (algebraMap A K a)⁻¹, (mem_inv_iff ?_).mpr ?_, ?_⟩

Goal state after:
case refine_1
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
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
⊢ ↑I ≠ 0

case refine_2
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
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
⊢ ∀ y ∈ ↑I, (algebraMap A K) b * ((algebraMap A K) a)⁻¹ * y ∈ 1

case refine_3
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
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
⊢ (algebraMap A K) b * ((algebraMap A K) a)⁻¹ ∉ ↑1
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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ (algebraMap R₁ K) y' = 0

Tactic:
y'_eq_zero,

Goal state after:
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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ (algebraMap R₁ K) 0 = 0
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 : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * aJ • y)

Tactic:
rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]

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
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1

Tactic:
← h.toEquiv.apply_eq_iff_eq

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
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → h.toEquiv (x * x⁻¹) = h.toEquiv 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1